let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible & M1 commutes_with M2 holds
( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~ ) * (M2 ~ ) )
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible & M1 commutes_with M2 holds
( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~ ) * (M2 ~ ) )
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is invertible & M2 is invertible & M1 commutes_with M2 implies ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~ ) * (M2 ~ ) ) )
assume that
A1: M1 is invertible and
A2: M2 is invertible and
A3: M1 commutes_with M2 ; :: thesis: ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~ ) * (M2 ~ ) )
A4: M2 ~ is_reverse_of M2 by A2, Def4;
A5: width ((M1 ~ ) * (M2 ~ )) = n by MATRIX_1:25;
A6: width (M2 ~ ) = n by MATRIX_1:25;
A7: len M2 = n by MATRIX_1:25;
A8: width M1 = n by MATRIX_1:25;
A9: ( width M2 = n & len M1 = n ) by MATRIX_1:25;
A10: M1 ~ is_reverse_of M1 by A1, Def4;
A11: ( width (M1 ~ ) = n & len (M2 ~ ) = n ) by MATRIX_1:25;
A12: len (M1 ~ ) = n by MATRIX_1:25;
width (M1 * M2) = n by MATRIX_1:25;
then A13: (M1 * M2) * ((M1 ~ ) * (M2 ~ )) = ((M1 * M2) * (M1 ~ )) * (M2 ~ ) by A11, A12, MATRIX_3:35
.= ((M2 * M1) * (M1 ~ )) * (M2 ~ ) by A3, Def1
.= (M2 * (M1 * (M1 ~ ))) * (M2 ~ ) by A8, A9, A12, MATRIX_3:35
.= (M2 * (1. K,n)) * (M2 ~ ) by A10, Def2
.= M2 * (M2 ~ ) by MATRIX_3:21
.= 1. K,n by A4, Def2 ;
((M1 ~ ) * (M2 ~ )) * (M1 * M2) = ((M1 ~ ) * (M2 ~ )) * (M2 * M1) by A3, Def1
.= (((M1 ~ ) * (M2 ~ )) * M2) * M1 by A7, A9, A5, MATRIX_3:35
.= ((M1 ~ ) * ((M2 ~ ) * M2)) * M1 by A7, A11, A6, MATRIX_3:35
.= ((M1 ~ ) * (1. K,n)) * M1 by A4, Def2
.= (M1 ~ ) * M1 by MATRIX_3:21
.= 1. K,n by A10, Def2 ;
then A14: (M1 ~ ) * (M2 ~ ) is_reverse_of M1 * M2 by A13, Def2;
then M1 * M2 is invertible by Def3;
hence ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~ ) * (M2 ~ ) ) by A14, Def4; :: thesis: verum