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: M2 ~ is_reverse_of M2 by A2, Def4;

A4: M1 ~ is_reverse_of M1 by A1, Def4;

A5: len (M2 ~) = n by MATRIX_0:24;

A6: width (M1 ~) = n by MATRIX_0:24;

A7: len M1 = n by MATRIX_0:24;

A8: width M2 = n by MATRIX_0:24;

A9: ( width M1 = n & len M2 = n ) by MATRIX_0:24;

A10: ( width (M2 ~) = n & len (M1 ~) = n ) by MATRIX_0:24;

width (M1 * M2) = n by MATRIX_0:24;

then A11: (M1 * M2) * ((M2 ~) * (M1 ~)) = ((M1 * M2) * (M2 ~)) * (M1 ~) by A5, A10, MATRIX_3:33

.= (M1 * (M2 * (M2 ~))) * (M1 ~) by A9, A8, A5, MATRIX_3:33

.= (M1 * (1. (K,n))) * (M1 ~) by A3

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

.= 1. (K,n) by A4 ;

width ((M2 ~) * (M1 ~)) = n by MATRIX_0:24;

then ((M2 ~) * (M1 ~)) * (M1 * M2) = (((M2 ~) * (M1 ~)) * M1) * M2 by A9, A7, MATRIX_3:33

.= ((M2 ~) * ((M1 ~) * M1)) * M2 by A7, A6, A10, MATRIX_3:33

.= ((M2 ~) * (1. (K,n))) * M2 by A4

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

.= 1. (K,n) by A3 ;

then A12: (M2 ~) * (M1 ~) is_reverse_of M1 * M2 by A11;

then M1 * M2 is invertible ;

hence ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) by A12, Def4; :: thesis: verum

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: M2 ~ is_reverse_of M2 by A2, Def4;

A4: M1 ~ is_reverse_of M1 by A1, Def4;

A5: len (M2 ~) = n by MATRIX_0:24;

A6: width (M1 ~) = n by MATRIX_0:24;

A7: len M1 = n by MATRIX_0:24;

A8: width M2 = n by MATRIX_0:24;

A9: ( width M1 = n & len M2 = n ) by MATRIX_0:24;

A10: ( width (M2 ~) = n & len (M1 ~) = n ) by MATRIX_0:24;

width (M1 * M2) = n by MATRIX_0:24;

then A11: (M1 * M2) * ((M2 ~) * (M1 ~)) = ((M1 * M2) * (M2 ~)) * (M1 ~) by A5, A10, MATRIX_3:33

.= (M1 * (M2 * (M2 ~))) * (M1 ~) by A9, A8, A5, MATRIX_3:33

.= (M1 * (1. (K,n))) * (M1 ~) by A3

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

.= 1. (K,n) by A4 ;

width ((M2 ~) * (M1 ~)) = n by MATRIX_0:24;

then ((M2 ~) * (M1 ~)) * (M1 * M2) = (((M2 ~) * (M1 ~)) * M1) * M2 by A9, A7, MATRIX_3:33

.= ((M2 ~) * ((M1 ~) * M1)) * M2 by A7, A6, A10, MATRIX_3:33

.= ((M2 ~) * (1. (K,n))) * M2 by A4

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

.= 1. (K,n) by A3 ;

then A12: (M2 ~) * (M1 ~) is_reverse_of M1 * M2 by A11;

then M1 * M2 is invertible ;

hence ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) by A12, Def4; :: thesis: verum