let n be Nat; :: thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 holds
M1 is_congruent_Matrix_of M3
let K be Field; :: thesis: for M1, M2, M3 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 holds
M1 is_congruent_Matrix_of M3
let M1, M2, M3 be Matrix of n,K; :: thesis: ( M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 implies M1 is_congruent_Matrix_of M3 )
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: M2 is_congruent_Matrix_of M3 and
A3: n > 0 ; :: thesis: M1 is_congruent_Matrix_of M3
A4: ( len M2 = n & width M2 = n ) by MATRIX_0:24;
consider M4 being Matrix of n,K such that
A5: M4 is invertible and
A6: M1 = ((M4 @) * M2) * M4 by A1;
A7: len M4 = n by MATRIX_0:24;
consider M5 being Matrix of n,K such that
A8: M5 is invertible and
A9: M2 = ((M5 @) * M3) * M5 by A2;
A10: len M5 = n by MATRIX_0:24;
A11: ( len M3 = n & len (M5 @) = n ) by MATRIX_0:24;
A12: width M5 = n by MATRIX_0:24;
take M5 * M4 ; :: according to MATRIX_8:def 6 :: thesis: ( M5 * M4 is invertible & M1 = (((M5 * M4) @) * M3) * (M5 * M4) )
A13: ( len ((M5 @) * M3) = n & len (M5 * M4) = n ) by MATRIX_0:24;
A14: width (M4 @) = n by MATRIX_0:24;
A15: width (M5 @) = n by MATRIX_0:24;
A16: width ((M5 @) * M3) = n by MATRIX_0:24;
width M4 = n by MATRIX_0:24;
then (((M5 * M4) @) * M3) * (M5 * M4) = (((M4 @) * (M5 @)) * M3) * (M5 * M4) by A3, A7, A12, MATRIX_3:22
.= ((M4 @) * ((M5 @) * M3)) * (M5 * M4) by A14, A11, A15, MATRIX_3:33
.= (M4 @) * (((M5 @) * M3) * (M5 * M4)) by A14, A16, A13, MATRIX_3:33
.= (M4 @) * ((((M5 @) * M3) * M5) * M4) by A7, A10, A12, A16, MATRIX_3:33
.= M1 by A6, A9, A4, A7, A14, MATRIX_3:33 ;
hence ( M5 * M4 is invertible & M1 = (((M5 * M4) @) * M3) * (M5 * M4) ) by A5, A8, MATRIX_6:36; :: thesis: verum