let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K holds
M1 is symmetric
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K holds
M1 is symmetric
let M1 be Matrix of n,K; :: thesis: ( M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K implies M1 is symmetric )
assume A1: ( M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K ) ; :: thesis: M1 is symmetric
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices M1 holds
(M1 @) * (i,j) = M1 * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies (M1 @) * (i,j) = M1 * (i,j) )
assume A3: [i,j] in Indices M1 ; :: thesis: (M1 @) * (i,j) = M1 * (i,j)
then [i,j] in [:(Seg n),(Seg n):] by MATRIX_1:24;
then ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
then A4: [j,i] in Indices M1 by A2, ZFMISC_1:87;

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: (M1 @) * (i,j) = M1 * (i,j)

hence (M1 @) * (i,j) = M1 * (i,j) by A4, MATRIX_1:def 6; :: thesis: verum

end;

suppose A5: i <> j ; :: thesis: (M1 @) * (i,j) = M1 * (i,j)

per cases ( i < j or i > j ) by A5, XXREAL_0:1;

suppose i < j ; :: thesis: (M1 @) * (i,j) = M1 * (i,j)

then ( M1 * (i,j) = 0. K & M1 * (j,i) = 0. K ) by A1, A3, A4, MATRIX_2:def 3, MATRIX_2:def 4;
hence (M1 @) * (i,j) = M1 * (i,j) by A4, MATRIX_1:def 6; :: thesis: verum

end;

suppose i > j ; :: thesis: (M1 @) * (i,j) = M1 * (i,j)

then ( M1 * (i,j) = 0. K & M1 * (j,i) = 0. K ) by A1, A3, A4, MATRIX_2:def 3, MATRIX_2:def 4;
hence (M1 @) * (i,j) = M1 * (i,j) by A4, MATRIX_1:def 6; :: thesis: verum

end;

end;

end;

end;

end;

then M1 @ = M1 by MATRIX_1:27;
hence M1 is symmetric by Def5; :: thesis: verum