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_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. (K,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. (K,n))) * M3 by A5

.= (M3 ~) * M3 by MATRIX_3:19

.= 1. (K,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. (K,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. (K,n))) * (M1 ~) by A5

.= M1 * (M1 ~) by MATRIX_3:19

.= 1. (K,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

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_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. (K,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. (K,n))) * M3 by A5

.= (M3 ~) * M3 by MATRIX_3:19

.= 1. (K,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. (K,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. (K,n))) * (M1 ~) by A5

.= M1 * (M1 ~) by MATRIX_3:19

.= 1. (K,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