let n be Nat; for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds
M1 + M2 commutes_with M2 + M2
let K be Field; for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds
M1 + M2 commutes_with M2 + M2
let M1, M2 be Matrix of n,K; ( n > 0 & M1 commutes_with M2 implies M1 + M2 commutes_with M2 + M2 )
assume that
A1:
n > 0
and
A2:
M1 commutes_with M2
; M1 + M2 commutes_with M2 + M2
A3:
( len M2 = n & width M2 = n )
by MATRIX_0:24;
A4:
len (M1 + M2) = n
by MATRIX_0:24;
A5:
( width M1 = n & len M1 = n )
by MATRIX_0:24;
width (M1 + M2) = n
by MATRIX_0:24;
then (M1 + M2) * (M2 + M2) =
((M1 + M2) * M2) + ((M1 + M2) * M2)
by A1, A3, A4, MATRIX_4:62
.=
((M1 * M2) + (M2 * M2)) + ((M1 + M2) * M2)
by A1, A3, A5, MATRIX_4:63
.=
((M1 * M2) + (M2 * M2)) + ((M1 * M2) + (M2 * M2))
by A1, A3, A5, MATRIX_4:63
.=
((M2 * M1) + (M2 * M2)) + ((M1 * M2) + (M2 * M2))
by A2
.=
((M2 * M1) + (M2 * M2)) + ((M2 * M1) + (M2 * M2))
by A2
.=
(M2 * (M1 + M2)) + ((M2 * M1) + (M2 * M2))
by A1, A3, A5, MATRIX_4:62
.=
(M2 * (M1 + M2)) + (M2 * (M1 + M2))
by A1, A3, A5, MATRIX_4:62
.=
(M2 + M2) * (M1 + M2)
by A1, A3, A4, MATRIX_4:63
;
hence
M1 + M2 commutes_with M2 + M2
; verum