let n be Nat; for K being Field
for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K ) holds
M * R is upper_triangular Matrix of n,K
let K be Field; for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K ) holds
M * R is upper_triangular Matrix of n,K
let M be Matrix of n,K; for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K ) holds
M * R is upper_triangular Matrix of n,K
let R be Permutation of (Seg n); ( R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K ) implies M * R is upper_triangular Matrix of n,K )
assume that
A1:
R = Rev (idseq n)
and
A2:
for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K
; M * R is upper_triangular Matrix of n,K
set I = idseq n;
set MR = M * R;
now for i, j being Nat st [i,j] in Indices (M * R) & i > j holds
(M * R) * (i,j) = 0. Klet i,
j be
Nat;
( [i,j] in Indices (M * R) & i > j implies (M * R) * (i,j) = 0. K )assume that A3:
[i,j] in Indices (M * R)
and A4:
i > j
;
(M * R) * (i,j) = 0. Kreconsider i9 =
i as
Element of
NAT by ORDINAL1:def 12;
A5:
Indices (M * R) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A6:
i in Seg n
by A3, ZFMISC_1:87;
then
i <= n
by FINSEQ_1:1;
then reconsider ni =
(n - i9) + 1 as
Element of
NAT by FINSEQ_5:1;
A7:
ni in Seg n
by A6, FINSEQ_5:2;
then A8:
(idseq n) . ni = ni
by FUNCT_1:17;
(n + 1) - i < (n + 1) - j
by A4, XREAL_1:15;
then
ni + j < ((n + 1) - j) + j
by XREAL_1:8;
then A9:
ni + j <= n
by NAT_1:13;
j in Seg n
by A3, A5, ZFMISC_1:87;
then A10:
M * (
ni,
j)
= 0. K
by A2, A7, A9;
A11:
len (idseq n) = n
by CARD_1:def 7;
A12:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
dom (idseq n) = Seg (len (idseq n))
by FINSEQ_1:def 3;
then
R . i = (idseq n) . ni
by A1, A6, A11, FINSEQ_5:58;
hence
(M * R) * (
i,
j)
= 0. K
by A3, A5, A12, A8, A10, MATRIX11:def 4;
verum end;
hence
M * R is upper_triangular Matrix of n,K
by MATRIX_1:def 8; verum