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