let k be Nat; for P being INT -valued Polynomial of (k + 1),F_Real
for a being Integer
for n being Nat
for i1, i2 being Element of n st k + 1 <= n & k in i2 holds
{ p where p is b3 -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)
let P be INT -valued Polynomial of (k + 1),F_Real; for a being Integer
for n being Nat
for i1, i2 being Element of n st k + 1 <= n & k in i2 holds
{ p where p is b2 -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)
let a be Integer; for n being Nat
for i1, i2 being Element of n st k + 1 <= n & k in i2 holds
{ p where p is b1 -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)
let n be Nat; for i1, i2 being Element of n st k + 1 <= n & k in i2 holds
{ p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2 be Element of n; ( k + 1 <= n & k in i2 implies { p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) )
assume A1:
( k + 1 <= n & k in i2 )
; { p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)
set k1 = k + 1;
dom (id k) = k
;
then reconsider Idk = id k as XFinSequence by AFINSQ_1:5;
A2:
len Idk = k
;
A3:
rng (id k) = Segm k
;
reconsider Idk = Idk as k -element XFinSequence of NAT by A2, CARD_1:def 7;
reconsider nk = n - (k + 1) as Nat by A1, NAT_1:21;
set f = <%i2%> ^ Idk;
A4:
rng <%i2%> = {i2}
by AFINSQ_1:33;
{i2} misses k
by A1, ZFMISC_1:50;
then
rng <%i2%> misses rng Idk
by AFINSQ_1:33;
then A6:
<%i2%> ^ Idk is one-to-one
by CARD_FIN:52;
set R = rng (<%i2%> ^ Idk);
A7:
len (<%i2%> ^ Idk) = k + 1
by CARD_1:def 7;
A8:
card (dom (<%i2%> ^ Idk)) = k + 1
by CARD_1:def 7;
A:
k < n
by A1, NAT_1:13;
then A9:
Segm k c= Segm n
by NAT_1:39;
i2 in n
by A1, SUBSET_1:def 1;
then
{i2} c= n
by ZFMISC_1:31;
then
k \/ {i2} c= n
by A9, XBOOLE_1:8;
then A10:
rng (<%i2%> ^ Idk) c= n
by AFINSQ_1:26, A4, A3;
then
card (n \ (rng (<%i2%> ^ Idk))) = (card n) - (card (rng (<%i2%> ^ Idk)))
by CARD_2:44;
then A11:
card (n \ (rng (<%i2%> ^ Idk))) = nk
by A8, A6, CARD_1:70;
A12:
Segm (k + 1) c= Segm n
by A1, NAT_1:39;
then card (n \ (k + 1)) =
(card n) - (card (k + 1))
by CARD_2:44
.=
nk
;
then consider g being Function such that
A13:
( g is one-to-one & dom g = n \ (k + 1) & rng g = n \ (rng (<%i2%> ^ Idk)) )
by A11, CARD_1:5, WELLORD2:def 4;
A14:
( rng (<%i2%> ^ Idk) misses rng g & dom (<%i2%> ^ Idk) misses dom g )
by A7, A13, XBOOLE_1:79;
then A15:
(<%i2%> ^ Idk) +* g is one-to-one
by A6, A13, FUNCT_4:92;
A16: dom ((<%i2%> ^ Idk) +* g) =
(k + 1) \/ (n \ (k + 1))
by A7, A13, FUNCT_4:def 1
.=
(k + 1) \/ n
by XBOOLE_1:39
.=
n
by A12, XBOOLE_1:12
;
A17: rng ((<%i2%> ^ Idk) +* g) =
(rng (<%i2%> ^ Idk)) \/ (rng g)
by A14, NECKLACE:6
.=
n \/ (rng (<%i2%> ^ Idk))
by A13, XBOOLE_1:39
.=
n
by A10, XBOOLE_1:12
;
then reconsider fg = (<%i2%> ^ Idk) +* g as Function of n,n by A16, FUNCT_2:2;
card n = card n
;
then
fg is onto
by A15, FINSEQ_4:63;
then reconsider fg = fg as Permutation of n by A15;
defpred S1[ XFinSequence of NAT ] means for q being k + 1 -element XFinSequence of NAT st q = ($1 * fg) | (k + 1) holds
a * ($1 . i1) = eval (P,(@ q));
defpred S2[ XFinSequence of NAT ] means for q being k + 1 -element XFinSequence of NAT st q = <%($1 . i2)%> ^ ($1 | k) holds
a * ($1 . i1) = eval (P,(@ q));
A18:
for p being n -element XFinSequence of NAT holds
( S1[p] iff S2[p] )
proof
let p be
n -element XFinSequence of
NAT ;
( S1[p] iff S2[p] )
A19:
len p = n
by CARD_1:def 7;
then
dom (p * fg) = n
by A17, A16, RELAT_1:27;
then reconsider pfg =
p * fg as
XFinSequence by AFINSQ_1:5;
set I =
<%(p . i2)%>;
len pfg = n
by A19, A17, A16, RELAT_1:27;
then A20:
len (pfg | (k + 1)) = k + 1
by A1, AFINSQ_1:54;
A21:
(
len (p | k) = k &
len <%(p . i2)%> = 1 )
by AFINSQ_1:11, A, A19, CARD_1:def 7;
then A22:
len (<%(p . i2)%> ^ (p | k)) = k + 1
by AFINSQ_1:17;
for
i being
Nat st
i in dom (<%(p . i2)%> ^ (p | k)) holds
(<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i
proof
let i be
Nat;
( i in dom (<%(p . i2)%> ^ (p | k)) implies (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i )
assume A23:
i in dom (<%(p . i2)%> ^ (p | k))
;
(<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i
then A24:
(
i in dom pfg &
i in k + 1 &
(pfg | (k + 1)) . i = pfg . i )
by RELAT_1:57, FUNCT_1:47, A20, A22;
then A25:
(
pfg . i = p . (fg . i) & not
i in dom g )
by FUNCT_1:12, A13, XBOOLE_1:79, XBOOLE_0:3;
then A26:
fg . i = (<%i2%> ^ Idk) . i
by FUNCT_4:11;
A27:
len <%i2%> = 1
by CARD_1:def 7;
per cases
( i in dom <%(p . i2)%> or ex j being Nat st
( j in dom (p | k) & i = (len <%(p . i2)%>) + j ) )
by A23, AFINSQ_1:20;
suppose
ex
j being
Nat st
(
j in dom (p | k) &
i = (len <%(p . i2)%>) + j )
;
(<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . ithen consider j being
Nat such that A29:
(
j in dom (p | k) &
i = (len <%(p . i2)%>) + j )
;
A30:
(
(<%(p . i2)%> ^ (p | k)) . i = (p | k) . j &
(p | k) . j = p . j )
by A29, AFINSQ_1:def 3, FUNCT_1:47;
j in dom Idk
by A, A19, A29, AFINSQ_1:11;
then
(
(<%i2%> ^ Idk) . i = Idk . j &
Idk . j = j )
by A21, A27, A29, AFINSQ_1:def 3, FUNCT_1:17;
hence
(<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i
by A30, A24, A25, FUNCT_4:11;
verum end;
end;
hence
(
S1[
p] iff
S2[
p] )
by A20, A22, AFINSQ_1:8;
verum
end;
{ p where p is n -element XFinSequence of NAT : S1[p] } = { q where q is n -element XFinSequence of NAT : S2[q] }
from HILB10_3:sch 2(A18);
hence
{ p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)
by Th13, A1; verum