let n be Nat; :: thesis: for R being Ring
for M1, M2, M3 being Matrix of n,R st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds
M1 commutes_with M2 * M3
let R be Ring; :: thesis: for M1, M2, M3 being Matrix of n,R 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,R; :: 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