let n be Nat; :: thesis: for K being Field

for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds

M1 commutes_with M2 * M3

let K be Field; :: thesis: for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds

M1 commutes_with M2 * M3

let M1, M2, M3 be Matrix of n,K; :: thesis: ( M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 implies M1 commutes_with M2 * M3 )

A1: width M1 = n by MATRIX_0:24;

A2: width M2 = n by MATRIX_0:24;

A3: len M1 = n by MATRIX_0:24;

A4: len M3 = n by MATRIX_0:24;

A5: ( width M3 = n & len M2 = n ) by MATRIX_0:24;

assume that

A6: M1 commutes_with M2 and

A7: M2 commutes_with M3 and

A8: M1 commutes_with M3 ; :: thesis: M1 commutes_with M2 * M3

(M2 * M3) * M1 = (M3 * M2) * M1 by A7

.= M3 * (M2 * M1) by A2, A3, A5, MATRIX_3:33

.= M3 * (M1 * M2) by A6

.= (M3 * M1) * M2 by A1, A3, A5, MATRIX_3:33

.= (M1 * M3) * M2 by A8

.= M1 * (M3 * M2) by A1, A5, A4, MATRIX_3:33

.= M1 * (M2 * M3) by A7 ;

hence M1 commutes_with M2 * M3 ; :: thesis: verum

for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds

M1 commutes_with M2 * M3

let K be Field; :: thesis: for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds

M1 commutes_with M2 * M3

let M1, M2, M3 be Matrix of n,K; :: thesis: ( M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 implies M1 commutes_with M2 * M3 )

A1: width M1 = n by MATRIX_0:24;

A2: width M2 = n by MATRIX_0:24;

A3: len M1 = n by MATRIX_0:24;

A4: len M3 = n by MATRIX_0:24;

A5: ( width M3 = n & len M2 = n ) by MATRIX_0:24;

assume that

A6: M1 commutes_with M2 and

A7: M2 commutes_with M3 and

A8: M1 commutes_with M3 ; :: thesis: M1 commutes_with M2 * M3

(M2 * M3) * M1 = (M3 * M2) * M1 by A7

.= M3 * (M2 * M1) by A2, A3, A5, MATRIX_3:33

.= M3 * (M1 * M2) by A6

.= (M3 * M1) * M2 by A1, A3, A5, MATRIX_3:33

.= (M1 * M3) * M2 by A8

.= M1 * (M3 * M2) by A1, A5, A4, MATRIX_3:33

.= M1 * (M2 * M3) by A7 ;

hence M1 commutes_with M2 * M3 ; :: thesis: verum