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

for i, j being Nat st [i,j] in Indices M1 holds

(M1 @) * (i,j) = M1 * (i,j)

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

for i, j being Nat st [i,j] in Indices M1 holds

(M1 @) * (i,j) = M1 * (i,j)

proof

hence
M1 is symmetric
by MATRIX_0:27; :: thesis: verum
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;

end;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 )
;

end;

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

end;