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

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