let K be Field; :: thesis: 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 diagonal
let M be diagonal Matrix of K; :: thesis: for P being finite without_zero Subset of NAT st [:P,P:] c= Indices M holds
Segm M,P,P is diagonal
let P be finite without_zero Subset of NAT ; :: thesis: ( [:P,P:] c= Indices M implies Segm M,P,P is diagonal )
assume A1: [:P,P:] c= Indices M ; :: thesis: Segm M,P,P is diagonal
set S = Segm M,P,P;
set SP = Sgm P;
let i, j be Element of NAT ; :: according to MATRIX_7:def 2 :: thesis: ( 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 ; :: thesis: (Segm M,P,P) * i,j = 0. K
A5: P c= Seg (len M) by A1, A2, Th67;
then A6: Sgm P is without_repeated_line by FINSEQ_3:99;
[i,j] in [:(Seg (card P)),(Seg (card P)):] by A2, A3, ZFMISC_1:106;
then A7: [i,j] in Indices (Segm M,P,P) by MATRIX_1:25;
dom (Sgm P) = Seg (card P) by A5, FINSEQ_3:45;
then A8: (Sgm P) . i <> (Sgm P) . j by A2, A3, A4, A6, FUNCT_1:def 8;
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 15; :: thesis: verum