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 A1: ( M1 is invertible & M2 is invertible & M1 commutes_with M2 ) ; :: thesis: ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~ ) * (M2 ~ ) )
A2: ( M1 is Matrix of n,K & M2 is Matrix of n,K & width M1 = n & len M2 = n & width M2 = n & len M1 = n ) by MATRIX_1:25;
A3: ( M1 ~ is Matrix of n,K & M2 ~ is Matrix of n,K & width (M1 ~ ) = n & len (M2 ~ ) = n & width (M2 ~ ) = n & len (M1 ~ ) = n ) by MATRIX_1:25;
A4: ( width ((M1 ~ ) * (M2 ~ )) = n & len ((M1 ~ ) * (M2 ~ )) = n & width (M1 * M2) = n & len (M1 * M2) = n ) by MATRIX_1:25;
A5: ( M2 ~ is_reverse_of M2 & M1 ~ is_reverse_of M1 ) by A1, Def4;
A6: ((M1 ~ ) * (M2 ~ )) * (M1 * M2) = ((M1 ~ ) * (M2 ~ )) * (M2 * M1) by A1, Def1
.= (((M1 ~ ) * (M2 ~ )) * M2) * M1 by A2, A4, MATRIX_3:35
.= ((M1 ~ ) * ((M2 ~ ) * M2)) * M1 by A2, A3, MATRIX_3:35
.= ((M1 ~ ) * (1. K,n)) * M1 by A5, Def2
.= (M1 ~ ) * M1 by MATRIX_3:21
.= 1. K,n by A5, Def2 ;
(M1 * M2) * ((M1 ~ ) * (M2 ~ )) = ((M1 * M2) * (M1 ~ )) * (M2 ~ ) by A3, A4, MATRIX_3:35
.= ((M2 * M1) * (M1 ~ )) * (M2 ~ ) by A1, Def1
.= (M2 * (M1 * (M1 ~ ))) * (M2 ~ ) by A2, A3, MATRIX_3:35
.= (M2 * (1. K,n)) * (M2 ~ ) by A5, Def2
.= M2 * (M2 ~ ) by MATRIX_3:21
.= 1. K,n by A5, Def2 ;
then A7: (M1 ~ ) * (M2 ~ ) is_reverse_of M1 * M2 by A6, Def2;
then M1 * M2 is invertible by Def3;
hence ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~ ) * (M2 ~ ) ) by A7, Def4; :: thesis: verum