let m', n' be Nat; :: thesis: for K being Field
for M' being Matrix of the carrier of K,n',
for P, Q being finite without_zero Subset of
for i being Nat
for j0 being non zero Nat st j0 in Seg n' & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M' holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) )
let K be Field; :: thesis: for M' being Matrix of the carrier of K,n',
for P, Q being finite without_zero Subset of
for i being Nat
for j0 being non zero Nat st j0 in Seg n' & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M' holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) )
let M' be Matrix of the carrier of K,n',; :: thesis: for P, Q being finite without_zero Subset of
for i being Nat
for j0 being non zero Nat st j0 in Seg n' & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M' holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) )
let P, Q be finite without_zero Subset of ; :: thesis: for i being Nat
for j0 being non zero Nat st j0 in Seg n' & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M' holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) )
let i be Nat; :: thesis: for j0 being non zero Nat st j0 in Seg n' & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M' holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) )
let j0 be non zero Nat; :: thesis: ( j0 in Seg n' & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M' implies ( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) ) )
assume that
A1: j0 in Seg n' and
A2: i in P and
A3: not j0 in P and
A4: card P = card Q and
A5: [:P,Q:] c= Indices M' ; :: thesis: ( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) )
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:65;
not j0 in P \ {i} by A3, XBOOLE_0:def 5;
hence A9: card ((P \ {i}) \/ {j0}) = C + 1 by A8, CARD_2:54
.= card P ;
:: thesis: ( [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) )
then reconsider SPij = Sgm ((P \ {i}) \/ {j0}), SQ' = Sgm Q as Element of (card P) -tuples_on NAT by A4;
A10: Segm M',SPij,SQ' = Segm M',((P \ {i}) \/ {j0}),Q by A4, A9
.= EqSegm M',((P \ {i}) \/ {j0}),Q by A4, A9, Def3 ;
P c= Seg (len M') by A4, A5, Th67;
then A11: P \ {i} c= Seg (len M') by A6, XBOOLE_1:1;
n' = len M' by MATRIX_1:def 3;
then {j0} c= Seg (len M') by A1, ZFMISC_1:37;
then A12: (P \ {i}) \/ {j0} c= Seg (len M') 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 M',i,(Line M',j0)),(Sgm P),(Sgm Q) = Segm M',PT,(Sgm Q) by A2, A5, A13, Th39;
Q c= Seg (width M') by A4, A5, Th67;
hence [:((P \ {i}) \/ {j0}),Q:] c= Indices M' by A4, A9, A12, Th67; :: thesis: ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) )
EqSegm (RLine M',i,(Line M',j0)),P,Q = Segm (RLine M',i,(Line M',j0)),P,Q by A4, Def3
.= Segm M',PT,SQ' by A4, A15 ;
hence ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) ) by A9, A7, A13, A14, A10, Th36; :: thesis: verum