| Metamath
Proof Explorer Theorem List (p. 357 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-msa 35601* | 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 35602* | 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 35603 | Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mSyn = Slot 6 | ||
| Definition | df-mesyn 35604* | Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023.) |
| ⊢ mESyn = (𝑡 ∈ V ↦ (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒))) | ||
| Definition | df-mgfs 35605* | 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 35606* | 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 35607 | Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mST = (𝑡 ∈ V ↦ ((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡)))) | ||
| Definition | df-msax 35608* | 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 35609 | Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)} | ||
| Syntax | cmuv 35610 | The universe of a model. |
| class mUV | ||
| Syntax | cmvl 35611 | The set of valuations. |
| class mVL | ||
| Syntax | cmvsb 35612 | Substitution for a valuation. |
| class mVSubst | ||
| Syntax | cmfsh 35613 | The freshness relation of a model. |
| class mFresh | ||
| Syntax | cmfr 35614 | The set of freshness relations. |
| class mFRel | ||
| Syntax | cmevl 35615 | The evaluation function of a model. |
| class mEval | ||
| Syntax | cmdl 35616 | The set of models. |
| class mMdl | ||
| Syntax | cusyn 35617 | The syntax function applied to elements of the model. |
| class mUSyn | ||
| Syntax | cgmdl 35618 | The set of models in a grammatical formal system. |
| class mGMdl | ||
| Syntax | cmitp 35619 | The interpretation function of the model. |
| class mItp | ||
| Syntax | cmfitp 35620 | The evaluation function derived from the interpretation. |
| class mFromItp | ||
| Definition | df-muv 35621 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mUV = Slot 7 | ||
| Definition | df-mfsh 35622 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mFresh = Slot ;19 | ||
| Definition | df-mevl 35623 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mEval = Slot ;20 | ||
| Definition | df-mvl 35624* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mVL = (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)})) | ||
| Definition | df-mvsb 35625* | 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 35626* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mFRel = (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))}) | ||
| Definition | df-mdl 35627* | 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 35628* | 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 35629* | 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 35630* | 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 35631* | 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 35632 | Completion of a metric space. |
| class cplMetSp | ||
| Syntax | chlb 35633 | Embeddings for a direct limit. |
| class HomLimB | ||
| Syntax | chlim 35634 | Direct limit structure. |
| class HomLim | ||
| Syntax | cpfl 35635 | Polynomial extension field. |
| class polyFld | ||
| Syntax | csf1 35636 | Splitting field for a single polynomial (auxiliary). |
| class splitFld1 | ||
| Syntax | csf 35637 | Splitting field for a finite set of polynomials. |
| class splitFld | ||
| Syntax | cpsl 35638 | Splitting field for a sequence of polynomials. |
| class polySplitLim | ||
| Definition | df-cplmet 35639* | 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 35640* | 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 35641* | 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 35642* | 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.) (Revised by Thierry Arnoux and Steven Nguyen, 21-Jun-2025.) |
| ⊢ polyFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌〈⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉), 𝑓〉) | ||
| Theorem | rexxfr3d 35643* | Transfer existential quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by SN, 20-Jun-2025.) |
| ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ∃𝑦 ∈ 𝐵 𝑥 = 𝑋)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | ||
| Theorem | rexxfr3dALT 35644* | Longer proof of rexxfr3d 35643 using ax-11 2157 instead of ax-12 2177, without the disjoint variable condition 𝐴𝑥𝑦. (Contributed by SN, 19-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ∃𝑦 ∈ 𝐵 𝑥 = 𝑋)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | ||
| Theorem | rspssbasd 35645 | The span of a set of ring elements is a set of ring elements. (Contributed by SN, 19-Jun-2025.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐺 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝐵) | ||
| Theorem | ellcsrspsn 35646* | Membership in a left coset in a quotient of a ring by the span of a singleton (that is, by the ideal generated by an element). This characterization comes from eqglact 19197 and elrspsn 21250. (Contributed by SN, 19-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑈 = (𝑅 /s ∼ ) & ⊢ 𝐼 = ((RSpan‘𝑅)‘{𝑀}) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑈)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (𝑋 = [𝑥] ∼ ∧ 𝑋 = {𝑧 ∣ ∃𝑦 ∈ 𝐵 𝑧 = (𝑥 + (𝑦 · 𝑀))})) | ||
| Theorem | ply1divalg3 35647* | Uniqueness of polynomial remainder: convert the subtraction in ply1divalg2 26178 to addition. (Contributed by SN, 20-Jun-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ + = (+g‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐶) ⇒ ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 + (𝑞 ∙ 𝐺))) < (𝐷‘𝐺)) | ||
| Theorem | r1peuqusdeg1 35648* | Uniqueness of polynomial remainder in terms of a quotient structure in the sense of the right hand side of r1pid2 26201. (Contributed by SN, 21-Jun-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐼 = ((RSpan‘𝑃)‘{𝐹}) & ⊢ 𝑇 = (𝑃 /s (𝑃 ~QG 𝐼)) & ⊢ 𝑄 = (Base‘𝑇) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐹 ∈ 𝑁) & ⊢ (𝜑 → 𝑍 ∈ 𝑄) ⇒ ⊢ (𝜑 → ∃!𝑞 ∈ 𝑍 (𝐷‘𝑞) < (𝐷‘𝐹)) | ||
| Definition | df-sfl1 35649* |
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 ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟deg1𝑝)))))) | ||
| Definition | df-sfl 35650* | 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 35651* | 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 35652 | Integral elements of a ring. |
| class ZRing | ||
| Syntax | cgf 35653 | Galois finite field. |
| class GF | ||
| Syntax | cgfo 35654 | Galois limit field. |
| class GF∞ | ||
| Syntax | ceqp 35655 | Equivalence relation for df-qp 35666. |
| class ~Qp | ||
| Syntax | crqp 35656 | Equivalence relation representatives for df-qp 35666. |
| class /Qp | ||
| Syntax | cqp 35657 | The set of 𝑝-adic rational numbers. |
| class Qp | ||
| Syntax | czp 35658 | The set of 𝑝-adic integers. (Not to be confused with czn 21513.) |
| class Zp | ||
| Syntax | cqpa 35659 | Algebraic completion of the 𝑝-adic rational numbers. |
| class _Qp | ||
| Syntax | ccp 35660 | Metric completion of _Qp. |
| class Cp | ||
| Definition | df-zrng 35661 | Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ ZRing = (𝑟 ∈ V ↦ (𝑟 IntgRing ran (ℤRHom‘𝑟))) | ||
| Definition | df-gf 35662* | 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 35663* | 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 35664* | 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 35665* | 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))))))) | ||
| Definition | df-qp 35666* | Define the 𝑝-adic completion of the rational numbers, as a normed field structure with a total order (that is not compatible with the operations). (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 10-Oct-2021.) |
| ⊢ Qp = (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉} ∪ {〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )))))) | ||
| Definition | df-zp 35667 | Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ Zp = (ZRing ∘ Qp) | ||
| Definition | df-qpa 35668* | Define the completion of the 𝑝-adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the 𝑛-th set the collection of polynomials with degree less than 𝑛 and with coefficients < (𝑝↑𝑛)). Krasner's lemma will then show that all monic polynomials have splitting fields isomorphic to a sufficiently close Eisenstein polynomial from the list, and unramified extensions are generated by the polynomial 𝑥↑(𝑝↑𝑛) − 𝑥, which is in the list. Thus, every finite extension of Qp is a subfield of this field extension, so it is algebraically closed. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ _Qp = (𝑝 ∈ ℙ ↦ ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}))) | ||
| Definition | df-cp 35669 | Define the metric completion of the algebraic completion of the 𝑝 -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ Cp = ( cplMetSp ∘ _Qp) | ||
I hope someone will enjoy solving (proving) the simple equations, inequalities, and calculations from this mathbox. I have proved these problems (theorems) using the Milpgame proof assistant. (It can be downloaded from https://us.metamath.org/other/milpgame/milpgame.html.) | ||
| Theorem | problem1 35670 | Practice problem 1. Clues: 5p4e9 12424 3p2e5 12417 eqtri 2765 oveq1i 7441. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ ((3 + 2) + 4) = 9 | ||
| Theorem | problem2 35671 | Practice problem 2. Clues: oveq12i 7443 adddiri 11274 add4i 11486 mulcli 11268 recni 11275 2re 12340 3eqtri 2769 10re 12752 5re 12353 1re 11261 4re 12350 eqcomi 2746 5p4e9 12424 oveq1i 7441 df-3 12330. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Revised by AV, 9-Sep-2021.) (Proof modification is discouraged.) |
| ⊢ (((2 · ;10) + 5) + ((1 · ;10) + 4)) = ((3 · ;10) + 9) | ||
| Theorem | problem3 35672 | Practice problem 3. Clues: eqcomi 2746 eqtri 2765 subaddrii 11598 recni 11275 4re 12350 3re 12346 1re 11261 df-4 12331 addcomi 11452. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ (𝐴 + 3) = 4 ⇒ ⊢ 𝐴 = 1 | ||
| Theorem | problem4 35673 | Practice problem 4. Clues: pm3.2i 470 eqcomi 2746 eqtri 2765 subaddrii 11598 recni 11275 7re 12359 6re 12356 ax-1cn 11213 df-7 12334 ax-mp 5 oveq1i 7441 3cn 12347 2cn 12341 df-3 12330 mullidi 11266 subdiri 11713 mp3an 1463 mulcli 11268 subadd23 11520 oveq2i 7442 oveq12i 7443 3t2e6 12432 mulcomi 11269 subcli 11585 biimpri 228 subadd2i 11597. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 3 & ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7 ⇒ ⊢ (𝐴 = 1 ∧ 𝐵 = 2) | ||
| Theorem | problem5 35674 | Practice problem 5. Clues: 3brtr3i 5172 mpbi 230 breqtri 5168 ltaddsubi 11824 remulcli 11277 2re 12340 3re 12346 9re 12365 eqcomi 2746 mvlladdi 11527 3cn 6cn 12357 eqtr3i 2767 6p3e9 12426 addcomi 11452 ltdiv1ii 12197 6re 12356 nngt0i 12305 2nn 12339 divcan3i 12013 recni 11275 2cn 12341 2ne0 12370 mpbir 231 eqtri 2765 mulcomi 11269 3t2e6 12432 divmuli 12021. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ ((2 · 𝐴) + 3) < 9 ⇒ ⊢ 𝐴 < 3 | ||
| Theorem | quad3 35675 | Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.) |
| ⊢ 𝑋 ∈ ℂ & ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ⇒ ⊢ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))) | ||
| Theorem | climuzcnv 35676* | Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.) |
| ⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑)))) | ||
| Theorem | sinccvglem 35677* | ((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ∖ {0})) & ⊢ (𝜑 → 𝐹 ⇝ 0) & ⊢ 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) & ⊢ 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) < 1) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) ⇝ 1) | ||
| Theorem | sinccvg 35678* | ((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.) |
| ⊢ ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝐹 ⇝ 0) → ((𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) ∘ 𝐹) ⇝ 1) | ||
| Theorem | circum 35679* | The circumference of a circle of radius 𝑅, defined as the limit as 𝑛 ⇝ +∞ of the perimeter of an inscribed n-sided isogons, is ((2 · π) · 𝑅). (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.) |
| ⊢ 𝐴 = ((2 · π) / 𝑛) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ ((2 · 𝑛) · (𝑅 · (sin‘(𝐴 / 2))))) & ⊢ 𝑅 ∈ ℝ ⇒ ⊢ 𝑃 ⇝ ((2 · π) · 𝑅) | ||
| Theorem | elfzm12 35680 | Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.) |
| ⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁))) | ||
| Theorem | nn0seqcvg 35681* | A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011.) |
| ⊢ 𝐹:ℕ0⟶ℕ0 & ⊢ 𝑁 = (𝐹‘0) & ⊢ (𝑘 ∈ ℕ0 → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘))) ⇒ ⊢ (𝐹‘𝑁) = 0 | ||
| Theorem | lediv2aALT 35682 | Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))) | ||
| Theorem | abs2sqlei 35683 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2)) | ||
| Theorem | abs2sqlti 35684 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2)) | ||
| Theorem | abs2sqle 35685 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2))) | ||
| Theorem | abs2sqlt 35686 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2))) | ||
| Theorem | abs2difi 35687 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)) | ||
| Theorem | abs2difabsi 35688 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)) | ||
| Theorem | 2thALT 35689 | Alternate proof of 2th 264. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
| Theorem | orbi2iALT 35690 | Alternate proof of orbi2i 913. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) | ||
| Theorem | pm3.48ALT 35691 | Alternate proof of pm3.48 966. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))) | ||
| Theorem | 3jcadALT 35692 | Alternate proof of 3jcad 1130. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) Use 3jcad instead. (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) | ||
| Theorem | currybi 35693 | Biconditional version of Curry's paradox. If some proposition 𝜑 amounts to the self-referential statement "This very statement is equivalent to 𝜓", then 𝜓 is true. See bj-currypara 36561 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.) |
| ⊢ ((𝜑 ↔ (𝜑 ↔ 𝜓)) → 𝜓) | ||
| Theorem | antnest 35694 | Suppose 𝜑, 𝜓 are distinct atomic propositional formulas, and let Γ be the smallest class of formulas for which ⊤ ∈ Γ and (𝜒 → 𝜑), (𝜒 → 𝜓) ∈ Γ for 𝜒 ∈ Γ. The present theorem is then an element of Γ, and the implications occurring in the theorem are in one-to-one correspondence with the formulas in Γ up to logical equivalence. In particular, the theorem itself is equivalent to ⊤ ∈ Γ. (Contributed by Adrian Ducourtial, 2-Oct-2025.) |
| ⊢ ((((((⊤ → 𝜑) → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓) | ||
| Syntax | ccloneop 35695 | Syntax for the function of the class of operations on a set. |
| class CloneOp | ||
| Definition | df-cloneop 35696* | Define the function that sends a set to the class of clone-theoretic operations on the set. For convenience, we take an operation on 𝑎 to be a function on finite sequences of elements of 𝑎 (rather than tuples) with values in 𝑎. Following line 6 of [Szendrei] p. 11, the arity 𝑛 of an operation (here, the length of the sequences at which the operation is defined) is always finite and non-zero, whence 𝑛 is taken to be a non-zero finite ordinal. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
| ⊢ CloneOp = (𝑎 ∈ V ↦ {𝑥 ∣ ∃𝑛 ∈ (ω ∖ 1o)𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))}) | ||
| Syntax | cprj 35697 | Syntax for the function of projections on sets. |
| class prj | ||
| Definition | df-prj 35698* | Define the function that, for a set 𝑎, arity 𝑛, and index 𝑖, returns the 𝑖-th 𝑛-ary projection on 𝑎. This is the 𝑛-ary operation on 𝑎 that, for any sequence of 𝑛 elements of 𝑎, returns the element having index 𝑖. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
| ⊢ prj = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑖 ∈ 𝑛 ↦ (𝑥 ∈ (𝑎 ↑m 𝑛) ↦ (𝑥‘𝑖)))) | ||
| Syntax | csuppos 35699 | Syntax for the function of superpositions. |
| class suppos | ||
| Definition | df-suppos 35700* | Define the function that, when given an 𝑛-ary operation 𝑓 and 𝑛 many 𝑚-ary operations (𝑔‘∅), ..., (𝑔‘∪ 𝑛), returns the superposition of 𝑓 with the (𝑔‘𝑖), itself another 𝑚-ary operation on 𝑎. Given 𝑥 (a sequence of 𝑚 arguments in 𝑎), the superposition effectively applies each of the (𝑔‘𝑖) to 𝑥, then applies 𝑓 to the resulting sequence of 𝑛 function values. This can be seen as a generalized version of function composition; see paragraph 3 of [Szendrei] p. 11. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
| ⊢ suppos = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑚 ∈ (ω ∖ 1o) ↦ (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥))))))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |