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_0:24;
A4: width M2 = n by MATRIX_0:24;
A5: ( M1 @ = M1 & M2 @ = M2 ) by A2;
thus ( M1 commutes_with M2 implies M1 * M2 is symmetric ) by A1, A5, A3, A4, MATRIX_3:22; :: thesis: ( M1 * M2 is symmetric implies M1 commutes_with M2 )
assume A6: M1 * M2 is symmetric ; :: thesis: M1 commutes_with M2
M2 * M1 = (M1 * M2) @ by A1, A5, A3, A4, MATRIX_3:22
.= M1 * M2 by A6 ;
hence M1 commutes_with M2 ; :: thesis: verum