let n be Nat; for A being diophantine Subset of (n -xtuples_of NAT)
for k being Nat st k <= n holds
{ (p | k) 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 being Nat st k <= n holds
{ (p | k) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)
let k be Nat; ( k <= n implies { (p | k) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT) )
assume A1:
k <= n
; { (p | k) 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;
set D = { (p | k) where p is n -element XFinSequence of NAT : p in A } ;
{ (p | k) where p is n -element XFinSequence of NAT : p in A } c= k -xtuples_of NAT
then reconsider D = { (p | k) where p is n -element XFinSequence of NAT : p in A } as Subset of (k -xtuples_of NAT) ;
reconsider nk = n - k as Nat by A1, NAT_1:21;
reconsider P = pA as INT -valued Polynomial of (k + (nk + nA)),F_Real ;
for s being object holds
( s in D iff ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 ) )
proof
let s be
object ;
( s in D iff ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 ) )
thus
(
s in D implies ex
x being
k -element XFinSequence of
NAT ex
y being
nk + nA -element XFinSequence of
NAT st
(
s = x &
eval (
P,
(@ (x ^ y)))
= 0 ) )
( ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 ) implies s in D )proof
assume
s in D
;
ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 )
then consider p being
n -element XFinSequence of
NAT such that A4:
(
s = p | k &
p in A )
;
consider x being
n -element XFinSequence of
NAT ,
y being
nA -element XFinSequence of
NAT such that A5:
(
p = x &
eval (
pA,
(@ (x ^ y)))
= 0 )
by A4, A2;
A6:
x = (x | k) ^ (x /^ k)
;
A7:
(
len x = n &
len y = nA )
by CARD_1:def 7;
then A8:
len (x | k) = k
by A1, AFINSQ_1:54;
len (x /^ k) =
(k + nk) -' k
by A7, AFINSQ_2:def 2
.=
nk
by NAT_D:34
;
then
len ((x /^ k) ^ y) = nk + nA
by A7, AFINSQ_1:17;
then reconsider X =
(x /^ k) ^ y as
nk + nA -element XFinSequence of
NAT by CARD_1:def 7;
A9:
x ^ y = (x | k) ^ X
by A6, AFINSQ_1:27;
reconsider xk =
x | k as
k -element XFinSequence of
NAT by A8, CARD_1:def 7;
s = xk
by A4, A5;
hence
ex
x being
k -element XFinSequence of
NAT ex
y being
nk + nA -element XFinSequence of
NAT st
(
s = x &
eval (
P,
(@ (x ^ y)))
= 0 )
by A9, A5;
verum
end;
given x being
k -element XFinSequence of
NAT ,
y being
nk + nA -element XFinSequence of
NAT such that A10:
(
s = x &
eval (
P,
(@ (x ^ y)))
= 0 )
;
s in D
A11:
y = (y | nk) ^ (y /^ nk)
;
A12:
(
len x = k &
len y = nk + nA )
by CARD_1:def 7;
then A13:
len (y | nk) = nk
by NAT_1:11, AFINSQ_1:54;
A14:
len (y /^ nk) =
(nk + nA) -' nk
by A12, AFINSQ_2:def 2
.=
nA
by NAT_D:34
;
len (x ^ (y | nk)) = k + nk
by A12, A13, AFINSQ_1:17;
then reconsider X =
x ^ (y | nk) as
n -element XFinSequence of
NAT by CARD_1:def 7;
reconsider Y =
y /^ nk as
nA -element XFinSequence of
NAT by CARD_1:def 7, A14;
x ^ y = X ^ Y
by A11, AFINSQ_1:27;
then
X in A
by A2, A10;
then
X | k in D
;
hence
s in D
by A10, A12, AFINSQ_1:57;
verum
end;
hence
{ (p | k) 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