let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is symmetric & M2 is symmetric holds
( M1 commutes_with M2 iff M1 * M2 is symmetric )
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 is symmetric & M2 is symmetric holds
( M1 commutes_with M2 iff M1 * M2 is symmetric )
let M1, M2 be Matrix of n,K; :: thesis: ( n > 0 & M1 is symmetric & M2 is symmetric implies ( M1 commutes_with M2 iff M1 * M2 is symmetric ) )
assume that
A1: n > 0 and
A2: ( M1 is symmetric & M2 is symmetric ) ; :: thesis: ( M1 commutes_with M2 iff M1 * M2 is symmetric )
A3: ( width M1 = n & len M2 = n ) by MATRIX_1:25;
A4: width M2 = n by MATRIX_1:25;
A5: ( M1 @ = M1 & M2 @ = M2 ) by A2, Def5;
thus ( M1 commutes_with M2 implies M1 * M2 is symmetric ) :: thesis: ( M1 * M2 is symmetric implies M1 commutes_with M2 )

proof

assume A6: M1 commutes_with M2 ; :: thesis: M1 * M2 is symmetric
(M1 * M2) @ = M2 * M1 by A1, A5, A3, A4, MATRIX_3:24
.= M1 * M2 by A6, Def1 ;
hence M1 * M2 is symmetric by Def5; :: thesis: verum

end;

assume A7: M1 * M2 is symmetric ; :: thesis: M1 commutes_with M2
M2 * M1 = (M1 * M2) @ by A1, A5, A3, A4, MATRIX_3:24
.= M1 * M2 by A7, Def5 ;
hence M1 commutes_with M2 by Def1; :: thesis: verum