Home | Metamath
Proof Explorer Theorem List (p. 329 of 449) | < 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: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mvhf1 32801 | 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 32802* | 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 32803 | Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ (𝐴 ∈ (𝐾𝐶𝐵) → (𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸)) | ||
Theorem | mclsssvlem 32804* | Lemma for mclsssv 32806. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) ⇒ ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸) | ||
Theorem | mclsval 32805* | 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 32806 | 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 32807 | Lemma for ssmcls 32809. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐾𝐶𝐵)) | ||
Theorem | vhmcls 32808 | All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻‘𝑋) ∈ (𝐾𝐶𝐵)) | ||
Theorem | ssmcls 32809 | The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) ⇒ ⊢ (𝜑 → 𝐵 ⊆ (𝐾𝐶𝐵)) | ||
Theorem | ss2mcls 32810 | 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 32811* | 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 32812* | 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 32813* | Lemma for mppspst 32816. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃 | ||
Theorem | mppsval 32814* | 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 32815 | 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 32816 | A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑃 | ||
Theorem | mthmval 32817 | 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 32818* | 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 32819 | 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 32820 | A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑈 = (mThm‘𝑇) & ⊢ 𝑆 = (mPreSt‘𝑇) ⇒ ⊢ 𝑈 ⊆ 𝑆 | ||
Theorem | mppsthm 32821 | A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑈 | ||
Theorem | mthmblem 32822 | Lemma for mthmb 32823. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ ((𝑅‘𝑋) = (𝑅‘𝑌) → (𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈)) | ||
Theorem | mthmb 32823 | 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 32824 | 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 32825* | The closure is closed under application of provable pre-statements. (Compare mclsax 32811.) 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 32826* | The closure is closed under application of provable pre-statements. (Compare mclsax 32811.) 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 32827 | Mapping expressions to statements. |
class m0St | ||
Syntax | cmsa 32828 | The set of syntax axioms. |
class mSA | ||
Syntax | cmwgfs 32829 | The set of weakly grammatical formal systems. |
class mWGFS | ||
Syntax | cmsy 32830 | The syntax typecode function. |
class mSyn | ||
Syntax | cmesy 32831 | The syntax typecode function for expressions. |
class mESyn | ||
Syntax | cmgfs 32832 | The set of grammatical formal systems. |
class mGFS | ||
Syntax | cmtree 32833 | The set of proof trees. |
class mTree | ||
Syntax | cmst 32834 | The set of syntax trees. |
class mST | ||
Syntax | cmsax 32835 | The indexing set for a syntax axiom. |
class mSAX | ||
Syntax | cmufs 32836 | The set of unambiguous formal sytems. |
class mUFS | ||
Definition | df-m0s 32837 | Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ m0St = (𝑎 ∈ V ↦ 〈∅, ∅, 𝑎〉) | ||
Definition | df-msa 32838* | 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 32839* | 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 32840 | Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mSyn = Slot 6 | ||
Definition | df-mesyn 32841* | Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023.) |
⊢ mESyn = (𝑡 ∈ V ↦ (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒))) | ||
Definition | df-mgfs 32842* | 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 32843* | 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 32844 | Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mST = (𝑡 ∈ V ↦ ((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡)))) | ||
Definition | df-msax 32845* | 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 32846 | Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)} | ||
Syntax | cmuv 32847 | The universe of a model. |
class mUV | ||
Syntax | cmvl 32848 | The set of valuations. |
class mVL | ||
Syntax | cmvsb 32849 | Substitution for a valuation. |
class mVSubst | ||
Syntax | cmfsh 32850 | The freshness relation of a model. |
class mFresh | ||
Syntax | cmfr 32851 | The set of freshness relations. |
class mFRel | ||
Syntax | cmevl 32852 | The evaluation function of a model. |
class mEval | ||
Syntax | cmdl 32853 | The set of models. |
class mMdl | ||
Syntax | cusyn 32854 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 32855 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 32856 | The interpretation function of the model. |
class mItp | ||
Syntax | cmfitp 32857 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 32858 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUV = Slot 7 | ||
Definition | df-mfsh 32859 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mFresh = Slot 8 | ||
Definition | df-mevl 32860 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mEval = Slot 9 | ||
Definition | df-mvl 32861* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVL = (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)})) | ||
Definition | df-mvsb 32862* | 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 32863* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mFRel = (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))}) | ||
Definition | df-mdl 32864* | 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 32865* | 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 32866* | 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 32867* | 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 32868* | 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 | citr 32869 | Integral subring of a ring. |
class IntgRing | ||
Syntax | ccpms 32870 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 32871 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 32872 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 32873 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 32874 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 32875 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 32876 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-irng 32877* | Define the subring of elements of 𝑟 integral over 𝑠 in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)})) | ||
Definition | df-cplmet 32878* | 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 32879* | 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 32880* | 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 32881* | 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 32882* |
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 32883* | 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 32884* | 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 32885 | Integral elements of a ring. |
class ZRing | ||
Syntax | cgf 32886 | Galois finite field. |
class GF | ||
Syntax | cgfo 32887 | Galois limit field. |
class GF∞ | ||
Syntax | ceqp 32888 | Equivalence relation for df-qp 32899. |
class ~Qp | ||
Syntax | crqp 32889 | Equivalence relation representatives for df-qp 32899. |
class /Qp | ||
Syntax | cqp 32890 | The set of 𝑝-adic rational numbers. |
class Qp | ||
Syntax | czp 32891 | The set of 𝑝-adic integers. (Not to be confused with czn 20644.) |
class Zp | ||
Syntax | cqpa 32892 | Algebraic completion of the 𝑝-adic rational numbers. |
class _Qp | ||
Syntax | ccp 32893 | Metric completion of _Qp. |
class Cp | ||
Definition | df-zrng 32894 | Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ ZRing = (𝑟 ∈ V ↦ (𝑟 IntgRing ran (ℤRHom‘𝑟))) | ||
Definition | df-gf 32895* | 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 32896* | 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 32897* | 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 32898* | 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 32899* | 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 32900 | Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ Zp = (ZRing ∘ Qp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |