let K be Field; for M being diagonal Matrix of K
for P being finite without_zero Subset of NAT st [:P,P:] c= Indices M holds
Segm (M,P,P) is V185(K)
let M be diagonal Matrix of K; for P being finite without_zero Subset of NAT st [:P,P:] c= Indices M holds
Segm (M,P,P) is V185(K)
let P be finite without_zero Subset of NAT; ( [:P,P:] c= Indices M implies Segm (M,P,P) is V185(K) )
assume A1:
[:P,P:] c= Indices M
; Segm (M,P,P) is V185(K)
set S = Segm (M,P,P);
set SP = Sgm P;
let i, j be Nat; MATRIX_7:def 2 ( not i in Seg (card P) or not j in Seg (card P) or i = j or (Segm (M,P,P)) * (i,j) = 0. K )
assume that
A2:
i in Seg (card P)
and
A3:
j in Seg (card P)
and
A4:
i <> j
; (Segm (M,P,P)) * (i,j) = 0. K
A5:
P c= Seg (len M)
by A1, A2, Th67;
then A6:
Sgm P is one-to-one
by FINSEQ_3:92;
[i,j] in [:(Seg (card P)),(Seg (card P)):]
by A2, A3, ZFMISC_1:87;
then A7:
[i,j] in Indices (Segm (M,P,P))
by MATRIX_0:24;
dom (Sgm P) = Seg (card P)
by A5, FINSEQ_3:40;
then A8:
(Sgm P) . i <> (Sgm P) . j
by A2, A3, A4, A6;
rng (Sgm P) = P
by A5, FINSEQ_1:def 13;
then A9:
[((Sgm P) . i),((Sgm P) . j)] in Indices M
by A1, A7, Th17;
(Segm (M,P,P)) * (i,j) = M * (((Sgm P) . i),((Sgm P) . j))
by A7, Def1;
hence
(Segm (M,P,P)) * (i,j) = 0. K
by A9, A8, MATRIX_1:def 6; verum