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

registration
let X be non empty set ;
let n be Nat;
existence
ex b1 being XFinSequence of X st b1 is n -element
proof end;
end;

registration
let n be Nat;
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;
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 ()
proof end;

registration
let X be set ;
coherence
0_ (X,F_Real) is natural-valued
proof end;
coherence
1_ (X,F_Real) is natural-valued
proof end;
end;

registration
let X be set ;
let x be Element of X;
coherence
1_1 (x,F_Real) is natural-valued
proof end;
end;

registration
let X be set ;
existence
ex b1 being Series of X,F_Real st b1 is INT -valued
proof end;
end;

registration
let O be Ordinal;
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;
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 ;
existence
ex b1 being Function of X,F_Real st b1 is natural-valued
proof end;
end;

registration
let O be Ordinal;
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
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 . 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 () 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 () 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 () 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;
coherence
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 ()
proof end;

theorem Th11: :: HILB10_2:11
for n being Nat
for b being bag of n holds support b = support ()
proof end;

theorem Th12: :: HILB10_2:12
for n being Nat
for b being bag of n holds SgmX ((),()) = SgmX ((RelIncl (n + 1)),(support ()))
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 ((),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 ((),A)) & m in dom (SgmX ((),A)) & n < m holds
(SgmX ((),A)) /. n < (SgmX ((),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 ((),())) = len (SgmX ((BagOrder (n + 1)),())) & ( for i being Nat st 1 <= i & i <= len (SgmX ((),())) holds
(SgmX ((BagOrder (n + 1)),())) /. i = ((SgmX ((),())) /. 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 ((),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 () & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = () . (((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 () = 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 () & 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 () 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 () 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 () 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 () 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 ();
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 () 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(());
coherence
for b1 being Subset of () st b1 is empty holds
b1 is diophantine
proof end;
coherence
[#] () is diophantine
proof end;
end;

registration
let n be zero Nat;
cluster -> diophantine for Element of K27(());
coherence
for b1 being Subset of () holds b1 is diophantine
proof end;
end;

registration
let n be Nat;
cluster functional non empty diophantine for Element of K27(());
existence
ex b1 being Subset of () st
( not b1 is empty & b1 is diophantine )
proof end;
existence
ex b1 being Subset of () st
( b1 is empty & b1 is diophantine )
proof end;
end;

registration
let n be Nat;
let A, B be diophantine Subset of ();
cluster A /\ B -> diophantine for Subset of ();
coherence
for b1 being Subset of () st b1 = A /\ B holds
b1 is diophantine
proof end;
cluster A \/ B -> diophantine for Subset of ();
coherence
for b1 being Subset of () st b1 = A \/ B holds
b1 is diophantine
proof end;
end;