let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K holds
( M is Lower_Triangular_Matrix of n,K iff M @ is Upper_Triangular_Matrix of n,K )
let K be Field; :: thesis: for M being Matrix of n,K holds
( M is Lower_Triangular_Matrix of n,K iff M @ is Upper_Triangular_Matrix of n,K )
let M be Matrix of n,K; :: thesis: ( M is Lower_Triangular_Matrix of n,K iff M @ is Upper_Triangular_Matrix of n,K )
thus ( M is Lower_Triangular_Matrix of n,K implies M @ is Upper_Triangular_Matrix of n,K ) :: thesis: ( M @ is Upper_Triangular_Matrix of n,K implies M is Lower_Triangular_Matrix of n,K )

proof

assume A1: M is Lower_Triangular_Matrix of n,K ; :: thesis: M @ is Upper_Triangular_Matrix of n,K

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (M @) & i > j implies (M @) * (i,j) = 0. K )
assume that
A2: [i,j] in Indices (M @) and
A3: i > j ; :: thesis: (M @) * (i,j) = 0. K
A4: [j,i] in Indices M by A2, MATRIX_1:def 7;
then M * (j,i) = 0. K by A1, A3, MATRIX_2:def 4;
hence (M @) * (i,j) = 0. K by A4, MATRIX_1:def 7; :: thesis: verum

end;

hence M @ is Upper_Triangular_Matrix of n,K by MATRIX_2:def 3; :: thesis: verum

end;

assume A5: M @ is Upper_Triangular_Matrix of n,K ; :: thesis: M is Lower_Triangular_Matrix of n,K

now

let i, j be Nat; :: thesis: ( [i,j] in Indices M & i < j implies M * (i,j) = 0. K )
assume that
A6: [i,j] in Indices M and
A7: i < j ; :: thesis: M * (i,j) = 0. K
[j,i] in Indices (M @) by A6, MATRIX_1:def 7;
then (M @) * (j,i) = 0. K by A5, A7, MATRIX_2:def 3;
hence M * (i,j) = 0. K by A6, MATRIX_1:def 7; :: thesis: verum

end;

hence M is Lower_Triangular_Matrix of n,K by MATRIX_2:def 4; :: thesis: verum