let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Nilpotent & M1 commutes_with M2 & n > 0 holds
M1 * M2 is Nilpotent
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is Nilpotent & M1 commutes_with M2 & n > 0 holds
M1 * M2 is Nilpotent
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is Nilpotent & M1 commutes_with M2 & n > 0 implies M1 * M2 is Nilpotent )
assume that
A1: M1 is Nilpotent and
A2: M1 commutes_with M2 and
A3: n > 0 ; :: thesis: M1 * M2 is Nilpotent
A4: ( len M1 = n & width M1 = n ) by MATRIX_0:24;
A5: width M2 = n by MATRIX_0:24;
A6: width (M2 * M1) = n by MATRIX_0:24;
A7: len M2 = n by MATRIX_0:24;
(M1 * M2) * (M1 * M2) = (M2 * M1) * (M1 * M2) by A2, MATRIX_6:def 1
.= ((M2 * M1) * M1) * M2 by A4, A7, A6, MATRIX_3:33
.= (M2 * (M1 * M1)) * M2 by A4, A5, MATRIX_3:33
.= (M2 * (0. (K,n))) * M2 by A1
.= (0. (K,n,n)) * M2 by A3, A7, A5, MATRIX_6:2
.= 0. (K,n) by A7, A5, MATRIX_6:1 ;
hence M1 * M2 is Nilpotent ; :: thesis: verum