let n be Nat; for K being Field
for M being Matrix of n,K
for perm being Element of Permutations n st perm <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) holds
(Path_product M) . perm = 0. K
let K be Field; for M being Matrix of n,K
for perm being Element of Permutations n st perm <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) holds
(Path_product M) . perm = 0. K
let M be Matrix of n,K; for perm being Element of Permutations n st perm <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) holds
(Path_product M) . perm = 0. K
let p be Element of Permutations n; ( p <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) implies (Path_product M) . p = 0. K )
assume that
A1:
p <> idseq n
and
A2:
( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K )
; (Path_product M) . p = 0. K
reconsider p9 = p as Permutation of (Seg n) by MATRIX_1:def 12;
set PP = Path_product M;
set PATH = Path_matrix (p,M);
now ex i being Nat st
( i in dom (Path_matrix (p,M)) & (Path_matrix (p,M)) . i = 0. K )per cases
( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K )
by A2;
suppose A3:
M is
lower_triangular Matrix of
n,
K
;
ex i being Nat st
( i in dom (Path_matrix (p,M)) & (Path_matrix (p,M)) . i = 0. K )A4:
rng p9 = Seg n
by FUNCT_2:def 3;
A5:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
consider i being
Nat such that A6:
i in Seg n
and A7:
p . i > i
by A1, Th4;
reconsider Pi =
p . i as
Nat ;
dom p9 = Seg n
by FUNCT_2:52;
then
p9 . i in Seg n
by A6, A4, FUNCT_1:def 3;
then
[i,Pi] in [:(Seg n),(Seg n):]
by A6, ZFMISC_1:87;
then A8:
M * (
i,
Pi)
= 0. K
by A3, A7, A5, MATRIX_1:def 9;
len (Path_matrix (p,M)) = n
by MATRIX_3:def 7;
then A9:
dom (Path_matrix (p,M)) = Seg n
by FINSEQ_1:def 3;
then
(Path_matrix (p,M)) . i = M * (
i,
Pi)
by A6, MATRIX_3:def 7;
hence
ex
i being
Nat st
(
i in dom (Path_matrix (p,M)) &
(Path_matrix (p,M)) . i = 0. K )
by A6, A9, A8;
verum end; suppose A10:
M is
upper_triangular Matrix of
n,
K
;
ex i being Nat st
( i in dom (Path_matrix (p,M)) & (Path_matrix (p,M)) . i = 0. K )A11:
rng p9 = Seg n
by FUNCT_2:def 3;
A12:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
consider i being
Nat such that A13:
i in Seg n
and A14:
p . i < i
by A1, Th4;
reconsider Pi =
p . i as
Nat ;
dom p9 = Seg n
by FUNCT_2:52;
then
p9 . i in Seg n
by A13, A11, FUNCT_1:def 3;
then
[i,Pi] in [:(Seg n),(Seg n):]
by A13, ZFMISC_1:87;
then A15:
M * (
i,
Pi)
= 0. K
by A10, A14, A12, MATRIX_1:def 8;
len (Path_matrix (p,M)) = n
by MATRIX_3:def 7;
then A16:
dom (Path_matrix (p,M)) = Seg n
by FINSEQ_1:def 3;
then
(Path_matrix (p,M)) . i = M * (
i,
Pi)
by A13, MATRIX_3:def 7;
hence
ex
i being
Nat st
(
i in dom (Path_matrix (p,M)) &
(Path_matrix (p,M)) . i = 0. K )
by A13, A16, A15;
verum end;
then
Product (Path_matrix (p,M)) = 0. K
by FVSUM_1:82;
then A17:
(Path_product M) . p = - ((0. K),p)
by MATRIX_3:def 8;
( - ((0. K),p) = 0. K or - ((0. K),p) = - (0. K) )
by MATRIX_1:def 16;
hence
(Path_product M) . p = 0. K
by A17, RLVECT_1:12; verum