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)
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. K & M1 * (j,i) = 0. K ) 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. K & M1 * (j,i) = 0. K ) 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