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