let n be Nat; :: thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 is invertible & M3 is invertible holds
( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~ ) * (M2 ~ )) * (M1 ~ ) )
let K be Field; :: thesis: for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 is invertible & M3 is invertible holds
( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~ ) * (M2 ~ )) * (M1 ~ ) )
let M1, M2, M3 be Matrix of n,K; :: thesis: ( M1 is invertible & M2 is invertible & M3 is invertible implies ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~ ) * (M2 ~ )) * (M1 ~ ) ) )
assume that
A1: M1 is invertible and
A2: M2 is invertible and
A3: M3 is invertible ; :: thesis: ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~ ) * (M2 ~ )) * (M1 ~ ) )
A4: M1 ~ is_reverse_of M1 by A1, Def4;
A5: M2 ~ is_reverse_of M2 by A2, Def4;
A6: len M3 = n by MATRIX_1:25;
A7: M3 ~ is_reverse_of M3 by A3, Def4;
A8: width (M2 ~ ) = n by MATRIX_1:25;
A9: width M3 = n by MATRIX_1:25;
A10: width (M1 * M2) = n by MATRIX_1:25;
A11: len (M1 ~ ) = n by MATRIX_1:25;
set M5 = ((M3 ~ ) * (M2 ~ )) * (M1 ~ );
set M4 = (M1 * M2) * M3;
A12: width M2 = n by MATRIX_1:25;
A13: ( len (M2 * M3) = n & width (((M3 ~ ) * (M2 ~ )) * (M1 ~ )) = n ) by MATRIX_1:25;
A14: len M2 = n by MATRIX_1:25;
A15: ( width ((M1 * M2) * M3) = n & len ((M2 ~ ) * (M1 ~ )) = n ) by MATRIX_1:25;
A16: len (M3 ~ ) = n by MATRIX_1:25;
A17: width ((M3 ~ ) * (M2 ~ )) = n by MATRIX_1:25;
A18: width (M3 ~ ) = n by MATRIX_1:25;
A19: width (M1 ~ ) = n by MATRIX_1:25;
A20: len M1 = n by MATRIX_1:25;
A21: len (M2 ~ ) = n by MATRIX_1:25;
A22: width M1 = n by MATRIX_1:25;
then A23: (((M3 ~ ) * (M2 ~ )) * (M1 ~ )) * ((M1 * M2) * M3) = (((M3 ~ ) * (M2 ~ )) * (M1 ~ )) * (M1 * (M2 * M3)) by A12, A14, A6, MATRIX_3:35
.= ((((M3 ~ ) * (M2 ~ )) * (M1 ~ )) * M1) * (M2 * M3) by A22, A20, A13, MATRIX_3:35
.= (((M3 ~ ) * (M2 ~ )) * ((M1 ~ ) * M1)) * (M2 * M3) by A20, A19, A11, A17, MATRIX_3:35
.= (((M3 ~ ) * (M2 ~ )) * (1. K,n)) * (M2 * M3) by A4, Def2
.= ((M3 ~ ) * (M2 ~ )) * (M2 * M3) by MATRIX_3:21
.= (((M3 ~ ) * (M2 ~ )) * M2) * M3 by A12, A14, A6, A17, MATRIX_3:35
.= ((M3 ~ ) * ((M2 ~ ) * M2)) * M3 by A14, A8, A18, A21, MATRIX_3:35
.= ((M3 ~ ) * (1. K,n)) * M3 by A5, Def2
.= (M3 ~ ) * M3 by MATRIX_3:21
.= 1. K,n by A7, Def2 ;
((M1 * M2) * M3) * (((M3 ~ ) * (M2 ~ )) * (M1 ~ )) = ((M1 * M2) * M3) * ((M3 ~ ) * ((M2 ~ ) * (M1 ~ ))) by A8, A18, A11, A21, MATRIX_3:35
.= (((M1 * M2) * M3) * (M3 ~ )) * ((M2 ~ ) * (M1 ~ )) by A18, A16, A15, MATRIX_3:35
.= ((M1 * M2) * (M3 * (M3 ~ ))) * ((M2 ~ ) * (M1 ~ )) by A9, A6, A10, A16, MATRIX_3:35
.= ((M1 * M2) * (1. K,n)) * ((M2 ~ ) * (M1 ~ )) by A7, Def2
.= (M1 * M2) * ((M2 ~ ) * (M1 ~ )) by MATRIX_3:21
.= ((M1 * M2) * (M2 ~ )) * (M1 ~ ) by A10, A8, A11, A21, MATRIX_3:35
.= (M1 * (M2 * (M2 ~ ))) * (M1 ~ ) by A22, A12, A14, A21, MATRIX_3:35
.= (M1 * (1. K,n)) * (M1 ~ ) by A5, Def2
.= M1 * (M1 ~ ) by MATRIX_3:21
.= 1. K,n by A4, Def2 ;
then A24: ((M3 ~ ) * (M2 ~ )) * (M1 ~ ) is_reverse_of (M1 * M2) * M3 by A23, Def2;
then (M1 * M2) * M3 is invertible by Def3;
hence ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~ ) * (M2 ~ )) * (M1 ~ ) ) by A24, Def4; :: thesis: verum