:: Diophantine sets -- Preliminaries :: by Karol P\kak :: :: Received March 27, 2018 :: Copyright (c) 2018-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0, BINOP_1, FUNCT_1, FINSOP_1, XXREAL_0, TARSKI, NAT_1, INT_1, ARYTM_3, ORDERS_1, FINSET_1, ZFMISC_1, CARD_1, PARTFUN1, ORDINAL1, RELAT_2, ARYTM_1, FUNCOP_1, PBOOLE, CARD_3, VALUED_0, FUNCT_2, PRE_POLY, XCMPLX_0, WELLORD2, QC_LANG1, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES, STRUCT_0, SUPINF_2, MESFUNC1, RFINSEQ, POLYNOM1, ALGSEQ_1, POLYNOM2, HILBASIS, GRAPH_2, AFINSQ_1, HILB10_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1, XXREAL_0, XCMPLX_0, RELAT_2, FUNCT_1, PBOOLE, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, FINSOP_1, FINSEQ_1, FUNCT_3, BINOP_1, XREAL_0, ORDERS_1, FUNCOP_1, NAT_1, INT_1, VALUED_0, FINSEQOP, ALGSTR_0, RLVECT_1, VFUNCT_1, VECTSP_1, GROUP_1, GROUP_4, RECDEF_1, PRE_POLY, POLYNOM1, POLYNOM2, BAGORDER, HILBASIS, AFINSQ_1, AFINSQ_2, STRUCT_0; constructors SETWISEO, FINSEQOP, FINSOP_1, RFUNCT_3, RECDEF_1, BINOP_2, CLASSES1, RELSET_1, DOMAIN_1, GROUP_4, VFUNCT_1, POLYNOM2, BAGORDER, HILBASIS, AFINSQ_2; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, VALUED_0, RELSET_1, FUNCT_2, INT_1, RFUNCT_2, STRUCT_0, VECTSP_1, POLYNOM1, PRE_POLY, VFUNCT_1, MEMBERED, PRE_CIRC, POLYNOM2, GROUP_1, FVSUM_1, AFINSQ_2, HILBASIS, BAGORDER, AFINSQ_1, NUMBERS; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve i,j,k,n,m for Nat, b,b1,b2 for bag of n; registration let X be non empty set; let n be Nat; cluster n-element for XFinSequence of X; end; registration let n be Nat; cluster n-element real-valued for XFinSequence; 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; end; registration let p be real-valued XFinSequence; let q be real-valued XFinSequence; cluster p^q -> real-valued; 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; end; 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; end; registration let X be set, p be Permutation of X, M be ManySortedSet of X; cluster M * p -> total; end; registration let F be finite-support Function; let f be one-to-one Function; cluster F*f -> finite-support; end; theorem :: HILB10_2:1 for F, G being XFinSequence st F^G is one-to-one holds rng F misses rng G; theorem :: HILB10_2:2 for X being set, f being X-defined Function, perm being Permutation of X holds card support (f*perm) = card support (f); registration let X be set; cluster 0_(X, F_Real) -> natural-valued; cluster 1_(X, F_Real) -> natural-valued; end; registration let X be set; let x be Element of X; cluster 1_1(x,F_Real) -> natural-valued; end; registration let X be set; cluster INT -valued for Series of X,F_Real; end; registration let O be Ordinal; cluster INT -valued for Polynomial of O,F_Real; end; registration let X be set, p be INT -valued Series of X, F_Real; cluster -p -> INT -valued; let q be INT -valued Series of X, F_Real; cluster p+q ->INT -valued; cluster p-q ->INT -valued; end; registration let X be Ordinal, p,q be INT -valued Series of X, F_Real; cluster p *' q ->INT -valued; end; registration let X be set; cluster natural-valued for Function of X, F_Real; end; registration let O be Ordinal; cluster INT -valued for Function of O, F_Real; 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; 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; end; begin :: Polynomial extended by 0 theorem :: HILB10_2:3 for b being ManySortedSet of n st k <= n holds (0,k)-cut b = b|k; theorem :: HILB10_2:4 for b being bag of (n+1) holds b = (0,n)-cut b bag_extend (b.n); theorem :: HILB10_2:5 (0,n)-cut (b bag_extend k) = b; definition let n; let L be non empty ZeroStr; let p be Series of n,L; func p extended_by_0 -> Series of n+1,L means :: 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); end; theorem :: HILB10_2:6 for L being non empty ZeroStr, p being Series of n,L holds (p extended_by_0).(b bag_extend 0) = p.b; theorem :: HILB10_2:7 for L being non empty ZeroStr, p being Series of n,L, b being bag of n+1 st b in Support (p extended_by_0) holds b.n = 0; theorem :: HILB10_2:8 for L being non empty ZeroStr, p being Series of n,L holds b bag_extend 0 in Support (p extended_by_0) iff b in Support p; theorem :: HILB10_2:9 for L being non empty ZeroStr, p being Series of n,L, 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; registration let n; let L be non empty ZeroStr; let p be Polynomial of n,L; cluster p extended_by_0 -> finite-Support; end; theorem :: HILB10_2:10 for L being non empty ZeroStr, p being Series of n,L holds {0.L} \/ rng p = rng (p extended_by_0); theorem :: HILB10_2:11 support b = support (b bag_extend 0); theorem :: HILB10_2:12 SgmX(RelIncl n, support b) = SgmX(RelIncl (n+1), support (b bag_extend 0)); theorem :: HILB10_2:13 for L being well-unital non trivial doubleLoopStr for x being Function of n, L, y be Function of n+1,L st y|n = x holds eval(b,x) = eval(b bag_extend 0,y); theorem :: HILB10_2:14 b1 < b2 iff b1 bag_extend k < b2 bag_extend k; theorem :: HILB10_2:15 for X being non empty set, A being finite Subset of X, R being Order of X st R linearly_orders A for i,k st 1 <= i <= k <= card A holds SgmX(R, rng (SgmX(R,A)|k))/.i = SgmX(R,A)/.i; theorem :: HILB10_2:16 for O being Ordinal, 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; theorem :: HILB10_2:17 for L being right_zeroed add-associative right_complementable well-unital distributive non trivial 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 be Nat st 1<=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; theorem :: HILB10_2:18 for L being right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p being Polynomial of n,L, x being Function of n, L, y being Function of (n+1), L st y|n=x holds eval(p,x) = eval(p extended_by_0,y); begin :: Polynomial permuted by perm theorem :: HILB10_2:19 for O being Ordinal, L being well-unital commutative associative non trivial doubleLoopStr, x being Function of O, L, b being bag of O for S being one-to-one FinSequence of O st rng S = support b ex y being FinSequence of L st len y = card support b & eval(b,x) = Product y & for i st 1 <= i & i <= len y holds y/.i = power(L).((x*S)/.i, (b*S)/.i); theorem :: HILB10_2:20 for O being Ordinal, L being well-unital commutative associative non trivial doubleLoopStr, x being Function of O, L, b being bag of O for perm being Permutation of O holds eval(b,x) = eval(b*perm,x*perm); 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 :: HILB10_2:def 4 for b being bag of O holds it.b = s.(b*perm); end; theorem :: HILB10_2:21 for O being Ordinal, L being non empty ZeroStr, perm being Permutation of O, s being Series of O,L, b being bag of O holds b in Support (s permuted_by perm) iff b*perm in Support s; theorem :: HILB10_2:22 for O being Ordinal, L being non empty ZeroStr, perm being Permutation of O, s being Series of O,L, b being bag of O holds b*perm" in Support (s permuted_by perm) iff b in Support s; theorem :: HILB10_2:23 for O being Ordinal, L being non empty ZeroStr, perm being Permutation of O, s being Series of O,L holds card Support s = card Support (s permuted_by perm); theorem :: HILB10_2:24 for O being Ordinal, L being Abelian right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p being Polynomial of O,L, x being Function of O, L for S being one-to-one FinSequence of Bags O st rng S = Support p 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); 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; end; theorem :: HILB10_2:25 for O being Ordinal, L being Abelian right_zeroed add-associative right_complementable well-unital distributive commutative associative non trivial doubleLoopStr, p being Polynomial of O,L, x being Function of O, L for perm being Permutation of O holds eval(p,x) = eval(p permuted_by perm,x*perm"); theorem :: HILB10_2:26 for O being Ordinal, L being non empty ZeroStr, s being Series of O,L, perm being Permutation of O holds rng (s permuted_by perm) = rng s; begin :: Main Lemmas theorem :: HILB10_2:27 for L being right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, 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, y being Function of (n+m), L st y|n=x holds eval(p,x) = eval(q,y); theorem :: HILB10_2:28 for L being Abelian right_zeroed add-associative right_complementable well-unital distributive commutative associative non trivial doubleLoopStr, 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, 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); begin :: Diophantine Sets reserve x,s for object; definition let D be non empty set; let n be Nat; func n -xtuples_of D -> Subset of D^omega means :: HILB10_2:def 5 x in it iff x is n-element XFinSequence of D; end; registration let D be non empty set; let n be Nat; cluster n -xtuples_of D -> non empty; cluster -> n-element D-valued for Element of n -xtuples_of D; end; definition let n be Nat; let A be Subset of n -xtuples_of NAT; attr A is diophantine means :: HILB10_2:def 6 ex m being Nat, p being INT -valued Polynomial of n+m,F_Real st for s holds s in A iff ex x being n-element XFinSequence of NAT, y being m-element XFinSequence of NAT st s = x & eval(p,@(x^y)) = 0; end; registration let n be Nat; cluster empty -> diophantine for Subset of n-xtuples_of NAT; cluster [#](n-xtuples_of NAT) -> diophantine; end; registration let n be zero Nat; cluster -> diophantine for Subset of n -xtuples_of NAT; end; registration let n be Nat; cluster non empty diophantine for Subset of n-xtuples_of NAT; cluster empty diophantine for Subset of n-xtuples_of NAT; 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; cluster A \/ B -> diophantine for Subset of n -xtuples_of NAT; end;