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

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