let m9, n9 be Nat; :: thesis:
let K be Field; :: thesis:
let M9 be Matrix of n9,m9,K; :: thesis:
let P, Q be finite without_zero Subset of NAT; :: thesis:
let i be Nat; :: thesis:
let j0 be non zero Nat; :: thesis:
assume that
A1: j0 in Seg n9 and
A2: i in P and
A3: not j0 in P and
A4: card P = card Q and
A5: [:P,Q:] c= Indices M9 ; :: thesis:
set Pi = P \ {i};
A6: P \ {i} c= P by XBOOLE_1:36;
set SQ = Sgm Q;
set Pij = (P \ {i}) \/ {j0};
set SPij = Sgm ((P \ {i}) \/ {j0});
ex k being Nat st (P \ {i}) \/ {j0} c= Seg k by Th43;
then A7: rng (Sgm ((P \ {i}) \/ {j0})) = (P \ {i}) \/ {j0} by FINSEQ_1:def 13;
card P > 0 by A2;
then reconsider C = (card P) - 1 as Element of NAT by NAT_1:20;
card P = C + 1 ;
then A8: card (P \ {i}) = C by A2, STIRL2_1:55;
not j0 in P \ {i} by A3, XBOOLE_0:def 5;
hence A9: card ((P \ {i}) \/ {j0}) = C + 1 by A8, CARD_2:41
.= card P ;
:: thesis:
then reconsider SPij = Sgm ((P \ {i}) \/ {j0}), SQ9 = Sgm Q as Element of (card P) -tuples_on NAT by A4;
A10: Segm (M9,SPij,SQ9) = Segm (M9,((P \ {i}) \/ {j0}),Q) by A4, A9
.= EqSegm (M9,((P \ {i}) \/ {j0}),Q) by A4, A9, Def3 ;
P c= Seg (len M9) by A4, A5, Th67;
then A11: P \ {i} c= Seg (len M9) by A6;
n9 = len M9 by MATRIX_0:def 2;
then {j0} c= Seg (len M9) by A1, ZFMISC_1:31;
then A12: (P \ {i}) \/ {j0} c= Seg (len M9) by A11, XBOOLE_1:8;
set SP = Sgm P;
ex m being Nat st Q c= Seg m by Th43;
then A13: rng (Sgm Q) = Q by FINSEQ_1:def 13;
ex n being Nat st P c= Seg n by Th43;
then rng (Sgm P) = P by FINSEQ_1:def 13;
then consider PT being Element of (card P) -tuples_on NAT such that
A14: rng PT = (P \ {i}) \/ {j0} and
A15: Segm ((RLine (M9,i,(Line (M9,j0)))),(Sgm P),(Sgm Q)) = Segm (M9,PT,(Sgm Q)) by A2, A5, A13, Th39;
Q c= Seg (width M9) by A4, A5, Th67;
hence [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 by A4, A9, A12, Th67; :: thesis:
EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q) = Segm ((RLine (M9,i,(Line (M9,j0)))),P,Q) by A4, Def3
.= Segm (M9,PT,SQ9) by A4, A15 ;
hence ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) by A9, A7, A13, A14, A10, Th36; :: thesis: