P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mtyf 29101	The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- F = (mVT ` T )   &    |- Y = (mType ` T )   =>    |- ( T e. mFS -> Y : V --> F )
Theorem	mvtss 29102	The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- F = (mVT ` T )   &    |- K = (mTC ` T )   =>    |- ( T e. mFS -> F C_ K )
Theorem	maxsta 29103	An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- A = (mAx ` T )   &    |- S = (mStat ` T )   =>    |- ( T e. mFS -> A C_ S )
Theorem	mvtinf 29104	Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- F = (mVT ` T )   &    |- Y = (mType ` T )   =>    |- ( ( T e. mFS /\ X e. F ) -> -. ( `' Y " { X } ) e. Fin )
Theorem	msubff1 29105	When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   &    |- E = (mEx ` T )   =>    |- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( E ^m E ) )
Theorem	msubff1o 29106	When restricted to complete mappings, the substitution-producing function is bijective to the set of all substitutions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   =>    |- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S )
Theorem	mvhf 29107	The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- E = (mEx ` T )   &    |- H = (mVH ` T )   =>    |- ( T e. mFS -> H : V --> E )
Theorem	mvhf1 29108	The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- E = (mEx ` T )   &    |- H = (mVH ` T )   =>    |- ( T e. mFS -> H : V -1-1-> E )
Theorem	msubvrs 29109*	The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mSubst ` T )   &    |- E = (mEx ` T )   &    |- V = (mVars ` T )   &    |- H = (mVH ` T )   =>    |- ( ( T e. mFS /\ F e. ran S /\ X e. E ) -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) )
Theorem	mclsrcl 29110	Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   =>    |- ( A e. ( K C B ) -> ( T e. _V /\ K C_ D /\ B C_ E ) )
Theorem	mclsssvlem 29111*	Lemma for mclsssv 29113. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- H = (mVH ` T )   &    |- A = (mAx ` T )   &    |- S = (mSubst ` T )   &    |- V = (mVars ` T )   =>    |- ( ph -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ E )
Theorem	mclsval 29112*	The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- H = (mVH ` T )   &    |- A = (mAx ` T )   &    |- S = (mSubst ` T )   &    |- V = (mVars ` T )   =>    |- ( ph -> ( K C B ) = |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
Theorem	mclsssv 29113	The closure of a set of expressions is a set of expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   =>    |- ( ph -> ( K C B ) C_ E )
Theorem	ssmclslem 29114	Lemma for ssmcls 29116. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- H = (mVH ` T )   =>    |- ( ph -> ( B u. ran H ) C_ ( K C B ) )
Theorem	vhmcls 29115	All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- H = (mVH ` T )   &    |- V = (mVR ` T )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( H ` X ) e. ( K C B ) )
Theorem	ssmcls 29116	The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   =>    |- ( ph -> B C_ ( K C B ) )
Theorem	ss2mcls 29117	The closure is monotonic under subsets of the original set of expressions and the set of disjoint variable conditions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- ( ph -> X C_ K )   &    |- ( ph -> Y C_ B )   =>    |- ( ph -> ( X C Y ) C_ ( K C B ) )
Theorem	mclsax 29118*	The closure is closed under axiom application. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- A = (mAx ` T )   &    |- L = (mSubst ` T )   &    |- V = (mVR ` T )   &    |- H = (mVH ` T )   &    |- W = (mVars ` T )   &    |- ( ph -> <. M , O , P >. e. A )   &    |- ( ph -> S e. ran L )   &    |- ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )   &    |- ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )   &    |- ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )   =>    |- ( ph -> ( S ` P ) e. ( K C B ) )
Theorem	mclsind 29119*	Induction theorem for closure: any other set Q closed under the axioms and the hypotheses contains all the elements of the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- A = (mAx ` T )   &    |- L = (mSubst ` T )   &    |- V = (mVR ` T )   &    |- H = (mVH ` T )   &    |- W = (mVars ` T )   &    |- ( ph -> B C_ Q )   &    |- ( ( ph /\ v e. V ) -> ( H ` v ) e. Q )   &    |- ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. Q )   =>    |- ( ph -> ( K C B ) C_ Q )
Theorem	mppspstlem 29120*	Lemma for mppspst 29123. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- J = (mPPSt ` T )   &    |- C = (mCls ` T )   =>    |- { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } C_ P
Theorem	mppsval 29121*	Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- J = (mPPSt ` T )   &    |- C = (mCls ` T )   =>    |- J = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) }
Theorem	elmpps 29122	Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- J = (mPPSt ` T )   &    |- C = (mCls ` T )   =>    |- ( <. D , H , A >. e. J <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) )
Theorem	mppspst 29123	A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- J = (mPPSt ` T )   =>    |- J C_ P
Theorem	mthmval 29124	A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. Unlike the difference between pre-statement and statement, this application of the reduct is not necessarily trivial: there are theorems that are not themselves provable but are provable once enough "dummy variables" are introduced. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- J = (mPPSt ` T )   &    |- U = (mThm ` T )   =>    |- U = ( `' R " ( R " J ) )
Theorem	elmthm 29125*	A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- J = (mPPSt ` T )   &    |- U = (mThm ` T )   =>    |- ( X e. U <-> E. x e. J ( R ` x ) = ( R ` X ) )
Theorem	mthmi 29126	A statement whose reduct is the reduct of a provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- J = (mPPSt ` T )   &    |- U = (mThm ` T )   =>    |- ( ( X e. J /\ ( R ` X ) = ( R ` Y ) ) -> Y e. U )
Theorem	mthmsta 29127	A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- U = (mThm ` T )   &    |- S = (mPreSt ` T )   =>    |- U C_ S
Theorem	mppsthm 29128	A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- J = (mPPSt ` T )   &    |- U = (mThm ` T )   =>    |- J C_ U
Theorem	mthmblem 29129	Lemma for mthmb 29130. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- U = (mThm ` T )   =>    |- ( ( R ` X ) = ( R ` Y ) -> ( X e. U -> Y e. U ) )
Theorem	mthmb 29130	If two statements have the same reduct then one is a theorem iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- U = (mThm ` T )   =>    |- ( ( R ` X ) = ( R ` Y ) -> ( X e. U <-> Y e. U ) )
Theorem	mthmpps 29131	Given a theorem, there is an explicitly definable witnessing provable pre-statement for the provability of the theorem. (However, this pre-statement requires infinitely many DV conditions, which is sometimes inconvenient.) (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- J = (mPPSt ` T )   &    |- U = (mThm ` T )   &    |- D = (mDV ` T )   &    |- V = (mVars ` T )   &    |- Z = U. ( V " ( H u. { A } ) )   &    |- M = ( C u. ( D \ ( Z X. Z ) ) )   =>    |- ( T e. mFS -> ( <. C , H , A >. e. U <-> ( <. M , H , A >. e. J /\ ( R ` <. M , H , A >. ) = ( R ` <. C , H , A >. ) ) ) )
Theorem	mclsppslem 29132*	The closure is closed under application of provable pre-statements. (Compare mclsax 29118.) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- J = (mPPSt ` T )   &    |- L = (mSubst ` T )   &    |- V = (mVR ` T )   &    |- H = (mVH ` T )   &    |- W = (mVars ` T )   &    |- ( ph -> <. M , O , P >. e. J )   &    |- ( ph -> S e. ran L )   &    |- ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )   &    |- ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )   &    |- ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )   &    |- ( ph -> <. m , o , p >. e. (mAx ` T ) )   &    |- ( ph -> s e. ran L )   &    |- ( ph -> ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) )   &    |- ( ph -> A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) )   =>    |- ( ph -> ( s ` p ) e. ( `' S " ( K C B ) ) )
Theorem	mclspps 29133*	The closure is closed under application of provable pre-statements. (Compare mclsax 29118.) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- J = (mPPSt ` T )   &    |- L = (mSubst ` T )   &    |- V = (mVR ` T )   &    |- H = (mVH ` T )   &    |- W = (mVars ` T )   &    |- ( ph -> <. M , O , P >. e. J )   &    |- ( ph -> S e. ran L )   &    |- ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )   &    |- ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )   &    |- ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )   =>    |- ( ph -> ( S ` P ) e. ( K C B ) )
21.5.15  Grammatical formal systems
Syntax	cm0s 29134	Mapping expressions to statements.
class m0St
Syntax	cmsa 29135	The set of syntax axioms.
class mSA
Syntax	cmwgfs 29136	The set of weakly grammatical formal systems.
class mWGFS
Syntax	cmsy 29137	The syntax typecode function.
class mSyn
Syntax	cmesy 29138	The syntax typecode function for expressions.
class mESyn
Syntax	cmgfs 29139	The set of grammatical formal systems.
class mGFS
Syntax	cmtree 29140	The set of proof trees.
class mTree
Syntax	cmst 29141	The set of syntax trees.
class mST
Syntax	cmsax 29142	The indexing set for a syntax axiom.
class mSAX
Syntax	cmufs 29143	The set of unambiguous formal sytems.
class mUFS
Definition	df-m0s 29144	Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- m0St = ( a e. _V |-> <. (/) , (/) , a >. )
Definition	df-msa 29145*	Define the set of syntax axioms. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mSA = ( t e. _V |-> { a e. (mEx ` t ) | ( (m0St ` a ) e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` (mVR ` t ) ) ) } )
Definition	df-mwgfs 29146*	Define the set of weakly grammatical formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mWGFS = { t e. mFS | A. d A. h A. a ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) ) }
Definition	df-msyn 29147	Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mSyn = Slot 6
Definition	df-mtree 29148*	Define the set of proof trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mTree = ( t e. _V |-> ( d e. ~P (mDV ` t ) , h e. ~P (mEx ` t ) |-> |^| { r | ( A. e e. ran (mVH ` t ) e r <. (m0St ` e ) , (/) >. /\ A. e e. h e r <. ( (mStRed ` t ) ` <. d , h , e >. ) , (/) >. /\ A. m A. o A. p ( <. m , o , p >. e. (mAx ` t ) -> A. s e. ran (mSubst ` t ) ( A. x A. y ( x m y -> ( ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` x ) ) ) X. ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` y ) ) ) ) C_ d ) -> ( { ( s ` p ) } X. X_ e e. ( o u. ( (mVH ` t ) " U. ( (mVars ` t ) " ( o u. { p } ) ) ) ) ( r " { ( s ` e ) } ) ) C_ r ) ) ) } ) )
Definition	df-mst 29149	Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mST = ( t e. _V |-> ( ( (/) (mTree ` t ) (/) ) |` ( (mEx ` t ) |` (mVT ` t ) ) ) )
Definition	df-msax 29150*	Define the indexing set for a syntax axiom's representation in a tree. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mSAX = ( t e. _V |-> ( p e. (mSA ` t ) |-> ( (mVH ` t ) " ( (mVars ` t ) ` p ) ) ) )
Definition	df-mufs 29151	Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mUFS = { t e. mGFS | Fun (mST ` t ) }
21.5.16  Models of formal systems
Syntax	cmuv 29152	The universe of a model.
class mUV
Syntax	cmvl 29153	The set of valuations.
class mVL
Syntax	cmvsb 29154	Substitution for a valuation.
class mVSubst
Syntax	cmfsh 29155	The freshness relation of a model.
class mFresh
Syntax	cmfr 29156	The set of freshness relations.
class mFRel
Syntax	cmevl 29157	The evaluation function of a model.
class mEval
Syntax	cmdl 29158	The set of models.
class mMdl
Syntax	cusyn 29159	The syntax function applied to elements of the model.
class mUSyn
Syntax	cgmdl 29160	The set of models in a grammatical formal system.
class mGMdl
Syntax	cmitp 29161	The interpretation function of the model.
class mItp
Syntax	cmfitp 29162	The evaluation function derived from the interpretation.
class mFromItp
Definition	df-muv 29163	Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mUV = Slot 7
Definition	df-mfsh 29164	Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mFresh = Slot 8
Definition	df-mevl 29165	Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mEval = Slot 9
Definition	df-mvl 29166*	Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mVL = ( t e. _V |-> X_ v e. (mVR ` t ) ( (mUV ` t ) " { ( (mType ` t ) ` v ) } ) )
Definition	df-mvsb 29167*	Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mVSubst = ( t e. _V |-> { <. <. s , m >. , x >. | ( ( s e. ran (mSubst ` t ) /\ m e. (mVL ` t ) ) /\ A. v e. (mVR ` t ) m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) /\ x = ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) ) ) } )
Definition	df-mfrel 29168*	Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mFRel = ( t e. _V |-> { r e. ~P ( (mUV ` t ) X. (mUV ` t ) ) | ( `' r = r /\ A. c e. (mVT ` t ) A. w e. ( ~P (mUV ` t ) i^i Fin ) E. v e. ( (mUV ` t ) " { c } ) w C_ ( r " { v } ) ) } )
Definition	df-mdl 29169*	Define the set of models of a formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mMdl = { t e. mFS | [. (mUV ` t ) / u ]. [. (mEx ` t ) / x ]. [. (mVL ` t ) / v ]. [. (mEval ` t ) / n ]. [. (mFresh ` t ) / f ]. ( ( u C_ ( (mTC ` t ) X. _V ) /\ f e. (mFRel ` t ) /\ n e. ( u ^pm ( v X. (mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. (mVR ` t ) <. m , ( (mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. (mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran (mSubst ` t ) A. e e. (mEx ` t ) A. y ( <. s , m >. (mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( (mVars ` t ) ` e ) ) = ( p |` ( (mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( (mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) }
Definition	df-musyn 29170*	Define the syntax typecode function for the model universe. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mUSyn = ( t e. _V |-> ( v e. (mUV ` t ) |-> <. ( (mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. ) )
Definition	df-gmdl 29171*	Define the set of models of a grammatical formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mGMdl = { t e. (mGFS i^i mMdl ) | ( A. c e. (mTC ` t ) ( (mUV ` t ) " { c } ) C_ ( (mUV ` t ) " { ( (mSyn ` t ) ` c ) } ) /\ A. v e. (mUV ` c ) A. w e. (mUV ` c ) ( v (mFresh ` t ) w <-> v (mFresh ` t ) ( (mUSyn ` t ) ` w ) ) /\ A. m e. (mVL ` t ) A. e e. (mEx ` t ) ( (mEval ` t ) " { <. m , e >. } ) = ( ( (mEval ` t ) " { <. m , ( (mESyn ` t ) ` e ) >. } ) i^i ( (mUV ` t ) " { ( 1st ` e ) } ) ) ) }
Definition	df-mitp 29172*	Define the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mItp = ( t e. _V |-> ( a e. (mSA ` t ) |-> ( g e. X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) |-> ( iota x E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) ) ) ) ) )
Definition	df-mfitp 29173*	Define a function that produces the evaluation function, given the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mFromItp = ( t e. _V |-> ( f e. X_ a e. (mSA ` t ) ( ( (mUV ` t ) " { ( ( 1st ` t ) ` a ) } ) ^m X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) ) |-> ( iota_ n e. ( (mUV ` t ) ^pm ( (mVL ` t ) X. (mEx ` t ) ) ) A. m e. (mVL ` t ) ( A. v e. (mVR ` t ) <. m , ( (mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e (mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( (mVars ` t ) ` a ) |-> ( m n ( g ` ( (mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. (mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( (mESyn ` t ) ` e ) >. } ) i^i ( (mUV ` t ) " { ( 1st ` e ) } ) ) ) ) ) )
21.5.17  Splitting fields
Syntax	citr 29174	Integral subring of a ring.
class IntgRing
Syntax	ccpms 29175	Completion of a metric space.
class cplMetSp
Syntax	chlb 29176	Embeddings for a direct limit.
class HomLimB
Syntax	chlim 29177	Direct limit structure.
class HomLim
Syntax	cpfl 29178	Polynomial extension field.
class polyFld
Syntax	csf1 29179	Splitting field for a single polynomial (auxiliary).
class splitFld1
Syntax	csf 29180	Splitting field for a finite set of polynomials.
class splitFld
Syntax	cpsl 29181	Splitting field for a sequence of polynomials.
class polySplitLim
Definition	df-irng 29182*	Define the subring of elements of r integral over s in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- IntgRing = ( r e. _V , s e. _V |-> U_ f e. (Monic1p ` ( r ↾s s ) ) ( `' f " { ( 0g ` r ) } ) )
Definition	df-cplmet 29183*	A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- cplMetSp = ( w e. _V |-> [_ ( ( w ^s NN ) ↾s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } ) )
Definition	df-homlimb 29184*	The input to this function is a sequence (on NN) of homomorphisms F ( n ) : R ( n ) --> R ( n + 1 ). The resulting structure is the direct limit of the direct system so defined. This function returns the pair <. S , G >. where S is the terminal object and G is a sequence of functions such that G ( n ) : R ( n ) --> S and G ( n ) = F ( n ) o. G ( n + 1 ). (Contributed by Mario Carneiro, 2-Dec-2014.)
|- HomLimB = ( f e. _V |-> [_ U_ n e. NN ( { n } X. dom ( f ` n ) ) / v ]_ [_ |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) } / e ]_ <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >. )
Definition	df-homlim 29185*	The input to this function is a sequence (on NN) of structures R ( n ) and homomorphisms F ( n ) : R ( n ) --> R ( n + 1 ). The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014.)
|- HomLim = ( r e. _V , f e. _V |-> [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } ) )
Definition	df-plfl 29186*	Define the field extension that augments a field with the root of the given irreducible polynomial, and extends the norm if one exists and the extension is unique. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- polyFld = ( r e. _V , p e. _V |-> [_ (Poly1 ` r ) / s ]_ [_ ( (RSpan ` s ) ` { p } ) / i ]_ [_ ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_ <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >. )
Definition	df-sfl1 29187*	Temporary construction for the splitting field of a polynomial. The inputs are a field r and a polynomial p that we want to split, along with a tuple j in the same format as the output. The output is a tuple <. S , F >. where S is the splitting field and F is an injective homomorphism from the original field r. The function works by repeatedly finding the smallest monic irreducible factor, and extending the field by that factor using the polyFld construction. We keep track of a total order in each of the splitting fields so that we can pick an element definably without needing global choice. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- splitFld1 = ( r e. _V , j e. _V |-> ( p e. (Poly1 ` r ) |-> ( rec ( ( s e. _V , f e. _V |-> [_ ( mPoly ` s ) / m ]_ [_ { g e. ( (Monic1p ` s ) i^i (Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) ) , j ) ` ( card ` ( 1 ... ( r deg1 p ) ) ) ) ) )
Definition	df-sfl 29188*	Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple <. S , F >. where S is the totally ordered splitting field and F is an injective homomorphism from the original field r. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- splitFld = ( r e. _V , p e. _V |-> ( iota x E. f ( f Isom < , ( lt ` r ) ( ( 1 ... ( # ` p ) ) , p ) /\ x = ( seq 0 ( ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) ) , ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } ) ) ` ( # ` p ) ) ) ) )
Definition	df-psl 29189*	Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring r, a strict order on r, and a sequence p : NN --> ( ~P r i^i Fin ) of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- polySplitLim = ( r e. _V , p e. ( ( ~P ( Base ` r ) i^i Fin ) ^m NN ) |-> [_ ( 1st o. seq 0 ( ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. ) , ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } ) ) ) / f ]_ ( ( 1st o. ( f shift 1 ) ) HomLim ( 2nd o. f ) ) )
21.5.18  p-adic number fields
Syntax	czr 29190	Integral elements of a ring.
class ZRing
Syntax	cgf 29191	Galois finite field.
class GF
Syntax	cgfo 29192	Galois limit field.
class GF∞
Syntax	ceqp 29193	Equivalence relation for df-qp 29204.
class ~Qp
Syntax	crqp 29194	Equivalence relation representatives for df-qp 29204.
class /Qp
Syntax	cqp 29195	The set of p-adic rational numbers.
class Qp
Syntax	czp 29196	The set of p-adic integers. (Not to be confused with czn 18633.)
class Zp
Syntax	cqpa 29197	Algebraic completion of the p-adic rational numbers.
class _Qp
Syntax	ccp 29198	Metric completion of _Qp.
class Cp
Definition	df-zrng 29199	Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- ZRing = ( r e. _V |-> ( r IntgRing ran ( ZRHom ` r ) ) )
Definition	df-gf 29200*	Define the Galois finite field of order p ^ n. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- GF = ( p e. Prime , n e. NN |-> [_ (ℤ/nℤ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )