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