let n be Nat; :: thesis: for R being Ring
for M1, M2, M3 being Matrix of n,R st M1 commutes_with M2 & 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 & M1 commutes_with M3 holds
M1 commutes_with M2 + M3
let M1, M2, M3 be Matrix of n,R; :: thesis: ( M1 commutes_with M2 & M1 commutes_with M3 implies M1 commutes_with M2 + M3 )
A1: width M1 = n by MATRIX_0:24;
A2: ( len M1 = n & len M2 = n ) by MATRIX_0:24;
A3: len M3 = n by MATRIX_0:24;
assume that
A4: M1 commutes_with M2 and
A5: M1 commutes_with M3 ; :: thesis: M1 commutes_with M2 + M3
A6: ( width M2 = n & width M3 = n ) by MATRIX_0:24;
then (M2 + M3) * M1 = (M2 * M1) + (M3 * M1) by A2, A3, MATRIX_4:63
.= (M1 * M2) + (M3 * M1) by A4
.= (M1 * M2) + (M1 * M3) by A5
.= M1 * (M2 + M3) by A1, A6, A2, A3, MATRIX_4:62 ;
hence M1 commutes_with M2 + M3 ; :: thesis: verum