let n be Nat; for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 * M2 = 0. (K,n,n) & M1 is invertible holds
M1 commutes_with M2
let K be Field; for M1, M2 being Matrix of n,K st n > 0 & M1 * M2 = 0. (K,n,n) & M1 is invertible holds
M1 commutes_with M2
let M1, M2 be Matrix of n,K; ( n > 0 & M1 * M2 = 0. (K,n,n) & M1 is invertible implies M1 commutes_with M2 )
assume that
A1:
n > 0
and
A2:
M1 * M2 = 0. (K,n,n)
and
A3:
M1 is invertible
; M1 commutes_with M2
A4:
M1 ~ is_reverse_of M1
by A3, Def4;
A5:
len M2 = n
by MATRIX_0:24;
A6:
( len M1 = n & width M1 = n )
by MATRIX_0:24;
A7:
len (M1 ~) = n
by MATRIX_0:24;
A8:
width (M1 ~) = n
by MATRIX_0:24;
M2 =
(1. (K,n)) * M2
by MATRIX_3:18
.=
((M1 ~) * M1) * M2
by A4
.=
(M1 ~) * (0. (K,n,n))
by A2, A6, A5, A8, MATRIX_3:33
.=
0. (K,n,n)
by A1, A7, A8, Th2
;
hence
M1 commutes_with M2
by Th3; verum