HomeTheorem List (p. 323 of 473)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 323 of 473) | < 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-29860) |
Hilbert Space Explorer
(29861-31383) |
Users' Mathboxes
(31384-47242) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | kerlidl 32201 | The kernel of a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (◡𝐹 “ { 0 }) ∈ 𝐼) | ||
| Theorem | 0ringidl 32202 | The zero ideal is the only ideal of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (LIdeal‘𝑅) = {{ 0 }}) | ||
| Theorem | elrspunidl 32203* | Elementhood to the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 𝑁 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑆 ⊆ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘∪ 𝑆) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))) | ||
| Theorem | lidlincl 32204 | Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.) |
| ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈) → (𝐼 ∩ 𝐽) ∈ 𝑈) | ||
| Theorem | idlinsubrg 32205 | The intersection between an ideal and a subring is an ideal of the subring. (Contributed by Thierry Arnoux, 6-Jul-2024.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝑉 = (LIdeal‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (𝐼 ∩ 𝐴) ∈ 𝑉) | ||
| Theorem | rhmimaidl 32206 | The image of an ideal 𝐼 by a surjective ring homomorphism 𝐹 is an ideal. (Contributed by Thierry Arnoux, 6-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑇 = (LIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵 ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ∈ 𝑈) | ||
| Syntax | cprmidl 32207 | Extend class notation with the class of prime ideals. |
| class PrmIdeal | ||
| Definition | df-prmidl 32208* | Define the class of prime ideals of a ring 𝑅. A proper ideal 𝐼 of 𝑅 is prime if whenever 𝐴𝐵 ⊆ 𝐼 for ideals 𝐴 and 𝐵, either 𝐴 ⊆ 𝐼 or 𝐵 ⊆ 𝐼. The more familiar definition using elements rather than ideals is equivalent provided 𝑅 is commutative; see prmidl2 32213 and isprmidlc 32220. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Theorem | prmidlval 32209* | The class of prime ideals of a ring 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Theorem | isprmidl 32210* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
| Theorem | prmidlnr 32211 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ≠ 𝐵) | ||
| Theorem | prmidl 32212* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) ∧ ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐽 (𝑥 · 𝑦) ∈ 𝑃) → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃)) | ||
| Theorem | prmidl2 32213* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 36529 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑃 ∈ (LIdeal‘𝑅)) ∧ (𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) → 𝑃 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | idlmulssprm 32214 | Let 𝑃 be a prime ideal containing the product (𝐼 × 𝐽) of two ideals 𝐼 and 𝐽. Then 𝐼 ⊆ 𝑃 or 𝐽 ⊆ 𝑃. (Contributed by Thierry Arnoux, 13-Apr-2024.) |
| ⊢ × = (LSSum‘(mulGrp‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑃 ∈ (PrmIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → (𝐼 × 𝐽) ⊆ 𝑃) ⇒ ⊢ (𝜑 → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃)) | ||
| Theorem | pridln1 32215 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ 1 ∈ 𝐼) | ||
| Theorem | prmidlidl 32216 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ∈ (LIdeal‘𝑅)) | ||
| Theorem | prmidlssidl 32217 | Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) ⊆ (LIdeal‘𝑅)) | ||
| Theorem | lidlnsg 32218 | An ideal is a normal subgroup. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) | ||
| Theorem | cringm4 32219 | Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 · 𝑌) · (𝑍 · 𝑊)) = ((𝑋 · 𝑍) · (𝑌 · 𝑊))) | ||
| Theorem | isprmidlc 32220* | The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in [Lang] p. 92. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))))) | ||
| Theorem | prmidlc 32221 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ (𝐼 · 𝐽) ∈ 𝑃)) → (𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃)) | ||
| Theorem | 0ringprmidl 32222 | The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (PrmIdeal‘𝑅) = ∅) | ||
| Theorem | prmidl0 32223 | The zero ideal of a commutative ring 𝑅 is a prime ideal if and only if 𝑅 is an integral domain. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ { 0 } ∈ (PrmIdeal‘𝑅)) ↔ 𝑅 ∈ IDomn) | ||
| Theorem | rhmpreimaprmidl 32224 | The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024.) |
| ⊢ 𝑃 = (PrmIdeal‘𝑅) ⇒ ⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝐽 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ∈ 𝑃) | ||
| Theorem | qsidomlem1 32225 | If the quotient ring of a commutative ring relative to an ideal is an integral domain, that ideal must be prime. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝐼 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | qsidomlem2 32226 | A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn) | ||
| Theorem | qsidom 32227 | An ideal 𝐼 in the commutative ring 𝑅 is prime if and only if the factor ring 𝑄 is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑄 ∈ IDomn ↔ 𝐼 ∈ (PrmIdeal‘𝑅))) | ||
| Syntax | cmxidl 32228 | Extend class notation with the class of maximal ideals. |
| class MaxIdeal | ||
| Definition | df-mxidl 32229* | Define the class of maximal ideals of a ring 𝑅. A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ MaxIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑗 ∈ (LIdeal‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = (Base‘𝑟))))}) | ||
| Theorem | mxidlval 32230* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (MaxIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑗 ∈ (LIdeal‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝐵)))}) | ||
| Theorem | ismxidl 32231* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑗 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝐵))))) | ||
| Theorem | mxidlidl 32232 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (LIdeal‘𝑅)) | ||
| Theorem | mxidlnr 32233 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵) | ||
| Theorem | mxidlmax 32234 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝐵)) | ||
| Theorem | mxidln1 32235 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ 1 ∈ 𝑀) | ||
| Theorem | mxidlnzr 32236 | A ring with a maximal ideal is a nonzero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑅 ∈ NzRing) | ||
| Theorem | mxidlprm 32237 | Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ × = (LSSum‘(mulGrp‘𝑅)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | ssmxidllem 32238* | The set 𝑃 used in the proof of ssmxidl 32239 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ≠ 𝐵) & ⊢ (𝜑 → 𝑍 ⊆ 𝑃) & ⊢ (𝜑 → 𝑍 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃) | ||
| Theorem | ssmxidl 32239* | Let 𝑅 be a ring, and let 𝐼 be a proper ideal of 𝑅. Then there is a maximal ideal of 𝑅 containing 𝐼. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝐼 ⊆ 𝑚) | ||
| Theorem | krull 32240* | Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ (𝑅 ∈ NzRing → ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅)) | ||
| Theorem | mxidlnzrb 32241* | A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅))) | ||
| Syntax | cidlsrg 32242 | Extend class notation with the semiring of ideals of a ring. |
| class IDLsrg | ||
| Definition | df-idlsrg 32243* | Define a structure for the ideals of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ IDLsrg = (𝑟 ∈ V ↦ ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩})) | ||
| Theorem | idlsrgstr 32244 | A constructed semiring of ideals is a structure. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩}) ⇒ ⊢ 𝑊 Struct ⟨1, ;10⟩ | ||
| Theorem | idlsrgval 32245* | Lemma for idlsrgbas 32246 through idlsrgtset 32250. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ⊗ = (LSSum‘𝐺) ⇒ ⊢ (𝑅 ∈ 𝑉 → (IDLsrg‘𝑅) = ({⟨(Base‘ndx), 𝐼⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}⟩})) | ||
| Theorem | idlsrgbas 32246 | Baae of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝐼 = (Base‘𝑆)) | ||
| Theorem | idlsrgplusg 32247 | Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → ⊕ = (+g‘𝑆)) | ||
| Theorem | idlsrg0g 32248 | The zero ideal is the additive identity of the semiring of ideals. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } = (0g‘𝑆)) | ||
| Theorem | idlsrgmulr 32249* | Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ⊗ = (LSSum‘𝐺) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) = (.r‘𝑆)) | ||
| Theorem | idlsrgtset 32250* | Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆)) | ||
| Theorem | idlsrgmulrval 32251 | Value of the ring multiplication for the ideals of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ · = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) = ((RSpan‘𝑅)‘(𝐼 · 𝐽))) | ||
| Theorem | idlsrgmulrcl 32252 | Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ∈ 𝐵) | ||
| Theorem | idlsrgmulrss1 32253 | In a commutative ring, the product of two ideals is a subset of the first one. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ 𝐼) | ||
| Theorem | idlsrgmulrss2 32254 | The product of two ideals is a subset of the second one. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ 𝐽) | ||
| Theorem | idlsrgmulrssin 32255 | In a commutative ring, the product of two ideals is a subset of their intersection. (Contributed by Thierry Arnoux, 17-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ (𝐼 ∩ 𝐽)) | ||
| Theorem | idlsrgmnd 32256 | The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Mnd) | ||
| Theorem | idlsrgcmnd 32257 | The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ CMnd) | ||
| Syntax | cufd 32258 | Class of unique factorization domains. |
| class UFD | ||
| Definition | df-ufd 32259* | Define the class of unique factorization domains. A unique factorization domain (UFD for short), is a commutative ring with an absolute value (from abvtriv 20300 this is equivalent to being a domain) such that every prime ideal contains a prime element (this is a characterization due to Irving Kaplansky). A UFD is sometimes also called a "factorial ring" following the terminology of Bourbaki. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ UFD = {𝑟 ∈ CRing ∣ ((AbsVal‘𝑟) ≠ ∅ ∧ ∀𝑖 ∈ (PrmIdeal‘𝑟)(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅)} | ||
| Theorem | isufd 32260* | The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐼 = (PrmIdeal‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) ⇒ ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ CRing ∧ (𝐴 ≠ ∅ ∧ ∀𝑖 ∈ 𝐼 (𝑖 ∩ 𝑃) ≠ ∅))) | ||
| Theorem | rprmval 32261* | The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))}) | ||
| Theorem | isrprm 32262* | Property for 𝑃 to be a prime element in the ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑃 ∈ (RPrime‘𝑅) ↔ (𝑃 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))))) | ||
| Theorem | asclmulg 32263 | Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ↑ = (.g‘𝑊) & ⊢ ∗ = (.g‘𝐹) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝐴‘(𝑁 ∗ 𝑋)) = (𝑁 ↑ (𝐴‘𝑋))) | ||
| Theorem | 0ringmon1p 32264 | There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑀 = ∅) | ||
| Theorem | fply1 32265 | Conditions for a function to be a univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (Base‘(Poly1‘𝑅)) & ⊢ (𝜑 → 𝐹:(ℕ0 ↑m 1o)⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑃) | ||
| Theorem | ply1scleq 32266 | Equality of a constant polynomial is the same as equality of the constant term. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐴‘𝐸) = (𝐴‘𝐹) ↔ 𝐸 = 𝐹)) | ||
| Theorem | evls1fn 32267 | Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → 𝑂 Fn 𝑈) | ||
| Theorem | evls1scafv 32268 | Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑄‘(𝐴‘𝑋))‘𝐶) = 𝑋) | ||
| Theorem | evls1expd 32269 | Univariate polynomial evaluation builder for an exponential. See also evl1expd 21711. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ ∧ = (.g‘(mulGrp‘𝑊)) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑁 ∧ 𝑀))‘𝐶) = (𝑁 ↑ ((𝑄‘𝑀)‘𝐶))) | ||
| Theorem | evls1varpwval 32270 | Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 21728. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑋 = (var1‘𝑈) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ ∧ = (.g‘(mulGrp‘𝑊)) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑁 ∧ 𝑋))‘𝐶) = (𝑁 ↑ 𝐶)) | ||
| Theorem | evls1fpws 32271* | Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ · = (.r‘𝑆) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ 𝐴 = (coe1‘𝑀) ⇒ ⊢ (𝜑 → (𝑄‘𝑀) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) | ||
| Theorem | ressply1evl 32272 | Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐸 = (eval1‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) ⇒ ⊢ (𝜑 → 𝑄 = (𝐸 ↾ 𝐵)) | ||
| Theorem | evls1addd 32273 | Univariate polynomial evaluation of a sum of polynomials. (Contributed by Thierry Arnoux, 8-Feb-2025.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ⨣ = (+g‘𝑊) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑀 ⨣ 𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) + ((𝑄‘𝑁)‘𝐶))) | ||
| Theorem | evls1muld 32274 | Univariate polynomial evaluation of a product of polynomials. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ × = (.r‘𝑊) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑀 × 𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) · ((𝑄‘𝑁)‘𝐶))) | ||
| Theorem | ressdeg1 32275 | The degree of a univariate polynomial in a structure restriction. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
| ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝐷‘𝑃) = (( deg1 ‘𝐻)‘𝑃)) | ||
| Theorem | ply1ascl0 32276 | The zero scalar as a polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
| ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 0 ) | ||
| Theorem | ressply10g 32277 | A restricted polynomial algebra has the same group identity (zero polynomial). (Contributed by Thierry Arnoux, 20-Jan-2025.) |
| ⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑍 = (0g‘𝑆) ⇒ ⊢ (𝜑 → 𝑍 = (0g‘𝑈)) | ||
| Theorem | ressply1mon1p 32278 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
| ⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑁 = (Monic1p‘𝐻) ⇒ ⊢ (𝜑 → 𝑁 = (𝐵 ∩ 𝑀)) | ||
| Theorem | ressply1invg 32279 | An element of a restricted polynomial algebra has the same group inverse. (Contributed by Thierry Arnoux, 30-Jan-2025.) |
| ⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((invg‘𝑈)‘𝑋) = ((invg‘𝑃)‘𝑋)) | ||
| Theorem | ressply1sub 32280 | A restricted polynomial algebra has the same subtraction operation. (Contributed by Thierry Arnoux, 30-Jan-2025.) |
| ⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(-g‘𝑈)𝑌) = (𝑋(-g‘𝑃)𝑌)) | ||
| Theorem | asclply1subcl 32281 | Closure of the algebra scalar injection function in a polynomial on a subring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝐴 = (algSc‘𝑉) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝑉 = (Poly1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑃 = (Base‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴‘𝑍) ∈ 𝑃) | ||
| Theorem | ply1chr 32282 | The characteristic of a polynomial ring is the characteristic of the underlying ring. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (chr‘𝑃) = (chr‘𝑅)) | ||
| Theorem | ply1fermltlchr 32283 | Fermat's little theorem for polynomials in a commutative ring 𝐹 of characteristic 𝑃 prime: we have the polynomial equation (𝑋 + 𝐴)↑𝑃 = ((𝑋↑𝑃) + 𝐴). (Contributed by Thierry Arnoux, 9-Jan-2025.) |
| ⊢ 𝑊 = (Poly1‘𝐹) & ⊢ 𝑋 = (var1‘𝐹) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (mulGrp‘𝑊) & ⊢ ↑ = (.g‘𝑁) & ⊢ 𝐶 = (algSc‘𝑊) & ⊢ 𝐴 = (𝐶‘((ℤRHom‘𝐹)‘𝐸)) & ⊢ 𝑃 = (chr‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐸 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝐴)) = ((𝑃 ↑ 𝑋) + 𝐴)) | ||
| Theorem | ply1fermltl 32284 | Fermat's little theorem for polynomials. If 𝑃 is prime, Then (𝑋 + 𝐴)↑𝑃 = ((𝑋↑𝑃) + 𝐴) modulo 𝑃. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑃) & ⊢ 𝑊 = (Poly1‘𝑍) & ⊢ 𝑋 = (var1‘𝑍) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (mulGrp‘𝑊) & ⊢ ↑ = (.g‘𝑁) & ⊢ 𝐶 = (algSc‘𝑊) & ⊢ 𝐴 = (𝐶‘((ℤRHom‘𝑍)‘𝐸)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐸 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝐴)) = ((𝑃 ↑ 𝑋) + 𝐴)) | ||
| Theorem | sra1r 32285 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 1 = (1r‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 1 = (1r‘𝐴)) | ||
| Theorem | sraring 32286 | Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ Ring) | ||
| Theorem | sradrng 32287 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing) | ||
| Theorem | srasubrg 32288 | A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴)) | ||
| Theorem | sralvec 32289 | Given a sub division ring 𝐹 of a division ring 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) ⇒ ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) | ||
| Theorem | srafldlvec 32290 | Given a subfield 𝐹 of a field 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) ⇒ ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) | ||
| Theorem | drgext0g 32291 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵)) | ||
| Theorem | drgextvsca 32292 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵)) | ||
| Theorem | drgext0gsca 32293 | The additive neutral element of the scalar field of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐵) = (0g‘(Scalar‘𝐵))) | ||
| Theorem | drgextsubrg 32294 | The scalar field is a subring of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵)) | ||
| Theorem | drgextlsp 32295 | The scalar field is a subspace of a subring algebra. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐵)) | ||
| Theorem | drgextgsum 32296* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌))) | ||
| Theorem | lvecdimfi 32297 | Finite version of lvecdim 20618 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18443, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ 𝐽) & ⊢ (𝜑 → 𝑇 ∈ 𝐽) & ⊢ (𝜑 → 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
| Syntax | cldim 32298 | Extend class notation with the dimension of a vector space. |
| class dim | ||
| Definition | df-dim 32299 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 20618, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
| ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) | ||
| Theorem | dimval 32300 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. (Contributed by Thierry Arnoux, 6-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝐹) ⇒ ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = (♯‘𝑆)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |