let K be Field; :: thesis: for M being Matrix of K
for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & Q c= Q1 & Det (EqSegm M,P1,Q1) <> 0. K holds
ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K )
let M be Matrix of K; :: thesis: for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & Q c= Q1 & Det (EqSegm M,P1,Q1) <> 0. K holds
ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K )
let P1, Q, Q1 be finite without_zero Subset of NAT ; :: thesis: ( card P1 = card Q1 & Q c= Q1 & Det (EqSegm M,P1,Q1) <> 0. K implies ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K ) )
assume that
A1:
( card P1 = card Q1 & Q c= Q1 )
and
A2:
Det (EqSegm M,P1,Q1) <> 0. K
; :: thesis: ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K )
defpred S1[ Nat] means for Q being finite without_zero Subset of NAT st Q c= Q1 & card Q = $1 holds
ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K );
A3:
S1[ card Q1]
A4:
for k being Element of NAT st k < card Q1 & S1[k + 1] holds
S1[k]
proof
let k be
Element of
NAT ;
:: thesis: ( k < card Q1 & S1[k + 1] implies S1[k] )
assume A5:
(
k < card Q1 &
S1[
k + 1] )
;
:: thesis: S1[k]
let Q be
finite without_zero Subset of
NAT ;
:: thesis: ( Q c= Q1 & card Q = k implies ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K ) )
assume A6:
(
Q c= Q1 &
card Q = k )
;
:: thesis: ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K )
Q c< Q1
by A5, A6, XBOOLE_0:def 8;
then
Q1 \ Q <> {}
by XBOOLE_1:105;
then consider x being
set such that A7:
x in Q1 \ Q
by XBOOLE_0:def 1;
reconsider x =
x as non
zero Element of
NAT by A7;
reconsider Qx =
Q \/ {x} as
finite without_zero Subset of
NAT ;
(
x in Q1 & not
0 in Q1 )
by A7, XBOOLE_0:def 5;
then A8:
( not
x in Q &
{x} c= Q1 )
by A7, XBOOLE_0:def 5, ZFMISC_1:37;
then A9:
(
card Qx = k + 1 &
Qx c= Q1 )
by A6, CARD_2:54, XBOOLE_1:8;
then consider P2 being
finite without_zero Subset of
NAT such that A10:
(
P2 c= P1 &
card Qx = card P2 &
Det (EqSegm M,P2,Qx) <> 0. K )
by A5;
set E =
EqSegm M,
P2,
Qx;
consider n being
Nat such that A11:
Qx c= Seg n
by Th43;
x in {x}
by TARSKI:def 1;
then
(
rng (Sgm Qx) = Qx &
dom (Sgm Qx) = Seg (card Qx) &
x in Qx )
by A11, FINSEQ_1:def 13, FINSEQ_3:45, XBOOLE_0:def 3;
then consider j being
set such that A12:
(
j in Seg (card Qx) &
(Sgm Qx) . j = x )
by FUNCT_1:def 5;
reconsider j =
j as
Element of
NAT by A12;
consider i being
Nat such that A13:
(
i in Seg (card Qx) &
Det (Delete (EqSegm M,P2,Qx),i,j) <> 0. K )
by A10, A12, Lm4;
take P =
P2 \ {((Sgm P2) . i)};
:: thesis: ( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K )
A14:
(
Qx \ {x} = Q &
P c= P2 &
(k + 1) -' 1
= (k + 1) - 1 )
by A8, XBOOLE_1:36, XREAL_0:def 2, ZFMISC_1:141;
then
card P = card Q
by A10, A12, A13, Th64;
hence
(
P c= P1 &
card P = card Q &
Det (EqSegm M,P,Q) <> 0. K )
by A6, A9, A10, A12, A13, A14, Th64, XBOOLE_1:1;
:: thesis: verum
end;
A15:
for k being Element of NAT st k <= card Q1 holds
S1[k]
from TRIANG_1:sch 1(A3, A4);
card Q <= card Q1
by A1, NAT_1:44;
hence
ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K )
by A1, A15; :: thesis: verum