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
M2 is_congruent_Matrix_of M1
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M2 is_congruent_Matrix_of M1
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is_congruent_Matrix_of M2 & n > 0 implies M2 is_congruent_Matrix_of M1 )
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: n > 0 ; :: thesis: M2 is_congruent_Matrix_of M1
consider M being Matrix of n,K such that
A3: M is invertible and
A4: M1 = ((M @ ) * M2) * M by A1, Def6;
A5: M ~ is_reverse_of M by A3, MATRIX_6:def 4;
take M ~ ; :: according to MATRIX_8:def 6 :: thesis: ( M ~ is invertible & M2 = (((M ~ ) @ ) * M1) * (M ~ ) )
A6: width (M ~ ) = n by MATRIX_1:25;
A7: ( len (M @ ) = n & width (M @ ) = n ) by MATRIX_1:25;
A8: width M = n by MATRIX_1:25;
A9: len (M ~ ) = n by MATRIX_1:25;
( len M = n & width ((M @ ) * M2) = n ) by MATRIX_1:25;
then A10: M1 * (M ~ ) = ((M @ ) * M2) * (M * (M ~ )) by A4, A8, A9, MATRIX_3:35
.= ((M @ ) * M2) * (1. K,n) by A5, MATRIX_6:def 2
.= (M @ ) * M2 by MATRIX_3:21 ;
A11: len M2 = n by MATRIX_1:25;
A12: width ((M ~ ) @ ) = n by MATRIX_1:25;
( len M1 = n & width M1 = n ) by MATRIX_1:25;
then (((M ~ ) @ ) * M1) * (M ~ ) = ((M ~ ) @ ) * (M1 * (M ~ )) by A9, A12, MATRIX_3:35
.= (((M ~ ) @ ) * (M @ )) * M2 by A7, A11, A12, A10, MATRIX_3:35
.= ((M * (M ~ )) @ ) * M2 by A2, A8, A9, A6, MATRIX_3:24
.= ((1. K,n) @ ) * M2 by A5, MATRIX_6:def 2
.= (1. K,n) * M2 by MATRIX_6:10
.= M2 by MATRIX_3:20 ;
hence ( M ~ is invertible & M2 = (((M ~ ) @ ) * M1) * (M ~ ) ) by A3, MATRIX_6:16; :: thesis: verum