let n be Nat; for A being diophantine Subset of (n -xtuples_of NAT)
for k, nk being Nat st k + nk = n holds
{ (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)
let A be diophantine Subset of (n -xtuples_of NAT); for k, nk being Nat st k + nk = n holds
{ (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)
let k, nk be Nat; ( k + nk = n implies { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT) )
assume A1:
k + nk = n
; { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)
consider nA being Nat, pA being INT -valued Polynomial of (n + nA),F_Real such that
A2:
for s being object holds
( s in A iff ex x being n -element XFinSequence of NAT ex y being nA -element XFinSequence of NAT st
( s = x & eval (pA,(@ (x ^ y))) = 0 ) )
by HILB10_2:def 6;
dom (id (n + nA)) = n + nA
;
then reconsider I = id (n + nA) as XFinSequence by AFINSQ_1:5;
set I1 = I | nk;
set I2 = (I | n) /^ nk;
set I3 = I /^ n;
Segm nk c= Segm n
by NAT_1:39, NAT_1:11, A1;
then A3:
(I | n) | nk = I | nk
by RELAT_1:74;
then A4:
( I = (I | n) ^ (I /^ n) & I | n = (I | nk) ^ ((I | n) /^ nk) )
;
then A5:
rng (I | n) misses rng (I /^ n)
by HILB10_2:1;
A6:
len I = n + nA
;
A7:
n <= n + nA
by NAT_1:11;
A8:
( len (I /^ n) = (n + nA) -' n & (n + nA) -' n = (n + nA) - n & len (I | n) = n )
by A6, AFINSQ_2:def 2, AFINSQ_1:54, NAT_1:11;
A9:
( len ((I | n) /^ nk) = n -' nk & n -' nk = n - nk & len (I | nk) = nk )
by A1, NAT_1:11, A8, AFINSQ_2:def 2, AFINSQ_1:54, A3;
A10:
( len ((((I | n) /^ nk) ^ (I | nk)) ^ (I /^ n)) = (len (((I | n) /^ nk) ^ (I | nk))) + (len (I /^ n)) & len (((I | n) /^ nk) ^ (I | nk)) = (len ((I | n) /^ nk)) + (len (I | nk)) )
by AFINSQ_1:17;
A11:
rng (I | nk) misses rng ((I | n) /^ nk)
by A4, HILB10_2:1;
A12:
(rng (I | n)) \/ (rng (I /^ n)) = rng I
by A4, AFINSQ_1:26;
A13:
( (rng (I | nk)) \/ (rng ((I | n) /^ nk)) = rng (I | n) & rng (((I | n) /^ nk) ^ (I | nk)) = (rng ((I | n) /^ nk)) \/ (rng (I | nk)) )
by A4, AFINSQ_1:26;
then
rng ((((I | n) /^ nk) ^ (I | nk)) ^ (I /^ n)) = n + nA
by A12, AFINSQ_1:26;
then reconsider J = (((I | n) /^ nk) ^ (I | nk)) ^ (I /^ n) as Function of (n + nA),(n + nA) by A10, A8, A9, FUNCT_2:1;
A14:
J is onto
by A13, A12, AFINSQ_1:26;
A15:
((I | n) /^ nk) ^ (I | nk) is one-to-one
by A11, CARD_FIN:52;
J is one-to-one
by A13, A5, A15, CARD_FIN:52;
then reconsider J = J as Permutation of (n + nA) by A14;
A16:
J = (J ") "
by FUNCT_1:43;
set h = pA permuted_by (J ");
reconsider H = pA permuted_by (J ") as Polynomial of (k + (nk + nA)),F_Real by A1;
( rng (pA permuted_by (J ")) = rng pA & rng pA c= INT )
by HILB10_2:26, RELAT_1:def 19;
then reconsider H = H as INT -valued Polynomial of (k + (nk + nA)),F_Real by RELAT_1:def 19;
set Y = { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } ;
{ (p /^ nk) where p is n -element XFinSequence of NAT : p in A } c= k -xtuples_of NAT
then reconsider Y = { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } as Subset of (k -xtuples_of NAT) ;
for s being object holds
( s in Y iff ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (H,(@ (x ^ y))) = 0 ) )
proof
let s be
object ;
( s in Y iff ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (H,(@ (x ^ y))) = 0 ) )
thus
(
s in Y implies ex
x being
k -element XFinSequence of
NAT ex
y being
nk + nA -element XFinSequence of
NAT st
(
s = x &
eval (
H,
(@ (x ^ y)))
= 0 ) )
( ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (H,(@ (x ^ y))) = 0 ) implies s in Y )proof
assume
s in Y
;
ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (H,(@ (x ^ y))) = 0 )
then consider w being
n -element XFinSequence of
NAT such that A18:
(
s = w /^ nk &
w in A )
;
consider x being
n -element XFinSequence of
NAT ,
y being
nA -element XFinSequence of
NAT such that A19:
(
w = x &
eval (
pA,
(@ (x ^ y)))
= 0 )
by A2, A18;
A20:
eval (
pA,
(@ (x ^ y)))
= eval (
(pA permuted_by (J ")),
((@ (x ^ y)) * ((J ") ")))
by HILB10_2:25;
A21:
(
len x = n &
len y = nA )
by CARD_1:def 7;
then A22:
len (x /^ nk) = k
by A1, A9, AFINSQ_2:def 2;
x /^ nk is
k -element
by A21, A1, A9, AFINSQ_2:def 2;
then reconsider S =
x /^ nk as
k -element XFinSequence of
NAT ;
A23:
len (x | nk) = nk
by CARD_1:def 7, A1;
reconsider XnkY =
(x | nk) ^ y as
nk + nA -element XFinSequence of
NAT by A1;
A26:
len (S ^ XnkY) = n + nA
by A1, CARD_1:def 7;
A27:
dom ((@ (x ^ y)) * J) = n + nA
by FUNCT_2:def 1;
(x | nk) ^ (x /^ nk) = x
;
then A28:
x ^ y = (x | nk) ^ (S ^ y)
by AFINSQ_1:27;
for
i being
object st
i in dom (S ^ XnkY) holds
((@ (x ^ y)) * J) . i = (S ^ XnkY) . i
proof
let j be
object ;
( j in dom (S ^ XnkY) implies ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j )
assume A29:
j in dom (S ^ XnkY)
;
((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
then reconsider j =
j as
Nat ;
A30:
(
j in dom J &
((@ (x ^ y)) * J) . j = (@ (x ^ y)) . (J . j) )
by A29, A26, A27, FUNCT_1:11, FUNCT_1:12;
per cases
( j in dom (((I | n) /^ nk) ^ (I | nk)) or ex n being Nat st
( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) )
by A30, AFINSQ_1:20;
suppose A31:
j in dom (((I | n) /^ nk) ^ (I | nk))
;
((@ (x ^ y)) * J) . j = (S ^ XnkY) . jthen A32:
J . j = (((I | n) /^ nk) ^ (I | nk)) . j
by AFINSQ_1:def 3;
per cases
( j in dom ((I | n) /^ nk) or ex k being Nat st
( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) )
by A31, AFINSQ_1:20;
suppose A33:
j in dom ((I | n) /^ nk)
;
((@ (x ^ y)) * J) . j = (S ^ XnkY) . jthen A34:
(
(((I | n) /^ nk) ^ (I | nk)) . j = ((I | n) /^ nk) . j &
((I | n) /^ nk) . j = (I | n) . (nk + j) &
j < k )
by A9, A1, AFINSQ_2:def 2, AFINSQ_1:66, AFINSQ_1:def 3;
A35:
nk + j in n
by A1, A33, A9, AFINSQ_1:66, HILB10_3:3;
then A36:
(I | n) . (nk + j) = I . (nk + j)
by FUNCT_1:49;
A37:
dom S c= dom (S ^ y)
by AFINSQ_1:21;
A38:
(
len S = k &
k = len ((I | n) /^ nk) )
by CARD_1:def 7, A1, A9;
Segm n = n
;
then
nk + j < n + nA
by NAT_1:44, A35, A7, XXREAL_0:2;
then
nk + j in Segm (n + nA)
by NAT_1:44;
then ((@ (x ^ y)) * J) . j =
(@ (x ^ y)) . (nk + j)
by FUNCT_1:17, A32, A30, A36, A34
.=
(x ^ y) . (nk + j)
by HILB10_2:def 1
.=
(S ^ y) . j
by A23, A37, A22, A33, A1, A9, A28, AFINSQ_1:def 3
.=
S . j
by A22, A33, A1, A9, AFINSQ_1:def 3
.=
(S ^ XnkY) . j
by A33, A38, AFINSQ_1:def 3
;
hence
((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
;
verum end; suppose
ex
k being
Nat st
(
k in dom (I | nk) &
j = (len ((I | n) /^ nk)) + k )
;
((@ (x ^ y)) * J) . j = (S ^ XnkY) . jthen consider w being
Nat such that A39:
(
w in dom (I | nk) &
j = (len ((I | n) /^ nk)) + w )
;
A40:
(
(((I | n) /^ nk) ^ (I | nk)) . j = (I | nk) . w &
(I | nk) . w = I . w &
w < nk )
by A39, A9, AFINSQ_1:66, AFINSQ_1:def 3, FUNCT_1:49;
A41:
dom (x | nk) c= dom ((x | nk) ^ y)
by AFINSQ_1:21;
nk <= nk + (k + nA)
by NAT_1:11;
then
w < n + nA
by A1, A39, A9, AFINSQ_1:66, XXREAL_0:2;
then A42:
w in Segm (n + nA)
by NAT_1:44;
J . j = w
by A42, A40, A32, FUNCT_1:17;
then ((@ (x ^ y)) * J) . j =
((x | nk) ^ (S ^ y)) . w
by A30, A28, HILB10_2:def 1
.=
(x | nk) . w
by AFINSQ_1:def 3, A39, A23, A9
.=
((x | nk) ^ y) . w
by A39, A23, A9, AFINSQ_1:def 3
.=
(S ^ XnkY) . j
by A22, A39, A1, A9, A41, A23, AFINSQ_1:def 3
;
hence
((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
;
verum end; end; end; suppose
ex
n being
Nat st
(
n in dom (I /^ n) &
j = (len (((I | n) /^ nk) ^ (I | nk))) + n )
;
((@ (x ^ y)) * J) . j = (S ^ XnkY) . jthen consider w being
Nat such that A43:
(
w in dom (I /^ n) &
j = (len (((I | n) /^ nk) ^ (I | nk))) + w )
;
A44:
len (S ^ (x | nk)) = n
by CARD_1:def 7, A1;
J . j =
(I /^ n) . w
by A43, AFINSQ_1:def 3
.=
I . j
by A9, A10, A43, AFINSQ_2:def 2
.=
j
by A29, A26, FUNCT_1:17
;
then ((@ (x ^ y)) * J) . j =
(x ^ y) . j
by A30, HILB10_2:def 1
.=
y . w
by A9, A10, A43, A8, A21, AFINSQ_1:def 3
.=
((S ^ (x | nk)) ^ y) . j
by A44, A9, A10, A43, A8, A21, AFINSQ_1:def 3
.=
(S ^ XnkY) . j
by AFINSQ_1:27
;
hence
((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
;
verum end; end;
end;
then
(@ (x ^ y)) * J = S ^ XnkY
by CARD_1:def 7, A1, A27, FUNCT_1:2;
then
(@ (x ^ y)) * J = @ (S ^ XnkY)
by HILB10_2:def 1;
hence
ex
x being
k -element XFinSequence of
NAT ex
y being
nk + nA -element XFinSequence of
NAT st
(
s = x &
eval (
H,
(@ (x ^ y)))
= 0 )
by A19, A18, A20, A16;
verum
end;
given S being
k -element XFinSequence of
NAT ,
XnkY being
nk + nA -element XFinSequence of
NAT such that A45:
(
s = S &
eval (
H,
(@ (S ^ XnkY)))
= 0 )
;
s in Y
set Xnk =
XnkY | nk;
set y =
XnkY /^ nk;
set X =
(XnkY | nk) ^ S;
A46:
(
len S = k &
len XnkY = nk + nA &
nk + nA >= nk )
by NAT_1:11, CARD_1:def 7;
then A47:
(
len (XnkY | nk) = nk &
len (XnkY /^ nk) = (nk + nA) -' nk &
(nk + nA) -' nk = (nk + nA) - nk )
by AFINSQ_1:54, AFINSQ_2:def 2;
reconsider y =
XnkY /^ nk as
nA -element XFinSequence of
NAT by A47, CARD_1:def 7;
reconsider X =
(XnkY | nk) ^ S as
n -element XFinSequence of
NAT by A1;
A48:
X | nk = XnkY | nk
by A47, AFINSQ_1:57;
(XnkY | nk) ^ S = (X | nk) ^ (X /^ nk)
;
then A49:
X /^ nk = S
by A48, AFINSQ_1:28;
A50:
XnkY = (XnkY | nk) ^ y
;
A51:
(
len X = n &
len y = nA )
by CARD_1:def 7;
A52:
len (X | nk) = nk
by A47, AFINSQ_1:57;
A53:
len (S ^ XnkY) = n + nA
by CARD_1:def 7, A1;
A54:
dom ((@ (X ^ y)) * J) = n + nA
by FUNCT_2:def 1;
A55:
X ^ y = (X | nk) ^ (S ^ y)
by A48, AFINSQ_1:27;
for
i being
object st
i in dom (S ^ XnkY) holds
((@ (X ^ y)) * J) . i = (S ^ XnkY) . i
proof
let j be
object ;
( j in dom (S ^ XnkY) implies ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j )
assume A56:
j in dom (S ^ XnkY)
;
((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
then reconsider j =
j as
Nat ;
A57:
(
j in dom J &
((@ (X ^ y)) * J) . j = (@ (X ^ y)) . (J . j) )
by A56, A53, A54, FUNCT_1:11, FUNCT_1:12;
per cases
( j in dom (((I | n) /^ nk) ^ (I | nk)) or ex n being Nat st
( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) )
by A57, AFINSQ_1:20;
suppose A58:
j in dom (((I | n) /^ nk) ^ (I | nk))
;
((@ (X ^ y)) * J) . j = (S ^ XnkY) . jthen A59:
J . j = (((I | n) /^ nk) ^ (I | nk)) . j
by AFINSQ_1:def 3;
per cases
( j in dom ((I | n) /^ nk) or ex k being Nat st
( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) )
by A58, AFINSQ_1:20;
suppose A60:
j in dom ((I | n) /^ nk)
;
((@ (X ^ y)) * J) . j = (S ^ XnkY) . jthen A61:
(
(((I | n) /^ nk) ^ (I | nk)) . j = ((I | n) /^ nk) . j &
((I | n) /^ nk) . j = (I | n) . (nk + j) &
j < k )
by A9, A1, AFINSQ_2:def 2, AFINSQ_1:66, AFINSQ_1:def 3;
then A63:
(I | n) . (nk + j) = I . (nk + j)
by A1, HILB10_3:3, FUNCT_1:49;
A62:
nk + j in n
by A60, A1, HILB10_3:3, A9, AFINSQ_1:66;
A64:
dom S c= dom (S ^ y)
by AFINSQ_1:21;
A65:
(
len S = k &
k = len ((I | n) /^ nk) )
by CARD_1:def 7, A1, A9;
Segm n = n
;
then
nk + j < n + nA
by NAT_1:44, A62, A7, XXREAL_0:2;
then
nk + j in Segm (n + nA)
by NAT_1:44;
then
I . (nk + j) = nk + j
by FUNCT_1:17;
then ((@ (X ^ y)) * J) . j =
((X | nk) ^ (S ^ y)) . (nk + j)
by A55, HILB10_2:def 1, A59, A57, A63, A61
.=
(S ^ y) . j
by A52, A64, A60, A1, A46, A9, AFINSQ_1:def 3
.=
S . j
by A60, A1, A46, A9, AFINSQ_1:def 3
.=
(S ^ XnkY) . j
by A60, A65, AFINSQ_1:def 3
;
hence
((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
;
verum end; suppose
ex
k being
Nat st
(
k in dom (I | nk) &
j = (len ((I | n) /^ nk)) + k )
;
((@ (X ^ y)) * J) . j = (S ^ XnkY) . jthen consider w being
Nat such that A66:
(
w in dom (I | nk) &
j = (len ((I | n) /^ nk)) + w )
;
A67:
(
(((I | n) /^ nk) ^ (I | nk)) . j = (I | nk) . w &
(I | nk) . w = I . w &
w < nk )
by A66, A9, AFINSQ_1:66, AFINSQ_1:def 3, FUNCT_1:49;
A68:
dom (X | nk) c= dom ((X | nk) ^ y)
by AFINSQ_1:21;
nk <= nk + (k + nA)
by NAT_1:11;
then
w < n + nA
by A1, A66, A9, AFINSQ_1:66, XXREAL_0:2;
then A69:
w in Segm (n + nA)
by NAT_1:44;
J . j = w
by A59, A69, FUNCT_1:17, A67;
then ((@ (X ^ y)) * J) . j =
(X ^ y) . w
by HILB10_2:def 1, A57
.=
(X | nk) . w
by AFINSQ_1:def 3, A66, A52, A9, A55
.=
((X | nk) ^ y) . w
by A66, A52, A9, AFINSQ_1:def 3
.=
(S ^ XnkY) . j
by A48, A46, A1, A9, A68, A47, A66, AFINSQ_1:def 3
;
hence
((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
;
verum end; end; end; suppose
ex
n being
Nat st
(
n in dom (I /^ n) &
j = (len (((I | n) /^ nk) ^ (I | nk))) + n )
;
((@ (X ^ y)) * J) . j = (S ^ XnkY) . jthen consider w being
Nat such that A70:
(
w in dom (I /^ n) &
j = (len (((I | n) /^ nk) ^ (I | nk))) + w )
;
A71:
len (S ^ (X | nk)) = n
by A1, CARD_1:def 7;
J . j =
(I /^ n) . w
by A70, AFINSQ_1:def 3
.=
I . j
by A9, A10, A70, AFINSQ_2:def 2
.=
j
by A56, A53, FUNCT_1:17
;
then ((@ (X ^ y)) * J) . j =
(X ^ y) . j
by HILB10_2:def 1, A57
.=
y . w
by A9, A10, A70, A8, A51, AFINSQ_1:def 3
.=
((S ^ (X | nk)) ^ y) . j
by A71, A9, A10, A70, A8, A51, AFINSQ_1:def 3
.=
(S ^ XnkY) . j
by AFINSQ_1:27, A48, A50
;
hence
((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
;
verum end; end;
end;
then
(@ (X ^ y)) * J = S ^ XnkY
by CARD_1:def 7, A1, A54, FUNCT_1:2;
then
(@ (X ^ y)) * J = @ (S ^ XnkY)
by HILB10_2:def 1;
then
eval (
H,
(@ (S ^ XnkY)))
= eval (
pA,
(@ (X ^ y)))
by A16, HILB10_2:25;
then
X in A
by A2, A45;
hence
s in Y
by A49, A45;
verum
end;
hence
{ (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)
by HILB10_2:def 6; verum