![]() |
Metamath
Proof Explorer Theorem List (p. 330 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mpstrcl 32901 | The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V)) | ||
Theorem | msrf 32902 | The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑅 = (mStRed‘𝑇) ⇒ ⊢ 𝑅:𝑃⟶𝑃 | ||
Theorem | msrrcl 32903 | If 𝑋 and 𝑌 have the same reduct, then one is a pre-statement iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑅 = (mStRed‘𝑇) ⇒ ⊢ ((𝑅‘𝑋) = (𝑅‘𝑌) → (𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑃)) | ||
Theorem | mstaval 32904 | Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ 𝑆 = ran 𝑅 | ||
Theorem | msrid 32905 | The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝑆 → (𝑅‘𝑋) = 𝑋) | ||
Theorem | msrfo 32906 | The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ 𝑅:𝑃–onto→𝑆 | ||
Theorem | mstapst 32907 | A statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ 𝑆 ⊆ 𝑃 | ||
Theorem | elmsta 32908 | Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) & ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴})) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 ↔ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍))) | ||
Theorem | ismfs 32909* | A formal system is a tuple 〈mCN, mVR, mType, mVT, mTC, mAx〉 such that: mCN and mVR are disjoint; mType is a function from mVR to mVT; mVT is a subset of mTC; mAx is a set of statements; and for each variable typecode, there are infinitely many variables of that type. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) & ⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) & ⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → (𝑇 ∈ mFS ↔ (((𝐶 ∩ 𝑉) = ∅ ∧ 𝑌:𝑉⟶𝐾) ∧ (𝐴 ⊆ 𝑆 ∧ ∀𝑣 ∈ 𝐹 ¬ (◡𝑌 “ {𝑣}) ∈ Fin)))) | ||
Theorem | mfsdisj 32910 | The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → (𝐶 ∩ 𝑉) = ∅) | ||
Theorem | mtyf2 32911 | The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐾) | ||
Theorem | mtyf 32912 | The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐹) | ||
Theorem | mvtss 32913 | The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐹 ⊆ 𝐾) | ||
Theorem | maxsta 32914 | An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐴 ⊆ 𝑆) | ||
Theorem | mvtinf 32915 | Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ ((𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹) → ¬ (◡𝑌 “ {𝑋}) ∈ Fin) | ||
Theorem | msubff1 32916 | 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 32917 | 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 32918 | The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) | ||
Theorem | mvhf1 32919 | 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 32920* | 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 32921 | Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ (𝐴 ∈ (𝐾𝐶𝐵) → (𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸)) | ||
Theorem | mclsssvlem 32922* | Lemma for mclsssv 32924. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) ⇒ ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸) | ||
Theorem | mclsval 32923* | 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 32924 | 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 32925 | Lemma for ssmcls 32927. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐾𝐶𝐵)) | ||
Theorem | vhmcls 32926 | All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻‘𝑋) ∈ (𝐾𝐶𝐵)) | ||
Theorem | ssmcls 32927 | The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) ⇒ ⊢ (𝜑 → 𝐵 ⊆ (𝐾𝐶𝐵)) | ||
Theorem | ss2mcls 32928 | 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 32929* | 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 32930* | 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 32931* | Lemma for mppspst 32934. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃 | ||
Theorem | mppsval 32932* | 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 32933 | 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 32934 | A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑃 | ||
Theorem | mthmval 32935 | 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 32936* | 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 32937 | 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 32938 | A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑈 = (mThm‘𝑇) & ⊢ 𝑆 = (mPreSt‘𝑇) ⇒ ⊢ 𝑈 ⊆ 𝑆 | ||
Theorem | mppsthm 32939 | A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑈 | ||
Theorem | mthmblem 32940 | Lemma for mthmb 32941. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ ((𝑅‘𝑋) = (𝑅‘𝑌) → (𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈)) | ||
Theorem | mthmb 32941 | 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 32942 | 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 32943* | The closure is closed under application of provable pre-statements. (Compare mclsax 32929.) 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 32944* | The closure is closed under application of provable pre-statements. (Compare mclsax 32929.) 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 32945 | Mapping expressions to statements. |
class m0St | ||
Syntax | cmsa 32946 | The set of syntax axioms. |
class mSA | ||
Syntax | cmwgfs 32947 | The set of weakly grammatical formal systems. |
class mWGFS | ||
Syntax | cmsy 32948 | The syntax typecode function. |
class mSyn | ||
Syntax | cmesy 32949 | The syntax typecode function for expressions. |
class mESyn | ||
Syntax | cmgfs 32950 | The set of grammatical formal systems. |
class mGFS | ||
Syntax | cmtree 32951 | The set of proof trees. |
class mTree | ||
Syntax | cmst 32952 | The set of syntax trees. |
class mST | ||
Syntax | cmsax 32953 | The indexing set for a syntax axiom. |
class mSAX | ||
Syntax | cmufs 32954 | The set of unambiguous formal sytems. |
class mUFS | ||
Definition | df-m0s 32955 | Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ m0St = (𝑎 ∈ V ↦ 〈∅, ∅, 𝑎〉) | ||
Definition | df-msa 32956* | 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 32957* | 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 32958 | Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mSyn = Slot 6 | ||
Definition | df-mesyn 32959* | Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023.) |
⊢ mESyn = (𝑡 ∈ V ↦ (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒))) | ||
Definition | df-mgfs 32960* | 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 32961* | 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 32962 | Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mST = (𝑡 ∈ V ↦ ((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡)))) | ||
Definition | df-msax 32963* | 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 32964 | Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)} | ||
Syntax | cmuv 32965 | The universe of a model. |
class mUV | ||
Syntax | cmvl 32966 | The set of valuations. |
class mVL | ||
Syntax | cmvsb 32967 | Substitution for a valuation. |
class mVSubst | ||
Syntax | cmfsh 32968 | The freshness relation of a model. |
class mFresh | ||
Syntax | cmfr 32969 | The set of freshness relations. |
class mFRel | ||
Syntax | cmevl 32970 | The evaluation function of a model. |
class mEval | ||
Syntax | cmdl 32971 | The set of models. |
class mMdl | ||
Syntax | cusyn 32972 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 32973 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 32974 | The interpretation function of the model. |
class mItp | ||
Syntax | cmfitp 32975 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 32976 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUV = Slot 7 | ||
Definition | df-mfsh 32977 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mFresh = Slot 8 | ||
Definition | df-mevl 32978 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mEval = Slot 9 | ||
Definition | df-mvl 32979* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVL = (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)})) | ||
Definition | df-mvsb 32980* | 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 32981* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mFRel = (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))}) | ||
Definition | df-mdl 32982* | 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 32983* | 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 32984* | 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 32985* | 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 32986* | 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 32987 | Integral subring of a ring. |
class IntgRing | ||
Syntax | ccpms 32988 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 32989 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 32990 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 32991 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 32992 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 32993 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 32994 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-irng 32995* | 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 32996* | 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 32997* | 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 32998* | 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 32999* | 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 33000* |
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 𝑝)))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |