P. 357 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35601-35700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hlhilphllem 35601*	Lemma for hlhil 22475. (Contributed by NM, 23-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- F = (Scalar ` U )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` L )   &    |- .+ = ( +g ` L )   &    |- .x. = ( .s ` L )   &    |- R = (Scalar ` L )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- Q = ( 0g ` R )   &    |- .0. = ( 0g ` L )   &    |- ., = ( .i ` U )   &    |- J = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- E = ( x e. V , y e. V |-> ( ( J ` y ) ` x ) )   =>    |- ( ph -> U e. PreHil )
Theorem	hlhilhillem 35602*	Lemma for hlhil 22475. (Contributed by NM, 23-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- F = (Scalar ` U )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` L )   &    |- .+ = ( +g ` L )   &    |- .x. = ( .s ` L )   &    |- R = (Scalar ` L )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- Q = ( 0g ` R )   &    |- .0. = ( 0g ` L )   &    |- ., = ( .i ` U )   &    |- J = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- E = ( x e. V , y e. V |-> ( ( J ` y ) ` x ) )   &    |- O = ( ocv ` U )   &    |- C = ( CSubSp ` U )   =>    |- ( ph -> U e. Hil )
Theorem	hlathil 35603	Construction of a Hilbert space (df-hil 19344) U from a Hilbert lattice (df-hlat 32988) K, where W is a fixed but arbitrary hyperplane (co-atom) in K. The Hilbert space U is identical to the vector space ( ( DVecH ` K ) ` W ) (see dvhlvec 34748) except that it is extended with involution and inner product components. The construction of these two components is provided by Theorem 3.6 in [Holland95] p. 13, whose proof we follow loosely. An example of involution is the complex conjugate when the division ring is the field of complex numbers. The nature of the division ring we constructed is indeterminate, however, until we specialize the initial Hilbert lattice with additional conditions found by Maria Solèr in 1995 and refined by René Mayet in 1998 that result in a division ring isomorphic to CC. See additional discussion at http://us.metamath.org/qlegif/mmql.html#what. W corresponds to the w in the proof of Theorem 13.4 of [Crawley] p. 111. Such a W always exists since HL has lattice rank of at least 4 by df-hil 19344. It can be eliminated if we just want to show the existence of a Hilbert space, as is done in the literature. (Contributed by NM, 23-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> U e. Hil )
21.22  Mathbox for OpenAI
Theorem	rntrclfvOAI 35604	The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.)
|- ( R e. V -> ran ( t+ ` R ) = ran R )
21.23  Mathbox for Stefan O'Rear
21.23.1  Additional elementary logic and set theory
Theorem	moxfr 35605*	Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.)
|- A e. _V   &    |- E! y x = A   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( E* x ph <-> E* y ps )
21.23.2  Additional theory of functions
Theorem	imaiinfv 35606*	Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( F Fn A /\ B C_ A ) -> |^|_ x e. B ( F ` x ) = |^| ( F " B ) )
21.23.3  Additional topology
Theorem	elrfi 35607*	Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( B e. V /\ C C_ ~P B ) -> ( A e. ( fi ` ( { B } u. C ) ) <-> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) ) )
Theorem	elrfirn 35608*	Elementhood in a set of relative finite intersections of an indexed family of sets. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( B e. V /\ F : I --> ~P B ) -> ( A e. ( fi ` ( { B } u. ran F ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v ( F ` y ) ) ) )
Theorem	elrfirn2 35609*	Elementhood in a set of relative finite intersections of an indexed family of sets (implicit). (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( B e. V /\ A. y e. I C C_ B ) -> ( A e. ( fi ` ( { B } u. ran ( y e. I |-> C ) ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v C ) ) )
Theorem	cmpfiiin 35610*	In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- X = U. J   &    |- ( ph -> J e. Comp )   &    |- ( ( ph /\ k e. I ) -> S e. ( Clsd ` J ) )   &    |- ( ( ph /\ ( l C_ I /\ l e. Fin ) ) -> ( X i^i |^|_ k e. l S ) =/= (/) )   =>    |- ( ph -> ( X i^i |^|_ k e. I S ) =/= (/) )
21.23.4  Characterization of closure operators. Kuratowski closure axioms
Theorem	ismrcd1 35611*	Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 15601), isotone (satisfies mrcss 15600), and idempotent (satisfies mrcidm 15603) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 35612 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ph -> B e. V )   &    |- ( ph -> F : ~P B --> ~P B )   &    |- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )   =>    |- ( ph -> dom ( F i^i _I ) e. (Moore ` B ) )
Theorem	ismrcd2 35612*	Second half of ismrcd1 35611. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ph -> B e. V )   &    |- ( ph -> F : ~P B --> ~P B )   &    |- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )   =>    |- ( ph -> F = (mrCls ` dom ( F i^i _I ) ) )
Theorem	istopclsd 35613*	A closure function which satisfies sscls 20148, clsidm 20160, cls0 20173, and clsun 31055 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ph -> B e. V )   &    |- ( ph -> F : ~P B --> ~P B )   &    |- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )   &    |- ( ph -> ( F ` (/) ) = (/) )   &    |- ( ( ph /\ x C_ B /\ y C_ B ) -> ( F ` ( x u. y ) ) = ( ( F ` x ) u. ( F ` y ) ) )   &    |- J = { z e. ~P B | ( F ` ( B \ z ) ) = ( B \ z ) }   =>    |- ( ph -> ( J e. (TopOn ` B ) /\ ( cls ` J ) = F ) )
Theorem	ismrc 35614*	A function is a Moore closure operator iff it satisfies mrcssid 15601, mrcss 15600, and mrcidm 15603. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( F e. (mrCls " (Moore ` B ) ) <-> ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) )
21.23.5  Algebraic closure systems
Syntax	cnacs 35615	Class of Noetherian closure systems.
class NoeACS
Definition	df-nacs 35616*	Define a closure system of Noetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- NoeACS = ( x e. _V |-> { c e. (ACS ` x ) | A. s e. c E. g e. ( ~P x i^i Fin ) s = ( (mrCls ` c ) ` g ) } )
Theorem	isnacs 35617*	Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (NoeACS ` X ) <-> ( C e. (ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) )
Theorem	nacsfg 35618*	In a Noetherian-type closure system, all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (NoeACS ` X ) /\ S e. C ) -> E. g e. ( ~P X i^i Fin ) S = ( F ` g ) )
Theorem	isnacs2 35619	Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (NoeACS ` X ) <-> ( C e. (ACS ` X ) /\ ( F " ( ~P X i^i Fin ) ) = C ) )
Theorem	mrefg2 35620*	Slight variation on finite genration for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (Moore ` X ) -> ( E. g e. ( ~P X i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S = ( F ` g ) ) )
Theorem	mrefg3 35621*	Slight variation on finite genration for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ S e. C ) -> ( E. g e. ( ~P X i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S C_ ( F ` g ) ) )
Theorem	nacsacs 35622	A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( C e. (NoeACS ` X ) -> C e. (ACS ` X ) )
Theorem	isnacs3 35623*	A choice-free order equivalent to the Noetherian condition on a closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( C e. (NoeACS ` X ) <-> ( C e. (Moore ` X ) /\ A. s e. ~P C ( (toInc ` s ) e. Dirset -> U. s e. s ) ) )
Theorem	incssnn0 35624*	Transitivity induction of subsets, lemma for nacsfix 35625. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 /\ B e. ( ZZ>= ` A ) ) -> ( F ` A ) C_ ( F ` B ) )
Theorem	nacsfix 35625*	An increasing sequence of closed sets in a Noetherian-type closure system eventually fixates. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( ( C e. (NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> E. y e. NN0 A. z e. ( ZZ>= ` y ) ( F ` z ) = ( F ` y ) )
21.23.6  Miscellanea 1. Map utilities
Theorem	constmap 35626	A constant (represented without dummy variables) is an element of a function set. _Note: In the following development, we will be quite often quantifying over functions and points in N-dimensional space (which are equivalent to functions from an "index set"). Many of the following theorems exist to transfer standard facts about functions to elements of function sets._ (Contributed by Stefan O'Rear, 30-Aug-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- A e. _V   &    |- C e. _V   =>    |- ( B e. C -> ( A X. { B } ) e. ( C ^m A ) )
Theorem	mapco2g 35627	Renaming indexes in a tuple, with sethood as antecedents. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|- ( ( E e. _V /\ A e. ( B ^m C ) /\ D : E --> C ) -> ( A o. D ) e. ( B ^m E ) )
Theorem	mapco2 35628	Post-composition (renaming indexes) of a mapping viewed as a point. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- E e. _V   =>    |- ( ( A e. ( B ^m C ) /\ D : E --> C ) -> ( A o. D ) e. ( B ^m E ) )
Theorem	mapfzcons 35629	Extending a one-based mapping by adding a tuple at the end results in another mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- M = ( N + 1 )   =>    |- ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( A u. { <. M , C >. } ) e. ( B ^m ( 1 ... M ) ) )
Theorem	mapfzcons1 35630	Recover prefix mapping from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- M = ( N + 1 )   =>    |- ( A e. ( B ^m ( 1 ... N ) ) -> ( ( A u. { <. M , C >. } ) |` ( 1 ... N ) ) = A )
Theorem	mapfzcons1cl 35631	A nonempty mapping has a prefix. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- M = ( N + 1 )   =>    |- ( A e. ( B ^m ( 1 ... M ) ) -> ( A |` ( 1 ... N ) ) e. ( B ^m ( 1 ... N ) ) )
Theorem	mapfzcons2 35632	Recover added element from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- M = ( N + 1 )   =>    |- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( ( A u. { <. M , C >. } ) ` M ) = C )
21.23.7  Miscellanea for polynomials
Theorem	mptfcl 35633*	Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( t e. A |-> B ) : A --> C -> ( t e. A -> B e. C ) )
21.23.8  Multivariate polynomials over the integers
Syntax	cmzpcl 35634	Extend class notation to include pre-polynomial rings.
class mzPolyCld
Syntax	cmzp 35635	Extend class notation to include polynomial rings.
class mzPoly
Definition	df-mzpcl 35636*	Define the polynomially closed function rings over an arbitrary index set v. The set (mzPolyCld ` v ) contains all sets of functions from ( ZZ ^m v ) to ZZ which include all constants and projections and are closed under addition and multiplication. This is a "temporary" set used to define the polynomial function ring itself (mzPoly ` v ); see df-mzp 35637. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- mzPolyCld = ( v e. _V |-> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) | ( ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )
Definition	df-mzp 35637	Polynomials over ZZ with an arbitrary index set, that is, the smallest ring of functions containing all constant functions and all projections. This is almost the most general reasonable definition; to reach full generality, we would need to be able to replace ZZ with an arbitrary (semi-)ring (and a coordinate subring), but rings have not been defined yet. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- mzPoly = ( v e. _V |-> |^| (mzPolyCld ` v ) )
Theorem	mzpclval 35638*	Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPolyCld ` V ) = { p e. ~P ( ZZ ^m ( ZZ ^m V ) ) | ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )
Theorem	elmzpcl 35639*	Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> ( P e. (mzPolyCld ` V ) <-> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) ) )
Theorem	mzpclall 35640	The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp 35637 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. (mzPolyCld ` V ) )
Theorem	mzpcln0 35641	Corrolary of mzpclall 35640: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPolyCld ` V ) =/= (/) )
Theorem	mzpcl1 35642	Defining property 1 of a polynomially closed function set P: it contains all constant functions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. ZZ ) -> ( ( ZZ ^m V ) X. { F } ) e. P )
Theorem	mzpcl2 35643*	Defining property 2 of a polynomially closed function set P: it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` F ) ) e. P )
Theorem	mzpcl34 35644	Defining properties 3 and 4 of a polynomially closed function set P: it is closed under pointwise addition and multiplication. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> ( ( F oF + G ) e. P /\ ( F oF x. G ) e. P ) )
Theorem	mzpval 35645	Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPoly ` V ) = |^| (mzPolyCld ` V ) )
Theorem	dmmzp 35646	mzPoly is defined for all index sets which are sets. This is used with elfvdm 5905 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- dom mzPoly = _V
Theorem	mzpincl 35647	Polynomial closedness is a universal first-order property and passes to intersections. This is where the closure properties of the polynomial ring itself are proved. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPoly ` V ) e. (mzPolyCld ` V ) )
Theorem	mzpconst 35648	Constant functions are polynomial. See also mzpconstmpt 35653. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( V e. _V /\ C e. ZZ ) -> ( ( ZZ ^m V ) X. { C } ) e. (mzPoly ` V ) )
Theorem	mzpf 35649	A polynomial function is a function from the coordinate space to the integers. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( F e. (mzPoly ` V ) -> F : ( ZZ ^m V ) --> ZZ )
Theorem	mzpproj 35650*	A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( V e. _V /\ X e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` X ) ) e. (mzPoly ` V ) )
Theorem	mzpadd 35651	The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 35654. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. (mzPoly ` V ) /\ B e. (mzPoly ` V ) ) -> ( A oF + B ) e. (mzPoly ` V ) )
Theorem	mzpmul 35652	The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 35655. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. (mzPoly ` V ) /\ B e. (mzPoly ` V ) ) -> ( A oF x. B ) e. (mzPoly ` V ) )
Theorem	mzpconstmpt 35653*	A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 35654, mzpmulmpt 35655, mzpnegmpt 35657, mzpsubmpt 35656, mzpexpmpt 35658) can be used to build proofs that functions which are "manifestly polynomial", in the sense of being a maps-to containing constants, projections, and simple arithmetic operations, are actually polynomial functions. There is no mzpprojmpt because mzpproj 35650 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( V e. _V /\ C e. ZZ ) -> ( x e. ( ZZ ^m V ) |-> C ) e. (mzPoly ` V ) )
Theorem	mzpaddmpt 35654*	Sum of polynomial functions is polynomial. Maps-to version of mzpadd 35651. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A + B ) ) e. (mzPoly ` V ) )
Theorem	mzpmulmpt 35655*	Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 35655. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A x. B ) ) e. (mzPoly ` V ) )
Theorem	mzpsubmpt 35656*	The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A - B ) ) e. (mzPoly ` V ) )
Theorem	mzpnegmpt 35657*	Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> -u A ) e. (mzPoly ` V ) )
Theorem	mzpexpmpt 35658*	Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ D e. NN0 ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) e. (mzPoly ` V ) )
Theorem	mzpindd 35659*	"Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( ph /\ f e. ZZ ) -> ch )   &    |- ( ( ph /\ f e. V ) -> th )   &    |- ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> ze )   &    |- ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> si )   &    |- ( x = ( ( ZZ ^m V ) X. { f } ) -> ( ps <-> ch ) )   &    |- ( x = ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) -> ( ps <-> th ) )   &    |- ( x = f -> ( ps <-> ta ) )   &    |- ( x = g -> ( ps <-> et ) )   &    |- ( x = ( f oF + g ) -> ( ps <-> ze ) )   &    |- ( x = ( f oF x. g ) -> ( ps <-> si ) )   &    |- ( x = A -> ( ps <-> rh ) )   =>    |- ( ( ph /\ A e. (mzPoly ` V ) ) -> rh )
Theorem	mzpmfp 35660	Relationship between multivariate Z-polynomials and general multivariate polynomial functions. (Contributed by Stefan O'Rear, 20-Mar-2015.) (Revised by AV, 13-Jun-2019.)
|- (mzPoly ` I ) = ran ( I eval ℤring )
Theorem	mzpsubst 35661*	Substituting polynomials for the variables of a polynomial results in a polynomial. G is expected to depend on y and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( W e. _V /\ F e. (mzPoly ` V ) /\ A. y e. V G e. (mzPoly ` W ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( y e. V |-> ( G ` x ) ) ) ) e. (mzPoly ` W ) )
Theorem	mzprename 35662*	Simplified version of mzpsubst 35661 to simply relabel variables in a polynomial. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( W e. _V /\ F e. (mzPoly ` V ) /\ R : V --> W ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. R ) ) ) e. (mzPoly ` W ) )
Theorem	mzpresrename 35663*	A polynomial is a polynomial over all larger index sets. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
|- ( ( W e. _V /\ V C_ W /\ F e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x |` V ) ) ) e. (mzPoly ` W ) )
Theorem	mzpcompact2lem 35664*	Lemma for mzpcompact2 35665. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- B e. _V   =>    |- ( A e. (mzPoly ` B ) -> E. a e. Fin E. b e. (mzPoly ` a ) ( a C_ B /\ A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) ) )
Theorem	mzpcompact2 35665*	Polynomials are finitary objects and can only reference a finite number of variables, even if the index set is infinite. Thus, every polynomial can be expressed as a (uniquely minimal, although we do not prove that) polynomial on a finite number of variables, which is then extended by adding an arbitrary set of ignored variables. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( A e. (mzPoly ` B ) -> E. a e. Fin E. b e. (mzPoly ` a ) ( a C_ B /\ A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) ) )
21.23.9  Miscellanea for Diophantine sets 1
Theorem	coeq0i 35666	coeq0 5351 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( A o. B ) = (/) )
Theorem	fzsplit1nn0 35667	Split a finite 1-based set of integers in the middle, allowing either end to be empty ( ( 1 ... 0 )). (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( ( A e. NN0 /\ B e. NN0 /\ A <_ B ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) )
21.23.10  Diophantine sets 1: definitions
Syntax	cdioph 35668	Extend class notation to include the family of Diophantine sets.
class Dioph
Definition	df-dioph 35669*	A Diophantine set is a set of positive integers which is a projection of the zero set of some polynomial. This definition somewhat awkwardly mixes ZZ (via mzPoly) and NN0 (to define the zero sets); the former could be avoided by considering coincidence sets of NN0 polynomials at the cost of requiring two, and the second is driven by consistency with our mu-recursive functions and the requirements of the Davis-Putnam-Robinson-Matiyasevich proof. Both are avoidable at a complexity cost. In particular, it is a consequence of 4sq 14993 that implicitly restricting variables to NN0 adds no expressive power over allowing them to range over ZZ. While this definition stipulates a specific index set for the polynomials, there is actually flexibility here, see eldioph2b 35676. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- Dioph = ( n e. NN0 |-> ran ( k e. ( ZZ>= ` n ) , p e. (mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } ) )
Theorem	eldiophb 35670*	Initial expression of Diophantine property of a set. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- ( D e. (Dioph ` N ) <-> ( N e. NN0 /\ E. k e. ( ZZ>= ` N ) E. p e. (mzPoly ` ( 1 ... k ) ) D = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
Theorem	eldioph 35671*	Condition for a set to be Diophantine (unpacking existential quantifier). (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( N e. NN0 /\ K e. ( ZZ>= ` N ) /\ P e. (mzPoly ` ( 1 ... K ) ) ) -> { t | E. u e. ( NN0 ^m ( 1 ... K ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. (Dioph ` N ) )
Theorem	diophrw 35672*	Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014.)
|- ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> { a | E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) } = { a | E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) } )
Theorem	eldioph2lem1 35673*	Lemma for eldioph2 35675. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> E. d e. ( ZZ>= ` N ) E. e e. _V ( e : ( 1 ... d ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
Theorem	eldioph2lem2 35674*	Lemma for eldioph2 35675. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) -> E. c ( c : ( 1 ... A ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
Theorem	eldioph2 35675*	Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 35665. (Contributed by Stefan O'Rear, 8-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
|- ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. (mzPoly ` S ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. (Dioph ` N ) )
Theorem	eldioph2b 35676*	While Diophantine sets were defined to have a finite number of witness variables consequtively following the observable variables, this is not necessary; they can equivalently be taken to use any witness set ( S \ ( 1 ... N ) ). For instance, in diophin 35686 we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( A e. (Dioph ` N ) <-> E. p e. (mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
Theorem	eldiophelnn0 35677	Remove antecedent on B from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. (Dioph ` B ) -> B e. NN0 )
Theorem	eldioph3b 35678*	Define Diophantine sets in terms of polynomials with variables indexed by NN. This avoids a quantifier over the number of witness variables and will be easier to use than eldiophb 35670 in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. (Dioph ` N ) <-> ( N e. NN0 /\ E. p e. (mzPoly ` NN ) A = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
Theorem	eldioph3 35679*	Inference version of eldioph3b 35678 with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( N e. NN0 /\ P e. (mzPoly ` NN ) ) -> { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. (Dioph ` N ) )
21.23.11  Diophantine sets 2 miscellanea
Theorem	ellz1 35680	Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( B e. ZZ -> ( A e. ( ZZ \ ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ /\ A <_ B ) ) )
Theorem	lzunuz 35681	The union of a lower set of integers and an upper set of integers which abut or overlap is all of the integers. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) = ZZ )
Theorem	fz1eqin 35682	Express a one-based finite range as the intersection of lower integers with NN. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( N e. NN0 -> ( 1 ... N ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) )
Theorem	lzenom 35683	Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ om )
Theorem	elmapresaun 35684	fresaun 5766 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) e. ( C ^m ( A u. B ) ) )
Theorem	elmapresaunres2 35685	fresaunres2 5767 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` B ) = G )
21.23.12  Diophantine sets 2: union and intersection. Monotone Boolean algebra
Theorem	diophin 35686	If two sets are Diophantine, so is their intersection. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ( A e. (Dioph ` N ) /\ B e. (Dioph ` N ) ) -> ( A i^i B ) e. (Dioph ` N ) )
Theorem	diophun 35687	If two sets are Diophantine, so is their union. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ( A e. (Dioph ` N ) /\ B e. (Dioph ` N ) ) -> ( A u. B ) e. (Dioph ` N ) )
Theorem	eldiophss 35688	Diophantine sets are sets of tuples of nonnegative integers. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( A e. (Dioph ` B ) -> A C_ ( NN0 ^m ( 1 ... B ) ) )
21.23.13  Diophantine sets 3: construction
Theorem	diophrex 35689*	Projecting a Diophantine set by removing a coordinate results in a Diophantine set. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. (Dioph ` M ) ) -> { t | E. u e. S t = ( u |` ( 1 ... N ) ) } e. (Dioph ` N ) )
Theorem	eq0rabdioph 35690*	This is the first of a number of theorems which allow sets to be proven Diophantine by syntactic induction, and models the correspondence between Diophantine sets and monotone existential first-order logic. This first theorem shows that the zero set of an implicit polynomial is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = 0 } e. (Dioph ` N ) )
Theorem	eqrabdioph 35691*	Diophantine set builder for equality of polynomial expressions. Note that the two expressions need not be nonnegative; only variables are so constrained. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = B } e. (Dioph ` N ) )
Theorem	0dioph 35692	The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN0 -> (/) e. (Dioph ` A ) )
Theorem	vdioph 35693	The "universal" set (as large as possible given eldiophss 35688) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN0 -> ( NN0 ^m ( 1 ... A ) ) e. (Dioph ` A ) )
Theorem	anrabdioph 35694*	Diophantine set builder for conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps ) } e. (Dioph ` N ) )
Theorem	orrabdioph 35695*	Diophantine set builder for disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps ) } e. (Dioph ` N ) )
Theorem	3anrabdioph 35696*	Diophantine set builder for ternary conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. (Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps /\ ch ) } e. (Dioph ` N ) )
Theorem	3orrabdioph 35697*	Diophantine set builder for ternary disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. (Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps \/ ch ) } e. (Dioph ` N ) )
21.23.14  Diophantine sets 4 miscellanea
Theorem	2sbcrex 35698*	Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.)
|- ( [. A / a ]. [. B / b ]. E. c e. C ph <-> E. c e. C [. A / a ]. [. B / b ]. ph )
Theorem	sbcrexgOLD 35699*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) Obsolete as of 18-Aug-2018. Use sbcrex 3331 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) )
Theorem	2sbcrexOLD 35700*	Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6342 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( [. A / a ]. [. B / b ]. E. c e. C ph <-> E. c e. C [. A / a ]. [. B / b ]. ph )