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