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 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
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 FINSEQ_3:40;
then A8: (Sgm P) . i <> (Sgm P) . j by A2, A3, A4, A6;
rng (Sgm P) = P by FINSEQ_1:def 14;
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; :: thesis: verum