Home | Metamath
Proof Explorer Theorem List (p. 328 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | msubff1 32701 | 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 32702 | 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 32703 | The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) | ||
Theorem | mvhf1 32704 | 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 32705* | 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 32706 | Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ (𝐴 ∈ (𝐾𝐶𝐵) → (𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸)) | ||
Theorem | mclsssvlem 32707* | Lemma for mclsssv 32709. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) ⇒ ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸) | ||
Theorem | mclsval 32708* | 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 32709 | 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 32710 | Lemma for ssmcls 32712. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐾𝐶𝐵)) | ||
Theorem | vhmcls 32711 | All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻‘𝑋) ∈ (𝐾𝐶𝐵)) | ||
Theorem | ssmcls 32712 | The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) ⇒ ⊢ (𝜑 → 𝐵 ⊆ (𝐾𝐶𝐵)) | ||
Theorem | ss2mcls 32713 | 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 32714* | 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 32715* | 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 32716* | Lemma for mppspst 32719. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃 | ||
Theorem | mppsval 32717* | 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 32718 | 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 32719 | A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑃 | ||
Theorem | mthmval 32720 | 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 32721* | 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 32722 | 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 32723 | A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑈 = (mThm‘𝑇) & ⊢ 𝑆 = (mPreSt‘𝑇) ⇒ ⊢ 𝑈 ⊆ 𝑆 | ||
Theorem | mppsthm 32724 | A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑈 | ||
Theorem | mthmblem 32725 | Lemma for mthmb 32726. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ ((𝑅‘𝑋) = (𝑅‘𝑌) → (𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈)) | ||
Theorem | mthmb 32726 | 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 32727 | 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 32728* | The closure is closed under application of provable pre-statements. (Compare mclsax 32714.) 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 32729* | The closure is closed under application of provable pre-statements. (Compare mclsax 32714.) 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 32730 | Mapping expressions to statements. |
class m0St | ||
Syntax | cmsa 32731 | The set of syntax axioms. |
class mSA | ||
Syntax | cmwgfs 32732 | The set of weakly grammatical formal systems. |
class mWGFS | ||
Syntax | cmsy 32733 | The syntax typecode function. |
class mSyn | ||
Syntax | cmesy 32734 | The syntax typecode function for expressions. |
class mESyn | ||
Syntax | cmgfs 32735 | The set of grammatical formal systems. |
class mGFS | ||
Syntax | cmtree 32736 | The set of proof trees. |
class mTree | ||
Syntax | cmst 32737 | The set of syntax trees. |
class mST | ||
Syntax | cmsax 32738 | The indexing set for a syntax axiom. |
class mSAX | ||
Syntax | cmufs 32739 | The set of unambiguous formal sytems. |
class mUFS | ||
Definition | df-m0s 32740 | Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ m0St = (𝑎 ∈ V ↦ 〈∅, ∅, 𝑎〉) | ||
Definition | df-msa 32741* | 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 32742* | 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 32743 | Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mSyn = Slot 6 | ||
Definition | df-mesyn 32744* | Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023.) |
⊢ mESyn = (𝑡 ∈ V ↦ (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒))) | ||
Definition | df-mgfs 32745* | 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 32746* | 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 32747 | Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mST = (𝑡 ∈ V ↦ ((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡)))) | ||
Definition | df-msax 32748* | 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 32749 | Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)} | ||
Syntax | cmuv 32750 | The universe of a model. |
class mUV | ||
Syntax | cmvl 32751 | The set of valuations. |
class mVL | ||
Syntax | cmvsb 32752 | Substitution for a valuation. |
class mVSubst | ||
Syntax | cmfsh 32753 | The freshness relation of a model. |
class mFresh | ||
Syntax | cmfr 32754 | The set of freshness relations. |
class mFRel | ||
Syntax | cmevl 32755 | The evaluation function of a model. |
class mEval | ||
Syntax | cmdl 32756 | The set of models. |
class mMdl | ||
Syntax | cusyn 32757 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 32758 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 32759 | The interpretation function of the model. |
class mItp | ||
Syntax | cmfitp 32760 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 32761 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUV = Slot 7 | ||
Definition | df-mfsh 32762 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mFresh = Slot 8 | ||
Definition | df-mevl 32763 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mEval = Slot 9 | ||
Definition | df-mvl 32764* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVL = (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)})) | ||
Definition | df-mvsb 32765* | 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 32766* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mFRel = (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))}) | ||
Definition | df-mdl 32767* | 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 32768* | 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 32769* | 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 32770* | 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 32771* | 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 32772 | Integral subring of a ring. |
class IntgRing | ||
Syntax | ccpms 32773 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 32774 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 32775 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 32776 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 32777 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 32778 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 32779 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-irng 32780* | 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 32781* | 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 32782* | 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 32783* | 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 32784* | 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 32785* |
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 32786* | 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 32787* | 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 32788 | Integral elements of a ring. |
class ZRing | ||
Syntax | cgf 32789 | Galois finite field. |
class GF | ||
Syntax | cgfo 32790 | Galois limit field. |
class GF∞ | ||
Syntax | ceqp 32791 | Equivalence relation for df-qp 32802. |
class ~Qp | ||
Syntax | crqp 32792 | Equivalence relation representatives for df-qp 32802. |
class /Qp | ||
Syntax | cqp 32793 | The set of 𝑝-adic rational numbers. |
class Qp | ||
Syntax | czp 32794 | The set of 𝑝-adic integers. (Not to be confused with czn 20580.) |
class Zp | ||
Syntax | cqpa 32795 | Algebraic completion of the 𝑝-adic rational numbers. |
class _Qp | ||
Syntax | ccp 32796 | Metric completion of _Qp. |
class Cp | ||
Definition | df-zrng 32797 | Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ ZRing = (𝑟 ∈ V ↦ (𝑟 IntgRing ran (ℤRHom‘𝑟))) | ||
Definition | df-gf 32798* | 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 32799* | 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 32800* | 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)))) ∈ ℤ)}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |