let n be Nat; :: thesis: for R being Ring
for M1, M2 being Matrix of n,R st M1 is upper_triangular Matrix of n,R & M1 is lower_triangular Matrix of n,R holds
M1 is symmetric
let R be Ring; :: thesis: for M1, M2 being Matrix of n,R st M1 is upper_triangular Matrix of n,R & M1 is lower_triangular Matrix of n,R holds
M1 is symmetric
let M1, M2 be Matrix of n,R; :: thesis: ( M1 is upper_triangular Matrix of n,R & M1 is lower_triangular Matrix of n,R implies M1 is symmetric )
assume A1: ( M1 is upper_triangular Matrix of n,R & M1 is lower_triangular Matrix of n,R ) ; :: thesis: M1 is symmetric
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0: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_0: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_0: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. R & M1 * (j,i) = 0. R ) by A1, A3, A4, MATRIX_1:def 9, MATRIX_1:def 8;
hence (M1 @) * (i,j) = M1 * (i,j) by A4, MATRIX_0:def 6; :: thesis: verum

end;

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

then ( M1 * (i,j) = 0. R & M1 * (j,i) = 0. R ) by A1, A3, A4, MATRIX_1:def 8, MATRIX_1:def 9;
hence (M1 @) * (i,j) = M1 * (i,j) by A4, MATRIX_0:def 6; :: thesis: verum

end;

end;

end;

end;

end;

hence M1 is symmetric by MATRIX_0:27; :: thesis: verum