![]() |
Metamath
Proof Explorer Theorem List (p. 352 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mvtinf 35101 | Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΉ = (mVTβπ) & β’ π = (mTypeβπ) β β’ ((π β mFS β§ π β πΉ) β Β¬ (β‘π β {π}) β Fin) | ||
Theorem | msubff1 35102 | When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ (π β mFS β (π βΎ (π βm π)):(π βm π)β1-1β(πΈ βm πΈ)) | ||
Theorem | msubff1o 35103 | When restricted to complete mappings, the substitution-producing function is bijective to the set of all substitutions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) β β’ (π β mFS β (π βΎ (π βm π)):(π βm π)β1-1-ontoβran π) | ||
Theorem | mvhf 35104 | The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΈ = (mExβπ) & β’ π» = (mVHβπ) β β’ (π β mFS β π»:πβΆπΈ) | ||
Theorem | mvhf1 35105 | The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΈ = (mExβπ) & β’ π» = (mVHβπ) β β’ (π β mFS β π»:πβ1-1βπΈ) | ||
Theorem | msubvrs 35106* | 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.) |
β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mVarsβπ) & β’ π» = (mVHβπ) β β’ ((π β mFS β§ πΉ β ran π β§ π β πΈ) β (πβ(πΉβπ)) = βͺ π₯ β (πβπ)(πβ(πΉβ(π»βπ₯)))) | ||
Theorem | mclsrcl 35107 | Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) β β’ (π΄ β (πΎπΆπ΅) β (π β V β§ πΎ β π· β§ π΅ β πΈ)) | ||
Theorem | mclsssvlem 35108* | Lemma for mclsssv 35110. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π» = (mVHβπ) & β’ π΄ = (mAxβπ) & β’ π = (mSubstβπ) & β’ π = (mVarsβπ) β β’ (π β β© {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β πΈ) | ||
Theorem | mclsval 35109* | The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π» = (mVHβπ) & β’ π΄ = (mAxβπ) & β’ π = (mSubstβπ) & β’ π = (mVarsβπ) β β’ (π β (πΎπΆπ΅) = β© {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) | ||
Theorem | mclsssv 35110 | The closure of a set of expressions is a set of expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) β β’ (π β (πΎπΆπ΅) β πΈ) | ||
Theorem | ssmclslem 35111 | Lemma for ssmcls 35113. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π» = (mVHβπ) β β’ (π β (π΅ βͺ ran π») β (πΎπΆπ΅)) | ||
Theorem | vhmcls 35112 | All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π» = (mVHβπ) & β’ π = (mVRβπ) & β’ (π β π β π) β β’ (π β (π»βπ) β (πΎπΆπ΅)) | ||
Theorem | ssmcls 35113 | The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) β β’ (π β π΅ β (πΎπΆπ΅)) | ||
Theorem | ss2mcls 35114 | 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.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ (π β π β πΎ) & β’ (π β π β π΅) β β’ (π β (ππΆπ) β (πΎπΆπ΅)) | ||
Theorem | mclsax 35115* | The closure is closed under axiom application. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π΄ = (mAxβπ) & β’ πΏ = (mSubstβπ) & β’ π = (mVRβπ) & β’ π» = (mVHβπ) & β’ π = (mVarsβπ) & β’ (π β β¨π, π, πβ© β π΄) & β’ (π β π β ran πΏ) & β’ ((π β§ π₯ β π) β (πβπ₯) β (πΎπΆπ΅)) & β’ ((π β§ π£ β π) β (πβ(π»βπ£)) β (πΎπΆπ΅)) & β’ ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) β β’ (π β (πβπ) β (πΎπΆπ΅)) | ||
Theorem | mclsind 35116* | Induction theorem for closure: any other set π closed under the axioms and the hypotheses contains all the elements of the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π΄ = (mAxβπ) & β’ πΏ = (mSubstβπ) & β’ π = (mVRβπ) & β’ π» = (mVHβπ) & β’ π = (mVarsβπ) & β’ (π β π΅ β π) & β’ ((π β§ π£ β π) β (π»βπ£) β π) & β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) β β’ (π β (πΎπΆπ΅) β π) | ||
Theorem | mppspstlem 35117* | Lemma for mppspst 35120. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π½ = (mPPStβπ) & β’ πΆ = (mClsβπ) β β’ {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} β π | ||
Theorem | mppsval 35118* | Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π½ = (mPPStβπ) & β’ πΆ = (mClsβπ) β β’ π½ = {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} | ||
Theorem | elmpps 35119 | Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π½ = (mPPStβπ) & β’ πΆ = (mClsβπ) β β’ (β¨π·, π», π΄β© β π½ β (β¨π·, π», π΄β© β π β§ π΄ β (π·πΆπ»))) | ||
Theorem | mppspst 35120 | A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π½ = (mPPStβπ) β β’ π½ β π | ||
Theorem | mthmval 35121 | 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.) |
β’ π = (mStRedβπ) & β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) β β’ π = (β‘π β (π β π½)) | ||
Theorem | elmthm 35122* | A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) β β’ (π β π β βπ₯ β π½ (π βπ₯) = (π βπ)) | ||
Theorem | mthmi 35123 | A statement whose reduct is the reduct of a provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) β β’ ((π β π½ β§ (π βπ) = (π βπ)) β π β π) | ||
Theorem | mthmsta 35124 | A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mThmβπ) & β’ π = (mPreStβπ) β β’ π β π | ||
Theorem | mppsthm 35125 | A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) β β’ π½ β π | ||
Theorem | mthmblem 35126 | Lemma for mthmb 35127. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mThmβπ) β β’ ((π βπ) = (π βπ) β (π β π β π β π)) | ||
Theorem | mthmb 35127 | If two statements have the same reduct then one is a theorem iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mThmβπ) β β’ ((π βπ) = (π βπ) β (π β π β π β π)) | ||
Theorem | mthmpps 35128 | 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 disjoint variable conditions, which is sometimes inconvenient.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) & β’ π· = (mDVβπ) & β’ π = (mVarsβπ) & β’ π = βͺ (π β (π» βͺ {π΄})) & β’ π = (πΆ βͺ (π· β (π Γ π))) β β’ (π β mFS β (β¨πΆ, π», π΄β© β π β (β¨π, π», π΄β© β π½ β§ (π ββ¨π, π», π΄β©) = (π ββ¨πΆ, π», π΄β©)))) | ||
Theorem | mclsppslem 35129* | The closure is closed under application of provable pre-statements. (Compare mclsax 35115.) 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.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π½ = (mPPStβπ) & β’ πΏ = (mSubstβπ) & β’ π = (mVRβπ) & β’ π» = (mVHβπ) & β’ π = (mVarsβπ) & β’ (π β β¨π, π, πβ© β π½) & β’ (π β π β ran πΏ) & β’ ((π β§ π₯ β π) β (πβπ₯) β (πΎπΆπ΅)) & β’ ((π β§ π£ β π) β (πβ(π»βπ£)) β (πΎπΆπ΅)) & β’ ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) & β’ (π β β¨π, π, πβ© β (mAxβπ)) & β’ (π β π β ran πΏ) & β’ (π β (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) & β’ (π β βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β β’ (π β (π βπ) β (β‘π β (πΎπΆπ΅))) | ||
Theorem | mclspps 35130* | The closure is closed under application of provable pre-statements. (Compare mclsax 35115.) 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.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π½ = (mPPStβπ) & β’ πΏ = (mSubstβπ) & β’ π = (mVRβπ) & β’ π» = (mVHβπ) & β’ π = (mVarsβπ) & β’ (π β β¨π, π, πβ© β π½) & β’ (π β π β ran πΏ) & β’ ((π β§ π₯ β π) β (πβπ₯) β (πΎπΆπ΅)) & β’ ((π β§ π£ β π) β (πβ(π»βπ£)) β (πΎπΆπ΅)) & β’ ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) β β’ (π β (πβπ) β (πΎπΆπ΅)) | ||
Syntax | cm0s 35131 | Mapping expressions to statements. |
class m0St | ||
Syntax | cmsa 35132 | The set of syntax axioms. |
class mSA | ||
Syntax | cmwgfs 35133 | The set of weakly grammatical formal systems. |
class mWGFS | ||
Syntax | cmsy 35134 | The syntax typecode function. |
class mSyn | ||
Syntax | cmesy 35135 | The syntax typecode function for expressions. |
class mESyn | ||
Syntax | cmgfs 35136 | The set of grammatical formal systems. |
class mGFS | ||
Syntax | cmtree 35137 | The set of proof trees. |
class mTree | ||
Syntax | cmst 35138 | The set of syntax trees. |
class mST | ||
Syntax | cmsax 35139 | The indexing set for a syntax axiom. |
class mSAX | ||
Syntax | cmufs 35140 | The set of unambiguous formal sytems. |
class mUFS | ||
Definition | df-m0s 35141 | Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ m0St = (π β V β¦ β¨β , β , πβ©) | ||
Definition | df-msa 35142* | Define the set of syntax axioms. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mSA = (π‘ β V β¦ {π β (mExβπ‘) β£ ((m0Stβπ) β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘) β§ Fun (β‘(2nd βπ) βΎ (mVRβπ‘)))}) | ||
Definition | df-mwgfs 35143* | Define the set of weakly grammatical formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mWGFS = {π‘ β mFS β£ βπβββπ((β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) β βπ β ran (mSubstβπ‘)π β (π β (mSAβπ‘)))} | ||
Definition | df-msyn 35144 | Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mSyn = Slot 6 | ||
Definition | df-mesyn 35145* | Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023.) |
β’ mESyn = (π‘ β V β¦ (π β (mTCβπ‘), π β (mRExβπ‘) β¦ (((mSynβπ‘)βπ)m0Stπ))) | ||
Definition | df-mgfs 35146* | Define the set of grammatical formal systems. (Contributed by Mario Carneiro, 12-Jun-2023.) |
β’ mGFS = {π‘ β mWGFS β£ ((mSynβπ‘):(mTCβπ‘)βΆ(mVTβπ‘) β§ βπ β (mVTβπ‘)((mSynβπ‘)βπ) = π β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘)))} | ||
Definition | df-mtree 35147* | Define the set of proof trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mTree = (π‘ β V β¦ (π β π« (mDVβπ‘), β β π« (mExβπ‘) β¦ β© {π β£ (βπ β ran (mVHβπ‘)ππβ¨(m0Stβπ), β β© β§ βπ β β ππβ¨((mStRedβπ‘)ββ¨π, β, πβ©), β β© β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π) β ({(π βπ)} Γ Xπ β (π βͺ ((mVHβπ‘) β βͺ ((mVarsβπ‘) β (π βͺ {π}))))(π β {(π βπ)})) β π)))})) | ||
Definition | df-mst 35148 | Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mST = (π‘ β V β¦ ((β (mTreeβπ‘)β ) βΎ ((mExβπ‘) βΎ (mVTβπ‘)))) | ||
Definition | df-msax 35149* | Define the indexing set for a syntax axiom's representation in a tree. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mSAX = (π‘ β V β¦ (π β (mSAβπ‘) β¦ ((mVHβπ‘) β ((mVarsβπ‘)βπ)))) | ||
Definition | df-mufs 35150 | Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUFS = {π‘ β mGFS β£ Fun (mSTβπ‘)} | ||
Syntax | cmuv 35151 | The universe of a model. |
class mUV | ||
Syntax | cmvl 35152 | The set of valuations. |
class mVL | ||
Syntax | cmvsb 35153 | Substitution for a valuation. |
class mVSubst | ||
Syntax | cmfsh 35154 | The freshness relation of a model. |
class mFresh | ||
Syntax | cmfr 35155 | The set of freshness relations. |
class mFRel | ||
Syntax | cmevl 35156 | The evaluation function of a model. |
class mEval | ||
Syntax | cmdl 35157 | The set of models. |
class mMdl | ||
Syntax | cusyn 35158 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 35159 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 35160 | The interpretation function of the model. |
class mItp | ||
Syntax | cmfitp 35161 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 35162 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUV = Slot 7 | ||
Definition | df-mfsh 35163 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFresh = Slot ;19 | ||
Definition | df-mevl 35164 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mEval = Slot ;20 | ||
Definition | df-mvl 35165* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVL = (π‘ β V β¦ Xπ£ β (mVRβπ‘)((mUVβπ‘) β {((mTypeβπ‘)βπ£)})) | ||
Definition | df-mvsb 35166* | Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVSubst = (π‘ β V β¦ {β¨β¨π , πβ©, π₯β© β£ ((π β ran (mSubstβπ‘) β§ π β (mVLβπ‘)) β§ βπ£ β (mVRβπ‘)πdom (mEvalβπ‘)(π β((mVHβπ‘)βπ£)) β§ π₯ = (π£ β (mVRβπ‘) β¦ (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£)))))}) | ||
Definition | df-mfrel 35167* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFRel = (π‘ β V β¦ {π β π« ((mUVβπ‘) Γ (mUVβπ‘)) β£ (β‘π = π β§ βπ β (mVTβπ‘)βπ€ β (π« (mUVβπ‘) β© Fin)βπ£ β ((mUVβπ‘) β {π})π€ β (π β {π£}))}) | ||
Definition | df-mdl 35168* | Define the set of models of a formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mMdl = {π‘ β mFS β£ [(mUVβπ‘) / π’][(mExβπ‘) / π₯][(mVLβπ‘) / π£][(mEvalβπ‘) / π][(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})))))} | ||
Definition | df-musyn 35169* | Define the syntax typecode function for the model universe. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUSyn = (π‘ β V β¦ (π£ β (mUVβπ‘) β¦ β¨((mSynβπ‘)β(1st βπ£)), (2nd βπ£)β©)) | ||
Definition | df-gmdl 35170* | Define the set of models of a grammatical formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mGMdl = {π‘ β (mGFS β© mMdl) β£ (βπ β (mTCβπ‘)((mUVβπ‘) β {π}) β ((mUVβπ‘) β {((mSynβπ‘)βπ)}) β§ βπ£ β (mUVβπ)βπ€ β (mUVβπ)(π£(mFreshβπ‘)π€ β π£(mFreshβπ‘)((mUSynβπ‘)βπ€)) β§ βπ β (mVLβπ‘)βπ β (mExβπ‘)((mEvalβπ‘) β {β¨π, πβ©}) = (((mEvalβπ‘) β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st βπ)})))} | ||
Definition | df-mitp 35171* | Define the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mItp = (π‘ β V β¦ (π β (mSAβπ‘) β¦ (π β Xπ β ((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)}) β¦ (β©π₯βπ β (mVLβπ‘)(π = (π βΎ ((mVarsβπ‘)βπ)) β§ π₯ = (π(mEvalβπ‘)π)))))) | ||
Definition | df-mfitp 35172* | Define a function that produces the evaluation function, given the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFromItp = (π‘ β V β¦ (π β Xπ β (mSAβπ‘)(((mUVβπ‘) β {((1st βπ‘)βπ)}) βm Xπ β ((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)})) β¦ (β©π β ((mUVβπ‘) βpm ((mVLβπ‘) Γ (mExβπ‘)))βπ β (mVLβπ‘)(βπ£ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) β§ βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) β§ βπ β (mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st βπ)})))))) | ||
Syntax | ccpms 35173 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 35174 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 35175 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 35176 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 35177 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 35178 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 35179 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-cplmet 35180* | A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ cplMetSp = (π€ β V β¦ β¦((π€ βs β) βΎs (Cauβ(distβπ€))) / πβ¦β¦(Baseβπ) / π£β¦β¦{β¨π, πβ© β£ ({π, π} β π£ β§ βπ₯ β β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβ(distβπ€))π₯))} / πβ¦((π /s π) sSet {β¨(distβndx), {β¨β¨π₯, π¦β©, π§β© β£ βπ β π£ βπ β π£ ((π₯ = [π]π β§ π¦ = [π]π) β§ (π βf (distβπ)π) β π§)}β©})) | ||
Definition | df-homlimb 35181* | The input to this function is a sequence (on β) of homomorphisms πΉ(π):π (π)βΆπ (π + 1). The resulting structure is the direct limit of the direct system so defined. This function returns the pair β¨π, πΊβ© where π is the terminal object and πΊ is a sequence of functions such that πΊ(π):π (π)βΆπ and πΊ(π) = πΉ(π) β πΊ(π + 1). (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ HomLimB = (π β V β¦ β¦βͺ π β β ({π} Γ dom (πβπ)) / π£β¦β¦β© {π β£ (π Er π£ β§ (π₯ β π£ β¦ β¨((1st βπ₯) + 1), ((πβ(1st βπ₯))β(2nd βπ₯))β©) β π )} / πβ¦β¨(π£ / π), (π β β β¦ (π₯ β dom (πβπ) β¦ [β¨π, π₯β©]π))β©) | ||
Definition | df-homlim 35182* | The input to this function is a sequence (on β) of structures π (π) and homomorphisms πΉ(π):π (π)βΆπ (π + 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 = (π β V, π β V β¦ β¦( HomLimB βπ) / πβ¦β¦(1st βπ) / π£β¦β¦(2nd βπ) / πβ¦({β¨(Baseβndx), π£β©, β¨(+gβndx), βͺ π β β ran (π₯ β dom (πβπ), π¦ β dom (πβπ) β¦ β¨β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©, ((πβπ)β(π₯(+gβ(πβπ))π¦))β©)β©, β¨(.rβndx), βͺ π β β ran (π₯ β dom (πβπ), π¦ β dom (πβπ) β¦ β¨β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©, ((πβπ)β(π₯(.rβ(πβπ))π¦))β©)β©} βͺ {β¨(TopOpenβndx), {π β π« π£ β£ βπ β β (β‘(πβπ) β π ) β (TopOpenβ(πβπ))}β©, β¨(distβndx), βͺ π β β ran (π₯ β dom ((πβπ)βπ), π¦ β dom ((πβπ)βπ) β¦ β¨β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©, (π₯(distβ(πβπ))π¦)β©)β©, β¨(leβndx), βͺ π β β (β‘(πβπ) β ((leβ(πβπ)) β (πβπ)))β©})) | ||
Definition | df-plfl 35183* | 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 = (π β V, π β V β¦ β¦(Poly1βπ) / π β¦β¦((RSpanβπ )β{π}) / πβ¦β¦(π§ β (Baseβπ) β¦ [(π§( Β·π βπ )(1rβπ ))](π ~QG π)) / πβ¦β¨β¦(π /s (π ~QG π)) / π‘β¦((π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) sSet β¨(leβndx), β¦(π§ β (Baseβπ‘) β¦ (β©π β π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β©), πβ©) | ||
Definition | df-sfl1 35184* |
Temporary construction for the splitting field of a polynomial. The
inputs are a field π and a polynomial π that we
want to split,
along with a tuple π in the same format as the output.
The output
is a tuple β¨π, πΉβ© where π is the splitting field
and πΉ
is an injective homomorphism from the original field π.
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 = (π β V, π β V β¦ (π β (Poly1βπ) β¦ (rec((π β V, π β V β¦ β¦( mPoly βπ ) / πβ¦β¦{π β ((Monic1pβπ ) β© (Irredβπ)) β£ (π(β₯rβπ)(π β π) β§ 1 < (π deg1 π))} / πβ¦if(((π β π) = (0gβπ) β¨ π = β ), β¨π , πβ©, β¦(glbβπ) / ββ¦β¦(π polyFld β) / π‘β¦β¨(1st βπ‘), (π β (2nd βπ‘))β©)), π)β(cardβ(1...(π deg1 π)))))) | ||
Definition | df-sfl 35185* | Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple β¨π, πΉβ© where π is the totally ordered splitting field and πΉ is an injective homomorphism from the original field π. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ splitFld = (π β V, π β V β¦ (β©π₯βπ(π Isom < , (ltβπ)((1...(β―βπ)), π) β§ π₯ = (seq0((π β V, π β V β¦ ((π splitFld1 π)βπ)), (π βͺ {β¨0, β¨π, ( I βΎ (Baseβπ))β©β©}))β(β―βπ))))) | ||
Definition | df-psl 35186* | 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 π, a strict order on π, and a sequence π:ββΆ(π« π β© 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 = (π β V, π β ((π« (Baseβπ) β© Fin) βm β) β¦ β¦(1st β seq0((π β V, π β V β¦ β¦(1st βπ) / πβ¦β¦(1st βπ) / π β¦β¦(π splitFld ran (π₯ β π β¦ (π₯ β (2nd βπ)))) / πβ¦β¨π, ((2nd βπ) β (2nd βπ))β©), (π βͺ {β¨0, β¨β¨π, β β©, ( I βΎ (Baseβπ))β©β©}))) / πβ¦((1st β (π shift 1)) HomLim (2nd β π))) | ||
Syntax | czr 35187 | Integral elements of a ring. |
class ZRing | ||
Syntax | cgf 35188 | Galois finite field. |
class GF | ||
Syntax | cgfo 35189 | Galois limit field. |
class GFβ | ||
Syntax | ceqp 35190 | Equivalence relation for df-qp 35201. |
class ~Qp | ||
Syntax | crqp 35191 | Equivalence relation representatives for df-qp 35201. |
class /Qp | ||
Syntax | cqp 35192 | The set of π-adic rational numbers. |
class Qp | ||
Syntax | czp 35193 | The set of π-adic integers. (Not to be confused with czn 21415.) |
class Zp | ||
Syntax | cqpa 35194 | Algebraic completion of the π-adic rational numbers. |
class _Qp | ||
Syntax | ccp 35195 | Metric completion of _Qp. |
class Cp | ||
Definition | df-zrng 35196 | Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ ZRing = (π β V β¦ (π IntgRing ran (β€RHomβπ))) | ||
Definition | df-gf 35197* | Define the Galois finite field of order πβπ. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ GF = (π β β, π β β β¦ β¦(β€/nβ€βπ) / πβ¦(1st β(π splitFld {β¦(Poly1βπ) / π β¦β¦(var1βπ) / π₯β¦(((πβπ)(.gβ(mulGrpβπ ))π₯)(-gβπ )π₯)}))) | ||
Definition | df-gfoo 35198* | Define the Galois field of order πβ+β, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ GFβ = (π β β β¦ β¦(β€/nβ€βπ) / πβ¦(π polySplitLim (π β β β¦ {β¦(Poly1βπ) / π β¦β¦(var1βπ) / π₯β¦(((πβπ)(.gβ(mulGrpβπ ))π₯)(-gβπ )π₯)}))) | ||
Definition | df-eqp 35199* | Define an equivalence relation on β€-indexed sequences of integers such that two sequences are equivalent iff the difference is equivalent to zero, and a sequence is equivalent to zero iff the sum Ξ£π β€ ππ(π)(πβπ) is a multiple of πβ(π + 1) for every π. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ ~Qp = (π β β β¦ {β¨π, πβ© β£ ({π, π} β (β€ βm β€) β§ βπ β β€ Ξ£π β (β€β₯β-π)(((πβ-π) β (πβ-π)) / (πβ(π + (π + 1)))) β β€)}) | ||
Definition | df-rqp 35200* | There is a unique element of (β€ βm (0...(π β 1))) ~Qp -equivalent to any element of (β€ βm β€), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ /Qp = (π β β β¦ (~Qp β© β¦{π β (β€ βm β€) β£ βπ₯ β ran β€β₯(β‘π β (β€ β {0})) β π₯} / π¦β¦(π¦ Γ (π¦ β© (β€ βm (0...(π β 1))))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |