:: Diophantine sets -- Preliminaries
:: by Karol P\kak
::
:: Received March 27, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users

registration

let X be non empty set ;
let n be Nat;

cluster Relation-like omega -defined X -valued Function-like Sequence-like finite n -element finite-support V268() for set ;

existence
ex b₁ being XFinSequence of X st b₁ is n -element

proof end;

end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like Sequence-like finite n -element real-valued finite-support V268() for set ;

existence
ex b₁ being XFinSequence st
( b₁ is n -element & b₁ is real-valued )

proof end;

end;

registration

let n, m be Nat;
let p be n -element XFinSequence;
let q be m -element XFinSequence;

cluster p ^ q -> n + m -element ;

coherence
p ^ q is n + m -element

proof end;

end;

registration

let p, q be real-valued XFinSequence;

cluster p ^ q -> real-valued ;

coherence
p ^ q is real-valued

proof end;

end;

definition

let n be Nat;
let p be n -element real-valued XFinSequence;

func @ p -> Function of n,F_Real equals :: HILB10_2:def 1
p;

coherence
p is Function of n,F_Real

proof end;

end;

:: deftheorem defines @ HILB10_2:def 1 :
for n being Nat
for p being b₁ -element real-valued XFinSequence holds @ p = p;

definition

let n be Nat;
let X be non empty set ;
let p be Function of n,X;

func @ p -> n -element XFinSequence of X equals :: HILB10_2:def 2
p;

coherence
p is n -element XFinSequence of X

proof end;

end;

:: deftheorem defines @ HILB10_2:def 2 :
for n being Nat
for X being non empty set
for p being Function of n,X holds @ p = p;

registration

let X be set ;
let p be Permutation of X;
let M be ManySortedSet of X;

cluster p * M -> total ;

coherence
M * p is total

proof end;

end;

registration

let F be finite-support Function;
let f be one-to-one Function;

cluster f * F -> finite-support ;

coherence
F * f is finite-support

proof end;

end;

theorem Th1: :: HILB10_2:1

for F, G being XFinSequence st F ^ G is one-to-one holds
rng F misses rng G

proof end;

theorem Th2: :: HILB10_2:2

for X being set
for f being b₁ -defined Function
for perm being Permutation of X holds card (support (f * perm)) = card (support f)

proof end;

registration

let X be set ;

cluster 0_ (X,F_Real) -> natural-valued ;

coherence
0_ (X,F_Real) is natural-valued

proof end;

cluster 1_ (X,F_Real) -> natural-valued ;

coherence
1_ (X,F_Real) is natural-valued

proof end;

end;

registration

let X be set ;
let x be Element of X;

cluster 1_1 (x,F_Real) -> natural-valued ;

coherence
1_1 (x,F_Real) is natural-valued

proof end;

end;

registration

let X be set ;

cluster Relation-like Bags X -defined INT -valued the carrier of F_Real -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued for Element of K27(K28((Bags X), the carrier of F_Real));

existence
ex b₁ being Series of X,F_Real st b₁ is INT -valued

proof end;

end;

registration

let O be Ordinal;

cluster Relation-like Bags O -defined INT -valued the carrier of F_Real -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued finite-Support for Element of K27(K28((Bags O), the carrier of F_Real));

existence
ex b₁ being Polynomial of O,F_Real st b₁ is INT -valued

proof end;

end;

registration

let X be set ;
let p be INT -valued Series of X,F_Real;

cluster - p -> INT -valued ;

coherence
- p is INT -valued

proof end;

let q be INT -valued Series of X,F_Real;

cluster p + q -> INT -valued ;

coherence
p + q is INT -valued

proof end;

cluster p - q -> INT -valued ;

coherence
p - q is INT -valued

proof end;

end;

registration

let X be Ordinal;
let p, q be INT -valued Series of X,F_Real;

cluster p *' q -> INT -valued ;

coherence
p *' q is INT -valued

proof end;

end;

registration

let X be set ;

cluster Relation-like X -defined the carrier of F_Real -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued for Element of K27(K28(X, the carrier of F_Real));

existence
ex b₁ being Function of X,F_Real st b₁ is natural-valued

proof end;

end;

registration

let O be Ordinal;

cluster Relation-like O -defined INT -valued the carrier of F_Real -valued Function-like total quasi_total complex-valued ext-real-valued real-valued for Element of K27(K28(O, the carrier of F_Real));

existence
ex b₁ being Function of O,F_Real st b₁ is INT -valued

proof end;

end;

registration

let O be Ordinal;
let b be bag of O;
let x be INT -valued Function of O,F_Real;

cluster eval (b,x) -> integer ;

coherence
eval (b,x) is integer

proof end;

end;

registration

let O be Ordinal;
let p be INT -valued Polynomial of O,F_Real;
let x be INT -valued Function of O,F_Real;

cluster eval (p,x) -> integer ;

coherence
eval (p,x) is integer

proof end;

end;

theorem Th3: :: HILB10_2:3

for k, n being Nat
for b being ManySortedSet of n st k <= n holds
(0,k) -cut b = b | k

proof end;

theorem Th4: :: HILB10_2:4

for n being Nat
for b being bag of n + 1 holds b = ((0,n) -cut b) bag_extend (b . n)

proof end;

theorem Th5: :: HILB10_2:5

for k, n being Nat
for b being bag of n holds (0,n) -cut (b bag_extend k) = b

proof end;

definition

let n be Nat;
let L be non empty ZeroStr ;
let p be Series of n,L;

func p extended_by_0 -> Series of (n + 1),L means :Def3: :: HILB10_2:def 3
for b being bag of n + 1 holds
( ( b . n <> 0 implies it . b = 0. L ) & ( b . n = 0 implies it . b = p . ((0,n) -cut b) ) );

existence
ex b₁ being Series of (n + 1),L st
for b being bag of n + 1 holds
( ( b . n <> 0 implies b₁ . b = 0. L ) & ( b . n = 0 implies b₁ . b = p . ((0,n) -cut b) ) )

proof end;

uniqueness
for b₁, b₂ being Series of (n + 1),L st ( for b being bag of n + 1 holds
( ( b . n <> 0 implies b₁ . b = 0. L ) & ( b . n = 0 implies b₁ . b = p . ((0,n) -cut b) ) ) ) & ( for b being bag of n + 1 holds
( ( b . n <> 0 implies b₂ . b = 0. L ) & ( b . n = 0 implies b₂ . b = p . ((0,n) -cut b) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines extended_by_0 HILB10_2:def 3 :
for n being Nat
for L being non empty ZeroStr
for p being Series of n,L
for b₄ being Series of (n + 1),L holds
( b₄ = p extended_by_0 iff for b being bag of n + 1 holds
( ( b . n <> 0 implies b₄ . b = 0. L ) & ( b . n = 0 implies b₄ . b = p . ((0,n) -cut b) ) ) );

theorem Th6: :: HILB10_2:6

for n being Nat
for b being bag of n
for L being non empty ZeroStr
for p being Series of n,L holds (p extended_by_0) . (b bag_extend 0) = p . b

proof end;

theorem Th7: :: HILB10_2:7

for n being Nat
for L being non empty ZeroStr
for p being Series of n,L
for b being bag of n + 1 st b in Support (p extended_by_0) holds
b . n = 0

proof end;

theorem Th8: :: HILB10_2:8

for n being Nat
for b being bag of n
for L being non empty ZeroStr
for p being Series of n,L holds
( b bag_extend 0 in Support (p extended_by_0) iff b in Support p )

proof end;

theorem Th9: :: HILB10_2:9

for n being Nat
for L being non empty ZeroStr
for p being Series of n,L
for b being bag of n + 1 st b . n = 0 holds
( b in Support (p extended_by_0) iff (0,n) -cut b in Support p )

proof end;

registration

let n be Nat;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;

cluster p extended_by_0 -> finite-Support ;

coherence
p extended_by_0 is finite-Support

proof end;

end;

theorem Th10: :: HILB10_2:10

for n being Nat
for L being non empty ZeroStr
for p being Series of n,L holds {(0. L)} \/ (rng p) = rng (p extended_by_0)

proof end;

theorem Th11: :: HILB10_2:11

for n being Nat
for b being bag of n holds support b = support (b bag_extend 0)

proof end;

theorem Th12: :: HILB10_2:12

for n being Nat
for b being bag of n holds SgmX ((RelIncl n),(support b)) = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))

proof end;

theorem Th13: :: HILB10_2:13

for n being Nat
for b being bag of n
for L being non trivial well-unital doubleLoopStr
for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (b,x) = eval ((b bag_extend 0),y)

proof end;

theorem Th14: :: HILB10_2:14

for k, n being Nat
for b1, b2 being bag of n holds
( b1 < b2 iff b1 bag_extend k < b2 bag_extend k )

proof end;

theorem :: HILB10_2:15

for X being non empty set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for i, k being Nat st 1 <= i & i <= k & k <= card A holds
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i

proof end;

theorem Th16: :: HILB10_2:16

for n, m being Nat
for O being Ordinal
for A being finite Subset of (Bags O) st n in dom (SgmX ((BagOrder O),A)) & m in dom (SgmX ((BagOrder O),A)) & n < m holds
(SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m

proof end;

theorem Th17: :: HILB10_2:17

for n being Nat
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L holds
( len (SgmX ((BagOrder n),(Support p))) = len (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) & ( for i being Nat st 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) holds
(SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 ) )

proof end;

theorem Th18: :: HILB10_2:18

for n being Nat
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L
for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (p,x) = eval ((p extended_by_0),y)

proof end;

theorem Th19: :: HILB10_2:19

for O being Ordinal
for L being non trivial associative commutative well-unital doubleLoopStr
for x being Function of O,L
for b being bag of O
for S being one-to-one FinSequence of O st rng S = support b holds
ex y being FinSequence of L st
( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )

proof end;

theorem Th20: :: HILB10_2:20

for O being Ordinal
for L being non trivial associative commutative well-unital doubleLoopStr
for x being Function of O,L
for b being bag of O
for perm being Permutation of O holds eval (b,x) = eval ((b * perm),(x * perm))

proof end;

definition

let O be Ordinal;
let L be non empty ZeroStr ;
let s be Series of O,L;
let perm be Permutation of O;

func s permuted_by perm -> Series of O,L means :Def4: :: HILB10_2:def 4
for b being bag of O holds it . b = s . (b * perm);

existence
ex b₁ being Series of O,L st
for b being bag of O holds b₁ . b = s . (b * perm)

proof end;

uniqueness
for b₁, b₂ being Series of O,L st ( for b being bag of O holds b₁ . b = s . (b * perm) ) & ( for b being bag of O holds b₂ . b = s . (b * perm) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines permuted_by HILB10_2:def 4 :
for O being Ordinal
for L being non empty ZeroStr
for s being Series of O,L
for perm being Permutation of O
for b₅ being Series of O,L holds
( b₅ = s permuted_by perm iff for b being bag of O holds b₅ . b = s . (b * perm) );

theorem Th21: :: HILB10_2:21

for O being Ordinal
for L being non empty ZeroStr
for perm being Permutation of O
for s being Series of O,L
for b being bag of O holds
( b in Support (s permuted_by perm) iff b * perm in Support s )

proof end;

theorem Th22: :: HILB10_2:22

for O being Ordinal
for L being non empty ZeroStr
for perm being Permutation of O
for s being Series of O,L
for b being bag of O holds
( b * (perm ") in Support (s permuted_by perm) iff b in Support s )

proof end;

theorem Th23: :: HILB10_2:23

for O being Ordinal
for L being non empty ZeroStr
for perm being Permutation of O
for s being Series of O,L holds card (Support s) = card (Support (s permuted_by perm))

proof end;

theorem Th24: :: HILB10_2:24

for O being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of O,L
for x being Function of O,L
for S being one-to-one FinSequence of Bags O st rng S = Support p holds
ex y being FinSequence of L st
( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )

proof end;

registration

let O be Ordinal;
let L be non empty ZeroStr ;
let perm be Permutation of O;
let p be Polynomial of O,L;

cluster p permuted_by perm -> finite-Support ;

coherence
p permuted_by perm is finite-Support

proof end;

end;

theorem Th25: :: HILB10_2:25

for O being Ordinal
for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of O,L
for x being Function of O,L
for perm being Permutation of O holds eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))

proof end;

theorem Th26: :: HILB10_2:26

for O being Ordinal
for L being non empty ZeroStr
for s being Series of O,L
for perm being Permutation of O holds rng (s permuted_by perm) = rng s

proof end;

theorem Th27: :: HILB10_2:27

for n, m being Nat
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) )

proof end;

theorem Th28: :: HILB10_2:28

for k, n, m being Nat
for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of (n + m),L ex q being Polynomial of ((n + k) + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for XY being Function of (n + m),L
for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds
eval (p,XY) = eval (q,XanyY) ) )

proof end;

definition

let D be non empty set ;
let n be Nat;

func n -xtuples_of D -> Subset of (D ^omega) means :Def5: :: HILB10_2:def 5
for x being object holds
( x in it iff x is n -element XFinSequence of D );

existence
ex b₁ being Subset of (D ^omega) st
for x being object holds
( x in b₁ iff x is n -element XFinSequence of D )

proof end;

uniqueness
for b₁, b₂ being Subset of (D ^omega) st ( for x being object holds
( x in b₁ iff x is n -element XFinSequence of D ) ) & ( for x being object holds
( x in b₂ iff x is n -element XFinSequence of D ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines -xtuples_of HILB10_2:def 5 :
for D being non empty set
for n being Nat
for b₃ being Subset of (D ^omega) holds
( b₃ = n -xtuples_of D iff for x being object holds
( x in b₃ iff x is b₂ -element XFinSequence of D ) );

registration

let D be non empty set ;
let n be Nat;

cluster n -xtuples_of D -> non empty ;

coherence
not n -xtuples_of D is empty

proof end;

cluster -> D -valued n -element for Element of n -xtuples_of D;

coherence
for b₁ being Element of n -xtuples_of D holds
( b₁ is n -element & b₁ is D -valued ) by Def5;

end;

definition

let n be Nat;
let A be Subset of (n -xtuples_of NAT);

attr A is diophantine means :Def6: :: HILB10_2:def 6
ex m being Nat ex p being INT -valued Polynomial of (n + m),F_Real st
for s being object holds
( s in A iff ex x being n -element XFinSequence of NAT ex y being b₁ -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) );

end;

:: deftheorem Def6 defines diophantine HILB10_2:def 6 :
for n being Nat
for A being Subset of (n -xtuples_of NAT) holds
( A is diophantine iff ex m being Nat ex p being INT -valued Polynomial of (n + m),F_Real st
for s being object holds
( s in A iff ex x being b₁ -element XFinSequence of NAT ex y being b₃ -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) ) );

registration

let n be Nat;

cluster empty -> diophantine for Element of K27((n -xtuples_of NAT));

coherence
for b₁ being Subset of (n -xtuples_of NAT) st b₁ is empty holds
b₁ is diophantine

proof end;

cluster [#] (n -xtuples_of NAT) -> diophantine ;

coherence
[#] (n -xtuples_of NAT) is diophantine

proof end;

end;

registration

let n be zero Nat;

cluster -> diophantine for Element of K27((n -xtuples_of NAT));

coherence
for b₁ being Subset of (n -xtuples_of NAT) holds b₁ is diophantine

proof end;

end;

registration

let n be Nat;

cluster functional non empty diophantine for Element of K27((n -xtuples_of NAT));

existence
ex b₁ being Subset of (n -xtuples_of NAT) st
( not b₁ is empty & b₁ is diophantine )

proof end;

cluster functional empty diophantine for Element of K27((n -xtuples_of NAT));

existence
ex b₁ being Subset of (n -xtuples_of NAT) st
( b₁ is empty & b₁ is diophantine )

proof end;

end;

registration

let n be Nat;
let A, B be diophantine Subset of (n -xtuples_of NAT);

cluster A /\ B -> diophantine for Subset of (n -xtuples_of NAT);

coherence
for b₁ being Subset of (n -xtuples_of NAT) st b₁ = A /\ B holds
b₁ is diophantine

proof end;

cluster A \/ B -> diophantine for Subset of (n -xtuples_of NAT);

coherence
for b₁ being Subset of (n -xtuples_of NAT) st b₁ = A \/ B holds
b₁ is diophantine

proof end;

end;