Home | Metamath
Proof Explorer Theorem List (p. 308 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mfsdisj 30701 | The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → (𝐶 ∩ 𝑉) = ∅) | ||
Theorem | mtyf2 30702 | The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐾) | ||
Theorem | mtyf 30703 | The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐹) | ||
Theorem | mvtss 30704 | The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐹 ⊆ 𝐾) | ||
Theorem | maxsta 30705 | An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐴 ⊆ 𝑆) | ||
Theorem | mvtinf 30706 | Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ ((𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹) → ¬ (◡𝑌 “ {𝑋}) ∈ Fin) | ||
Theorem | msubff1 30707 | 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 → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝐸 ↑𝑚 𝐸)) | ||
Theorem | msubff1o 30708 | 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 → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1-onto→ran 𝑆) | ||
Theorem | mvhf 30709 | The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) | ||
Theorem | mvhf1 30710 | 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 30711* | 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 30712 | Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ (𝐴 ∈ (𝐾𝐶𝐵) → (𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸)) | ||
Theorem | mclsssvlem 30713* | Lemma for mclsssv 30715. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) ⇒ ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸) | ||
Theorem | mclsval 30714* | 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 30715 | 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 30716 | Lemma for ssmcls 30718. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐾𝐶𝐵)) | ||
Theorem | vhmcls 30717 | All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻‘𝑋) ∈ (𝐾𝐶𝐵)) | ||
Theorem | ssmcls 30718 | The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) ⇒ ⊢ (𝜑 → 𝐵 ⊆ (𝐾𝐶𝐵)) | ||
Theorem | ss2mcls 30719 | 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 30720* | 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 30721* | 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 30722* | Lemma for mppspst 30725. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃 | ||
Theorem | mppsval 30723* | 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 30724 | 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 30725 | A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑃 | ||
Theorem | mthmval 30726 | 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 30727* | 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 30728 | 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 30729 | A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑈 = (mThm‘𝑇) & ⊢ 𝑆 = (mPreSt‘𝑇) ⇒ ⊢ 𝑈 ⊆ 𝑆 | ||
Theorem | mppsthm 30730 | A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑈 | ||
Theorem | mthmblem 30731 | Lemma for mthmb 30732. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ ((𝑅‘𝑋) = (𝑅‘𝑌) → (𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈)) | ||
Theorem | mthmb 30732 | 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 30733 | Given a theorem, there is an explicitly definable witnessing provable pre-statement for the provability of the theorem. (However, this pre-statement requires infinitely many dv conditions, which is sometimes inconvenient.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) & ⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) & ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴})) & ⊢ 𝑀 = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ⇒ ⊢ (𝑇 ∈ mFS → (〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈 ↔ (〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)))) | ||
Theorem | mclsppslem 30734* | The closure is closed under application of provable pre-statements. (Compare mclsax 30720.) 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 30735* | The closure is closed under application of provable pre-statements. (Compare mclsax 30720.) 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 30736 | Mapping expressions to statements. |
class m0St | ||
Syntax | cmsa 30737 | The set of syntax axioms. |
class mSA | ||
Syntax | cmwgfs 30738 | The set of weakly grammatical formal systems. |
class mWGFS | ||
Syntax | cmsy 30739 | The syntax typecode function. |
class mSyn | ||
Syntax | cmesy 30740 | The syntax typecode function for expressions. |
class mESyn | ||
Syntax | cmgfs 30741 | The set of grammatical formal systems. |
class mGFS | ||
Syntax | cmtree 30742 | The set of proof trees. |
class mTree | ||
Syntax | cmst 30743 | The set of syntax trees. |
class mST | ||
Syntax | cmsax 30744 | The indexing set for a syntax axiom. |
class mSAX | ||
Syntax | cmufs 30745 | The set of unambiguous formal sytems. |
class mUFS | ||
Definition | df-m0s 30746 | Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ m0St = (𝑎 ∈ V ↦ 〈∅, ∅, 𝑎〉) | ||
Definition | df-msa 30747* | 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 30748* | 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 30749 | Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mSyn = Slot 6 | ||
Definition | df-mtree 30750* | 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 30751 | Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mST = (𝑡 ∈ V ↦ ((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡)))) | ||
Definition | df-msax 30752* | 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 30753 | Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)} | ||
Syntax | cmuv 30754 | The universe of a model. |
class mUV | ||
Syntax | cmvl 30755 | The set of valuations. |
class mVL | ||
Syntax | cmvsb 30756 | Substitution for a valuation. |
class mVSubst | ||
Syntax | cmfsh 30757 | The freshness relation of a model. |
class mFresh | ||
Syntax | cmfr 30758 | The set of freshness relations. |
class mFRel | ||
Syntax | cmevl 30759 | The evaluation function of a model. |
class mEval | ||
Syntax | cmdl 30760 | The set of models. |
class mMdl | ||
Syntax | cusyn 30761 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 30762 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 30763 | The interpretation function of the model. |
class mItp | ||
Syntax | cmfitp 30764 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 30765 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUV = Slot 7 | ||
Definition | df-mfsh 30766 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mFresh = Slot 8 | ||
Definition | df-mevl 30767 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mEval = Slot 9 | ||
Definition | df-mvl 30768* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVL = (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)})) | ||
Definition | df-mvsb 30769* | 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 30770* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mFRel = (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))}) | ||
Definition | df-mdl 30771* | 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 30772* | 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 30773* | 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 30774* | 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 30775* | 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 ‘𝑡)‘𝑎)}) ↑𝑚 X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})) ↦ (℩𝑛 ∈ ((mUV‘𝑡) ↑pm ((mVL‘𝑡) × (mEx‘𝑡)))∀𝑚 ∈ (mVL‘𝑡)(∀𝑣 ∈ (mVR‘𝑡)〈𝑚, ((mVH‘𝑡)‘𝑣)〉𝑛(𝑚‘𝑣) ∧ ∀𝑒∀𝑎∀𝑔(𝑒(mST‘𝑡)〈𝑎, 𝑔〉 → 〈𝑚, 𝑒〉𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))) ∧ ∀𝑒 ∈ (mEx‘𝑡)(𝑛 “ {〈𝑚, 𝑒〉}) = ((𝑛 “ {〈𝑚, ((mESyn‘𝑡)‘𝑒)〉}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)})))))) | ||
Syntax | citr 30776 | Integral subring of a ring. |
class IntgRing | ||
Syntax | ccpms 30777 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 30778 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 30779 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 30780 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 30781 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 30782 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 30783 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-irng 30784* | 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 30785* | 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), {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}〉})) | ||
Definition | df-homlimb 30786* | 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 30787* | 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 30788* | 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 30789* |
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 30790* | 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 30791* | 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) ↑𝑚 ℕ) ↦ ⦋(1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌〈𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))〉), (𝑝 ∪ {〈0, 〈〈𝑟, ∅〉, ( I ↾ (Base‘𝑟))〉〉}))) / 𝑓⦌((1st ∘ (𝑓 shift 1)) HomLim (2nd ∘ 𝑓))) | ||
Syntax | czr 30792 | Integral elements of a ring. |
class ZRing | ||
Syntax | cgf 30793 | Galois finite field. |
class GF | ||
Syntax | cgfo 30794 | Galois limit field. |
class GF∞ | ||
Syntax | ceqp 30795 | Equivalence relation for df-qp 30807. |
class ~Qp | ||
Syntax | crqp 30796 | Equivalence relation representatives for df-qp 30807. |
class /Qp | ||
Syntax | cqp 30797 | The set of 𝑝-adic rational numbers. |
class Qp | ||
Syntax | cqpOLD 30798 | The set of 𝑝-adic rational numbers. (New usage is discouraged.) |
class QpOLD | ||
Syntax | czp 30799 | The set of 𝑝-adic integers. (Not to be confused with czn 19670.) |
class Zp | ||
Syntax | cqpa 30800 | Algebraic completion of the 𝑝-adic rational numbers. |
class _Qp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |