Formalizace důkazu v lineární algebře – Matematika – Fórum – Programujte.com

Ahoj, mám menší problém s formalizací důkazu:

Příklad - Nechť A,B jsou matice z T(n,n), potom matice A,B jsou obě regulární právě tehdy, když matice AB a BA jsou obě regulární. Dokažte.

Postupoval jsem tedy takto:
Regulární matici definujeme jako takovou, která má nenulový determinant.
Determinant A = a11*a22*a33*...*ann   -> determinant je vynásobením všech prvků hlavní diagonály. čísla jsou indexy.

Podle definice maticového násobení tedy ((AB)nn := (sum from l=1 to n; Anl*Bln))  n a l jsou indexy.
Takže i pro matici AB i BA musí platit, že pokud by A nebo B nebyly regulární, po vynásobení můžou vzniknout v hlavní diagonále nuly, tj determinant matice AB nebo BA by v sobě měl nulu
det AB = ab11*ab22*ab33*...*0*...*abnn   -> kvůli čemuž by samotný determinant byl nulový a matice by nebyla regulární.

Pokud jsem někde udělal chybu, prosím, opravte mne. Pokud ne, jak by šel takovýto důkaz formalizovat?
Předem díky za odpovědi :)