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;

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_0:24;

A7: ( len (M @) = n & width (M @) = n ) by MATRIX_0:24;

A8: width M = n by MATRIX_0:24;

A9: len (M ~) = n by MATRIX_0:24;

( len M = n & width ((M @) * M2) = n ) by MATRIX_0:24;

then A10: M1 * (M ~) = ((M @) * M2) * (M * (M ~)) by A4, A8, A9, MATRIX_3:33

.= ((M @) * M2) * (1. (K,n)) by A5, MATRIX_6:def 2

.= (M @) * M2 by MATRIX_3:19 ;

A11: len M2 = n by MATRIX_0:24;

A12: width ((M ~) @) = n by MATRIX_0:24;

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

then (((M ~) @) * M1) * (M ~) = ((M ~) @) * (M1 * (M ~)) by A9, A12, MATRIX_3:33

.= (((M ~) @) * (M @)) * M2 by A7, A11, A12, A10, MATRIX_3:33

.= ((M * (M ~)) @) * M2 by A2, A8, A9, A6, MATRIX_3:22

.= ((1. (K,n)) @) * M2 by A5, MATRIX_6:def 2

.= (1. (K,n)) * M2 by MATRIX_6:10

.= M2 by MATRIX_3:18 ;

hence ( M ~ is invertible & M2 = (((M ~) @) * M1) * (M ~) ) by A3; :: thesis: verum

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;

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_0:24;

A7: ( len (M @) = n & width (M @) = n ) by MATRIX_0:24;

A8: width M = n by MATRIX_0:24;

A9: len (M ~) = n by MATRIX_0:24;

( len M = n & width ((M @) * M2) = n ) by MATRIX_0:24;

then A10: M1 * (M ~) = ((M @) * M2) * (M * (M ~)) by A4, A8, A9, MATRIX_3:33

.= ((M @) * M2) * (1. (K,n)) by A5, MATRIX_6:def 2

.= (M @) * M2 by MATRIX_3:19 ;

A11: len M2 = n by MATRIX_0:24;

A12: width ((M ~) @) = n by MATRIX_0:24;

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

then (((M ~) @) * M1) * (M ~) = ((M ~) @) * (M1 * (M ~)) by A9, A12, MATRIX_3:33

.= (((M ~) @) * (M @)) * M2 by A7, A11, A12, A10, MATRIX_3:33

.= ((M * (M ~)) @) * M2 by A2, A8, A9, A6, MATRIX_3:22

.= ((1. (K,n)) @) * M2 by A5, MATRIX_6:def 2

.= (1. (K,n)) * M2 by MATRIX_6:10

.= M2 by MATRIX_3:18 ;

hence ( M ~ is invertible & M2 = (((M ~) @) * M1) * (M ~) ) by A3; :: thesis: verum