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 @ commutes_with M2 @
let K be Field; for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds
M1 @ commutes_with M2 @
let M1, M2 be Matrix of n,K; ( n > 0 & M1 commutes_with M2 implies M1 @ commutes_with M2 @ )
A1:
( width M1 = n & width M2 = n )
by MATRIX_0:24;
set M3 = M1 @ ;
set M4 = M2 @ ;
A2:
len M2 = n
by MATRIX_0:24;
assume that
A3:
n > 0
and
A4:
M1 commutes_with M2
; M1 @ commutes_with M2 @
len M1 = n
by MATRIX_0:24;
then (M1 @) * (M2 @) =
(M2 * M1) @
by A1, A3, MATRIX_3:22
.=
(M1 * M2) @
by A4
.=
(M2 @) * (M1 @)
by A1, A2, A3, MATRIX_3:22
;
hence
M1 @ commutes_with M2 @
; verum