:: 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 b1 being XFinSequence of X st b1 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 b1 being XFinSequence st
( b1 is n -element & b1 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 b1 -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 b1 -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 b1 being Series of X,F_Real st b1 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 b1 being Polynomial of O,F_Real st b1 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 b1 being Function of X,F_Real st b1 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 b1 being Function of O,F_Real st b1 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 b1 being Series of (n + 1),L st
for b being bag of n + 1 holds
( ( b . n <> 0 implies b1 . b = 0. L ) & ( b . n = 0 implies b1 . b = p . ((0,n) -cut b) ) )
proof end;
uniqueness
for b1, b2 being Series of (n + 1),L st ( for b being bag of n + 1 holds
( ( b . n <> 0 implies b1 . b = 0. L ) & ( b . n = 0 implies b1 . b = p . ((0,n) -cut b) ) ) ) & ( for b being bag of n + 1 holds
( ( b . n <> 0 implies b2 . b = 0. L ) & ( b . n = 0 implies b2 . b = p . ((0,n) -cut b) ) ) ) holds
b1 = b2
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 b4 being Series of (n + 1),L holds
( b4 = p extended_by_0 iff for b being bag of n + 1 holds
( ( b . n <> 0 implies b4 . b = 0. L ) & ( b . n = 0 implies b4 . 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 b1 being Series of O,L st
for b being bag of O holds b1 . b = s . (b * perm)
proof end;
uniqueness
for b1, b2 being Series of O,L st ( for b being bag of O holds b1 . b = s . (b * perm) ) & ( for b being bag of O holds b2 . b = s . (b * perm) ) holds
b1 = b2
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 b5 being Series of O,L holds
( b5 = s permuted_by perm iff for b being bag of O holds b5 . 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 b1 being Subset of (D ^omega) st
for x being object holds
( x in b1 iff x is n -element XFinSequence of D )
proof end;
uniqueness
for b1, b2 being Subset of (D ^omega) st ( for x being object holds
( x in b1 iff x is n -element XFinSequence of D ) ) & ( for x being object holds
( x in b2 iff x is n -element XFinSequence of D ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines -xtuples_of HILB10_2:def 5 :
for D being non empty set
for n being Nat
for b3 being Subset of (D ^omega) holds
( b3 = n -xtuples_of D iff for x being object holds
( x in b3 iff x is b2 -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 b1 being Element of n -xtuples_of D holds
( b1 is n -element & b1 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 b1 -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 b1 -element XFinSequence of NAT ex y being b3 -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 b1 being Subset of (n -xtuples_of NAT) st b1 is empty holds
b1 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 b1 being Subset of (n -xtuples_of NAT) holds b1 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 b1 being Subset of (n -xtuples_of NAT) st
( not b1 is empty & b1 is diophantine )
proof end;
cluster functional empty diophantine for Element of K27((n -xtuples_of NAT));
existence
ex b1 being Subset of (n -xtuples_of NAT) st
( b1 is empty & b1 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 b1 being Subset of (n -xtuples_of NAT) st b1 = A /\ B holds
b1 is diophantine
proof end;
cluster A \/ B -> diophantine for Subset of (n -xtuples_of NAT);
coherence
for b1 being Subset of (n -xtuples_of NAT) st b1 = A \/ B holds
b1 is diophantine
proof end;
end;