let n be Nat; for K being Field
for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds
M1 * M1 commutes_with M2 * M2
let K be Field; for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds
M1 * M1 commutes_with M2 * M2
let M1, M2 be Matrix of n,K; ( M1 commutes_with M2 implies M1 * M1 commutes_with M2 * M2 )
A1:
width M2 = n
by MATRIX_0:24;
A2:
len (M1 * M1) = n
by MATRIX_0:24;
A3:
( width M1 = n & len M1 = n )
by MATRIX_0:24;
assume A4:
M1 commutes_with M2
; M1 * M1 commutes_with M2 * M2
A5:
len M2 = n
by MATRIX_0:24;
A6:
width (M1 * M1) = n
by MATRIX_0:24;
then (M1 * M1) * (M2 * M2) =
((M1 * M1) * M2) * M2
by A1, A5, MATRIX_3:33
.=
(M1 * (M1 * M2)) * M2
by A3, A5, MATRIX_3:33
.=
(M1 * (M2 * M1)) * M2
by A4
.=
((M1 * M2) * M1) * M2
by A1, A3, A5, MATRIX_3:33
.=
((M2 * M1) * M1) * M2
by A4
.=
(M2 * (M1 * M1)) * M2
by A1, A3, MATRIX_3:33
.=
M2 * ((M1 * M1) * M2)
by A1, A5, A6, A2, MATRIX_3:33
.=
M2 * (M1 * (M1 * M2))
by A3, A5, MATRIX_3:33
.=
M2 * (M1 * (M2 * M1))
by A4
.=
M2 * ((M1 * M2) * M1)
by A1, A3, A5, MATRIX_3:33
.=
M2 * ((M2 * M1) * M1)
by A4
.=
M2 * (M2 * (M1 * M1))
by A1, A3, MATRIX_3:33
.=
(M2 * M2) * (M1 * M1)
by A1, A5, A2, MATRIX_3:33
;
hence
M1 * M1 commutes_with M2 * M2
; verum