let n be Nat; :: thesis: for R being Ring
for M1, M2, M3 being Matrix of n,R st M1 is invertible & M2 is invertible & M3 is invertible holds
( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) )
let R be Ring; :: thesis: for M1, M2, M3 being Matrix of n,R 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,R; :: 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_0:24;
A7: M3 ~ is_reverse_of M3 by A3, Def4;
A8: width (M2 ~) = n by MATRIX_0:24;
A9: width M3 = n by MATRIX_0:24;
A10: width (M1 * M2) = n by MATRIX_0:24;
A11: len (M1 ~) = n by MATRIX_0:24;
set M5 = ((M3 ~) * (M2 ~)) * (M1 ~);
set M4 = (M1 * M2) * M3;
A12: width M2 = n by MATRIX_0:24;
A13: ( len (M2 * M3) = n & width (((M3 ~) * (M2 ~)) * (M1 ~)) = n ) by MATRIX_0:24;
A14: len M2 = n by MATRIX_0:24;
A15: ( width ((M1 * M2) * M3) = n & len ((M2 ~) * (M1 ~)) = n ) by MATRIX_0:24;
A16: len (M3 ~) = n by MATRIX_0:24;
A17: width ((M3 ~) * (M2 ~)) = n by MATRIX_0:24;
A18: width (M3 ~) = n by MATRIX_0:24;
A19: width (M1 ~) = n by MATRIX_0:24;
A20: len M1 = n by MATRIX_0:24;
A21: len (M2 ~) = n by MATRIX_0:24;
A22: width M1 = n by MATRIX_0:24;
then A23: (((M3 ~) * (M2 ~)) * (M1 ~)) * ((M1 * M2) * M3) = (((M3 ~) * (M2 ~)) * (M1 ~)) * (M1 * (M2 * M3)) by A12, A14, A6, MATRIX_3:33
.= ((((M3 ~) * (M2 ~)) * (M1 ~)) * M1) * (M2 * M3) by A22, A20, A13, MATRIX_3:33
.= (((M3 ~) * (M2 ~)) * ((M1 ~) * M1)) * (M2 * M3) by A20, A19, A11, A17, MATRIX_3:33
.= (((M3 ~) * (M2 ~)) * (1. (R,n))) * (M2 * M3) by A4
.= ((M3 ~) * (M2 ~)) * (M2 * M3) by MATRIX_3:19
.= (((M3 ~) * (M2 ~)) * M2) * M3 by A12, A14, A6, A17, MATRIX_3:33
.= ((M3 ~) * ((M2 ~) * M2)) * M3 by A14, A8, A18, A21, MATRIX_3:33
.= ((M3 ~) * (1. (R,n))) * M3 by A5
.= (M3 ~) * M3 by MATRIX_3:19
.= 1. (R,n) by A7 ;
((M1 * M2) * M3) * (((M3 ~) * (M2 ~)) * (M1 ~)) = ((M1 * M2) * M3) * ((M3 ~) * ((M2 ~) * (M1 ~))) by A8, A18, A11, A21, MATRIX_3:33
.= (((M1 * M2) * M3) * (M3 ~)) * ((M2 ~) * (M1 ~)) by A18, A16, A15, MATRIX_3:33
.= ((M1 * M2) * (M3 * (M3 ~))) * ((M2 ~) * (M1 ~)) by A9, A6, A10, A16, MATRIX_3:33
.= ((M1 * M2) * (1. (R,n))) * ((M2 ~) * (M1 ~)) by A7
.= (M1 * M2) * ((M2 ~) * (M1 ~)) by MATRIX_3:19
.= ((M1 * M2) * (M2 ~)) * (M1 ~) by A10, A8, A11, A21, MATRIX_3:33
.= (M1 * (M2 * (M2 ~))) * (M1 ~) by A22, A12, A14, A21, MATRIX_3:33
.= (M1 * (1. (R,n))) * (M1 ~) by A5
.= M1 * (M1 ~) by MATRIX_3:19
.= 1. (R,n) by A4 ;
then A24: ((M3 ~) * (M2 ~)) * (M1 ~) is_reverse_of (M1 * M2) * M3 by A23;
then (M1 * M2) * M3 is invertible ;
hence ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) ) by A24, Def4; :: thesis: verum