let n, k be Nat; :: thesis: for P being INT -valued Polynomial of k,F_Real

for a being Integer

for perm being Permutation of n

for i1 being Element of n st k <= n holds

{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let P be INT -valued Polynomial of k,F_Real; :: thesis: for a being Integer

for perm being Permutation of n

for i1 being Element of n st k <= n holds

{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let a be Integer; :: thesis: for perm being Permutation of n

for i1 being Element of n st k <= n holds

{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let perm be Permutation of n; :: thesis: for i1 being Element of n st k <= n holds

{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let i1 be Element of n; :: thesis: ( k <= n implies { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) )

assume A1: k <= n ; :: thesis: { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

defpred S_{1}[ XFinSequence of NAT ] means for q being k -element XFinSequence of NAT st q = ($1 * perm) | k holds

a * ($1 . i1) = eval (P,(@ q));

set A = { p where p is n -element XFinSequence of NAT : S_{1}[p] } ;

{ p where p is n -element XFinSequence of NAT : S_{1}[p] } c= n -xtuples_of NAT
_{1}[p] } as Subset of (n -xtuples_of NAT) ;

for a being Integer

for perm being Permutation of n

for i1 being Element of n st k <= n holds

{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let P be INT -valued Polynomial of k,F_Real; :: thesis: for a being Integer

for perm being Permutation of n

for i1 being Element of n st k <= n holds

{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let a be Integer; :: thesis: for perm being Permutation of n

for i1 being Element of n st k <= n holds

{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let perm be Permutation of n; :: thesis: for i1 being Element of n st k <= n holds

{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let i1 be Element of n; :: thesis: ( k <= n implies { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) )

assume A1: k <= n ; :: thesis: { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

defpred S

a * ($1 . i1) = eval (P,(@ q));

set A = { p where p is n -element XFinSequence of NAT : S

{ p where p is n -element XFinSequence of NAT : S

proof

then reconsider A = { p where p is n -element XFinSequence of NAT : S
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : S_{1}[p] } or y in n -xtuples_of NAT )

assume A2: y in { p where p is n -element XFinSequence of NAT : S_{1}[p] }
; :: thesis: y in n -xtuples_of NAT

ex p being n -element XFinSequence of NAT st

( y = p & S_{1}[p] )
by A2;

hence y in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum

end;assume A2: y in { p where p is n -element XFinSequence of NAT : S

ex p being n -element XFinSequence of NAT st

( y = p & S

hence y in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum

per cases
( n = 0 or n <> 0 )
;

end;

suppose
n = 0
; :: thesis: { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

then
A is diophantine
;

hence { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) ; :: thesis: verum

end;hence { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) ; :: thesis: verum

suppose A3:
n <> 0
; :: thesis: { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

reconsider nk = n - k as Nat by A1, NAT_1:21;

consider Q being Polynomial of (k + nk),F_Real such that

A4: rng Q c= (rng P) \/ {(0. F_Real)} and

A5: for x being Function of k,F_Real

for y being Function of (k + nk),F_Real st y | k = x holds

eval (P,x) = eval (Q,y) by HILB10_2:27;

A6: rng P c= INT by RELAT_1:def 19;

0. F_Real in INT by INT_1:def 1;

then {(0. F_Real)} c= INT by ZFMISC_1:31;

then (rng P) \/ {(0. F_Real)} c= INT by A6, XBOOLE_1:8;

then reconsider Q1 = Q as INT -valued Polynomial of n,F_Real by RELAT_1:def 19, A4, XBOOLE_1:1;

set T = Q1 permuted_by perm;

A7: rng (Q1 permuted_by perm) = rng Q1 by HILB10_2:26;

rng Q1 c= INT by RELAT_1:def 19;

then reconsider T1 = Q1 permuted_by perm as INT -valued Polynomial of n,F_Real by A7, RELAT_1:def 19;

reconsider FR = F_Real as Field ;

reconsider ar = a as Element of FR by XREAL_0:def 1;

reconsider Ar = ar as Element of F_Real ;

reconsider t = Q1 permuted_by perm as Polynomial of n,FR ;

T1 = t ;

then reconsider TI = t - (ar * (1_1 (i1,FR))) as INT -valued Polynomial of (n + 0),F_Real ;

for s being object holds

( s in A iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st

( s = x & eval (TI,(@ (x ^ y))) = 0 ) )

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) by HILB10_2:def 6; :: thesis: verum

end;consider Q being Polynomial of (k + nk),F_Real such that

A4: rng Q c= (rng P) \/ {(0. F_Real)} and

A5: for x being Function of k,F_Real

for y being Function of (k + nk),F_Real st y | k = x holds

eval (P,x) = eval (Q,y) by HILB10_2:27;

A6: rng P c= INT by RELAT_1:def 19;

0. F_Real in INT by INT_1:def 1;

then {(0. F_Real)} c= INT by ZFMISC_1:31;

then (rng P) \/ {(0. F_Real)} c= INT by A6, XBOOLE_1:8;

then reconsider Q1 = Q as INT -valued Polynomial of n,F_Real by RELAT_1:def 19, A4, XBOOLE_1:1;

set T = Q1 permuted_by perm;

A7: rng (Q1 permuted_by perm) = rng Q1 by HILB10_2:26;

rng Q1 c= INT by RELAT_1:def 19;

then reconsider T1 = Q1 permuted_by perm as INT -valued Polynomial of n,F_Real by A7, RELAT_1:def 19;

reconsider FR = F_Real as Field ;

reconsider ar = a as Element of FR by XREAL_0:def 1;

reconsider Ar = ar as Element of F_Real ;

reconsider t = Q1 permuted_by perm as Polynomial of n,FR ;

T1 = t ;

then reconsider TI = t - (ar * (1_1 (i1,FR))) as INT -valued Polynomial of (n + 0),F_Real ;

for s being object holds

( s in A iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st

( s = x & eval (TI,(@ (x ^ y))) = 0 ) )

proof

hence
{ p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds
let s be object ; :: thesis: ( s in A iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st

( s = x & eval (TI,(@ (x ^ y))) = 0 ) )

thus ( s in A implies ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st

( s = x & eval (TI,(@ (x ^ y))) = 0 ) ) :: thesis: ( ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st

( s = x & eval (TI,(@ (x ^ y))) = 0 ) implies s in A )

reconsider xy = @ (x ^ y) as Function of n,FR ;

A17: eval ((1_1 (i1,FR)),xy) = xy . i1 by A3, HILB10_3:1

.= x . i1 by HILB10_2:def 1 ;

reconsider Eval = eval ((1_1 (i1,FR)),xy) as Element of F_Real ;

A18: eval ((ar * (1_1 (i1,FR))),xy) = Ar * Eval by POLYNOM7:29

.= a * (x . i1) by A17 ;

A19: ( dom perm = n & rng perm = n & len x = n ) by FUNCT_2:52, FUNCT_2:def 3, CARD_1:def 7;

then dom (x * perm) = n by RELAT_1:27;

then reconsider xp = x * perm as XFinSequence by AFINSQ_1:5;

A20: len xp = n by A19, RELAT_1:27;

reconsider XP = xp as n -element XFinSequence of NAT by A20, CARD_1:def 7;

len (XP | k) = k by A20, A1, AFINSQ_1:54;

then reconsider XPk = XP | k as k -element XFinSequence of NAT by CARD_1:def 7;

(@ XP) | k = XP | k by HILB10_2:def 1;

then A21: (@ XP) | k = @ XPk by HILB10_2:def 1;

XP * (perm ") = x * (perm * (perm ")) by RELAT_1:36

.= x * (id n) by FUNCT_2:61

.= x by A19, RELAT_1:51 ;

then A22: XP * (perm ") = @ x by HILB10_2:def 1;

A23: eval ((Q1 permuted_by perm),(@ x)) = eval ((Q1 permuted_by perm),((@ XP) * (perm "))) by A22, HILB10_2:def 1

.= eval (Q1,(@ XP)) by HILB10_2:25

.= eval (P,(@ XPk)) by A5, A21 ;

A24: (eval (t,xy)) - (eval ((ar * (1_1 (i1,FR))),xy)) = 0. FR by POLYNOM2:24, A16;

S_{1}[x]
by A24, A18, A23, VECTSP_1:19;

hence s in A by A16; :: thesis: verum

end;( s = x & eval (TI,(@ (x ^ y))) = 0 ) )

thus ( s in A implies ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st

( s = x & eval (TI,(@ (x ^ y))) = 0 ) ) :: thesis: ( ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st

( s = x & eval (TI,(@ (x ^ y))) = 0 ) implies s in A )

proof

given x being n -element XFinSequence of NAT , y being 0 -element XFinSequence of NAT such that A16:
( s = x & eval (TI,(@ (x ^ y))) = 0 )
; :: thesis: s in A
assume
s in A
; :: thesis: ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st

( s = x & eval (TI,(@ (x ^ y))) = 0 )

then consider p being n -element XFinSequence of NAT such that

A8: ( s = p & S_{1}[p] )
;

reconsider E = <%> NAT as 0 -element XFinSequence of NAT ;

take p ; :: thesis: ex y being 0 -element XFinSequence of NAT st

( s = p & eval (TI,(@ (p ^ y))) = 0 )

take E ; :: thesis: ( s = p & eval (TI,(@ (p ^ E))) = 0 )

thus s = p by A8; :: thesis: eval (TI,(@ (p ^ E))) = 0

reconsider pE = @ (p ^ E) as Function of n,FR ;

A9: eval ((1_1 (i1,FR)),pE) = pE . i1 by A3, HILB10_3:1

.= p . i1 by HILB10_2:def 1 ;

reconsider Eval = eval ((1_1 (i1,FR)),pE) as Element of F_Real ;

A10: eval ((ar * (1_1 (i1,FR))),pE) = Ar * Eval by POLYNOM7:29

.= a * (p . i1) by A9 ;

A11: ( dom perm = n & rng perm = n & len p = n ) by FUNCT_2:52, FUNCT_2:def 3, CARD_1:def 7;

then dom (p * perm) = n by RELAT_1:27;

then reconsider pp = p * perm as XFinSequence by AFINSQ_1:5;

A12: len pp = n by A11, RELAT_1:27;

reconsider PP = pp as n -element XFinSequence of NAT by A12, CARD_1:def 7;

len (PP | k) = k by A12, A1, AFINSQ_1:54;

then reconsider PPk = PP | k as k -element XFinSequence of NAT by CARD_1:def 7;

(@ PP) | k = PP | k by HILB10_2:def 1;

then A13: (@ PP) | k = @ PPk by HILB10_2:def 1;

PP * (perm ") = p * (perm * (perm ")) by RELAT_1:36

.= p * (id n) by FUNCT_2:61

.= p by A11, RELAT_1:51 ;

then A14: PP * (perm ") = @ p by HILB10_2:def 1;

A15: eval ((Q1 permuted_by perm),(@ p)) = eval ((Q1 permuted_by perm),((@ PP) * (perm "))) by A14, HILB10_2:def 1

.= eval (Q1,(@ PP)) by HILB10_2:25

.= eval (P,(@ PPk)) by A5, A13

.= a * (p . i1) by A8 ;

thus eval (TI,(@ (p ^ E))) = (eval (t,pE)) - (eval ((ar * (1_1 (i1,FR))),pE)) by POLYNOM2:24

.= 0. FR by A10, A15, RLVECT_1:5

.= 0 ; :: thesis: verum

end;( s = x & eval (TI,(@ (x ^ y))) = 0 )

then consider p being n -element XFinSequence of NAT such that

A8: ( s = p & S

reconsider E = <%> NAT as 0 -element XFinSequence of NAT ;

take p ; :: thesis: ex y being 0 -element XFinSequence of NAT st

( s = p & eval (TI,(@ (p ^ y))) = 0 )

take E ; :: thesis: ( s = p & eval (TI,(@ (p ^ E))) = 0 )

thus s = p by A8; :: thesis: eval (TI,(@ (p ^ E))) = 0

reconsider pE = @ (p ^ E) as Function of n,FR ;

A9: eval ((1_1 (i1,FR)),pE) = pE . i1 by A3, HILB10_3:1

.= p . i1 by HILB10_2:def 1 ;

reconsider Eval = eval ((1_1 (i1,FR)),pE) as Element of F_Real ;

A10: eval ((ar * (1_1 (i1,FR))),pE) = Ar * Eval by POLYNOM7:29

.= a * (p . i1) by A9 ;

A11: ( dom perm = n & rng perm = n & len p = n ) by FUNCT_2:52, FUNCT_2:def 3, CARD_1:def 7;

then dom (p * perm) = n by RELAT_1:27;

then reconsider pp = p * perm as XFinSequence by AFINSQ_1:5;

A12: len pp = n by A11, RELAT_1:27;

reconsider PP = pp as n -element XFinSequence of NAT by A12, CARD_1:def 7;

len (PP | k) = k by A12, A1, AFINSQ_1:54;

then reconsider PPk = PP | k as k -element XFinSequence of NAT by CARD_1:def 7;

(@ PP) | k = PP | k by HILB10_2:def 1;

then A13: (@ PP) | k = @ PPk by HILB10_2:def 1;

PP * (perm ") = p * (perm * (perm ")) by RELAT_1:36

.= p * (id n) by FUNCT_2:61

.= p by A11, RELAT_1:51 ;

then A14: PP * (perm ") = @ p by HILB10_2:def 1;

A15: eval ((Q1 permuted_by perm),(@ p)) = eval ((Q1 permuted_by perm),((@ PP) * (perm "))) by A14, HILB10_2:def 1

.= eval (Q1,(@ PP)) by HILB10_2:25

.= eval (P,(@ PPk)) by A5, A13

.= a * (p . i1) by A8 ;

thus eval (TI,(@ (p ^ E))) = (eval (t,pE)) - (eval ((ar * (1_1 (i1,FR))),pE)) by POLYNOM2:24

.= 0. FR by A10, A15, RLVECT_1:5

.= 0 ; :: thesis: verum

reconsider xy = @ (x ^ y) as Function of n,FR ;

A17: eval ((1_1 (i1,FR)),xy) = xy . i1 by A3, HILB10_3:1

.= x . i1 by HILB10_2:def 1 ;

reconsider Eval = eval ((1_1 (i1,FR)),xy) as Element of F_Real ;

A18: eval ((ar * (1_1 (i1,FR))),xy) = Ar * Eval by POLYNOM7:29

.= a * (x . i1) by A17 ;

A19: ( dom perm = n & rng perm = n & len x = n ) by FUNCT_2:52, FUNCT_2:def 3, CARD_1:def 7;

then dom (x * perm) = n by RELAT_1:27;

then reconsider xp = x * perm as XFinSequence by AFINSQ_1:5;

A20: len xp = n by A19, RELAT_1:27;

reconsider XP = xp as n -element XFinSequence of NAT by A20, CARD_1:def 7;

len (XP | k) = k by A20, A1, AFINSQ_1:54;

then reconsider XPk = XP | k as k -element XFinSequence of NAT by CARD_1:def 7;

(@ XP) | k = XP | k by HILB10_2:def 1;

then A21: (@ XP) | k = @ XPk by HILB10_2:def 1;

XP * (perm ") = x * (perm * (perm ")) by RELAT_1:36

.= x * (id n) by FUNCT_2:61

.= x by A19, RELAT_1:51 ;

then A22: XP * (perm ") = @ x by HILB10_2:def 1;

A23: eval ((Q1 permuted_by perm),(@ x)) = eval ((Q1 permuted_by perm),((@ XP) * (perm "))) by A22, HILB10_2:def 1

.= eval (Q1,(@ XP)) by HILB10_2:25

.= eval (P,(@ XPk)) by A5, A21 ;

A24: (eval (t,xy)) - (eval ((ar * (1_1 (i1,FR))),xy)) = 0. FR by POLYNOM2:24, A16;

S

hence s in A by A16; :: thesis: verum

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) by HILB10_2:def 6; :: thesis: verum