HomeTheorem List (p. 339 of 507)
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. 339 of 507) | < 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-31307) |
Hilbert Space Explorer
(31308-32830) |
Users' Mathboxes
(32831-50694) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | opprqusbas 33801 | The base of the quotient of the opposite ring is the same as the base of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (Base‘(oppr‘𝑄)) = (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))) | ||
| Theorem | opprqusplusg 33802 | The group operation of the quotient of the opposite ring is the same as the group operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) & ⊢ 𝐸 = (Base‘𝑄) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋(+g‘(oppr‘𝑄))𝑌) = (𝑋(+g‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) | ||
| Theorem | opprqus0g 33803 | The group identity element of the quotient of the opposite ring is the same as the group identity element of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) ⇒ ⊢ (𝜑 → (0g‘(oppr‘𝑄)) = (0g‘(𝑂 /s (𝑂 ~QG 𝐼)))) | ||
| Theorem | opprqusmulr 33804 | The multiplication operation of the quotient of the opposite ring is the same as the multiplication operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐸 = (Base‘𝑄) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋(.r‘(oppr‘𝑄))𝑌) = (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) | ||
| Theorem | opprqus1r 33805 | The ring unity of the quotient of the opposite ring is the same as the ring unity of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) ⇒ ⊢ (𝜑 → (1r‘(oppr‘𝑄)) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼)))) | ||
| Theorem | opprqusdrng 33806 | The quotient of the opposite ring is a division ring iff the opposite of the quotient ring is. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) ⇒ ⊢ (𝜑 → ((oppr‘𝑄) ∈ DivRing ↔ (𝑂 /s (𝑂 ~QG 𝐼)) ∈ DivRing)) | ||
| Theorem | qsdrngilem 33807* | Lemma for qsdrngi 33808. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅)) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑄)(𝑣(.r‘𝑄)[𝑋](𝑅 ~QG 𝑀)) = (1r‘𝑄)) | ||
| Theorem | qsdrngi 33808 | A quotient by a maximal left and maximal right ideal is a division ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂)) ⇒ ⊢ (𝜑 → 𝑄 ∈ DivRing) | ||
| Theorem | qsdrnglem2 33809 | Lemma for qsdrng 33810. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ DivRing) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ (𝐽 ∖ 𝑀)) ⇒ ⊢ (𝜑 → 𝐽 = 𝐵) | ||
| Theorem | qsdrng 33810 | An ideal 𝑀 is both left and right maximal if and only if the factor ring 𝑄 is a division ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑄 ∈ DivRing ↔ (𝑀 ∈ (MaxIdeal‘𝑅) ∧ 𝑀 ∈ (MaxIdeal‘𝑂)))) | ||
| Theorem | qsfld 33811 | An ideal 𝑀 in the commutative ring 𝑅 is maximal if and only if the factor ring 𝑄 is a field. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑄 ∈ Field ↔ 𝑀 ∈ (MaxIdeal‘𝑅))) | ||
| Theorem | mxidlprmALT 33812 | Every maximal ideal is prime - alternative proof. (Contributed by Thierry Arnoux, 15-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝑀 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | drnglring 33813 | A division ring is a local ring. (Contributed by Thierry Arnoux, 2-Jun-2026.) |
| ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝐹 ∈ LRing) | ||
| Theorem | dflring2 33814* | Alternate definition of a local ring. (Contributed by Thierry Arnoux, 2-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ − = (-g‘𝑅) ⇒ ⊢ (𝑅 ∈ LRing ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥) ∈ 𝑈))) | ||
| Theorem | dflringlem 33815 | Lemma for dflring3 33818. If a ring 𝑅 has a single maximal ideal 𝑀, then any element 𝑋 outside of 𝑀 is a unit. (Contributed by Thierry Arnoux, 2-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → (MaxIdeal‘𝑅) = {𝑀}) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑀)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑈) | ||
| Theorem | dflringlem2 33816 | Lemma for dflring3 33818. In a commutative local ring 𝑅, the set (𝐵 ∖ 𝑈) of non-units is an ideal. (Contributed by Thierry Arnoux, 2-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ LRing) ⇒ ⊢ (𝜑 → (𝐵 ∖ 𝑈) ∈ (LIdeal‘𝑅)) | ||
| Theorem | dflringlem3 33817 | Lemma for dflring3 33818. In a commutative local ring 𝑅, the set (𝐵 ∖ 𝑈) of non-units is a maximal ideal. (Contributed by Thierry Arnoux, 2-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ LRing) ⇒ ⊢ (𝜑 → (𝐵 ∖ 𝑈) ∈ (MaxIdeal‘𝑅)) | ||
| Theorem | dflring3 33818 | Alternate definition of a local ring: local rings have a single maximal ideal. (Contributed by Thierry Arnoux, 2-Jun-2026.) |
| ⊢ (𝑅 ∈ CRing → (𝑅 ∈ LRing ↔ (MaxIdeal‘𝑅) ≈ 1o)) | ||
| Theorem | dflring4 33819 | Alternate definition of a local ring: the set (𝐵 ∖ 𝑈) of non-units is an ideal. (Contributed by Thierry Arnoux, 2-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑅 ∈ LRing ↔ (𝐵 ∖ 𝑈) ∈ (LIdeal‘𝑅))) | ||
| Theorem | fldlring 33820 | A field is a local ring. (Contributed by Thierry Arnoux, 3-Jun-2026.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → 𝐹 ∈ Field) ⇒ ⊢ (𝜑 → 𝐹 ∈ LRing) | ||
| Syntax | cidlsrg 33821 | Extend class notation with the semiring of ideals of a ring. |
| class IDLsrg | ||
| Definition | df-idlsrg 33822* | 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 33823 | 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 33824* | Lemma for idlsrgbas 33825 through idlsrgtset 33829. (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 33825 | Base of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝐼 = (Base‘𝑆)) | ||
| Theorem | idlsrgplusg 33826 | Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → ⊕ = (+g‘𝑆)) | ||
| Theorem | idlsrg0g 33827 | 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 33828* | Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ⊗ = (LSSum‘𝐺) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) = (.r‘𝑆)) | ||
| Theorem | idlsrgtset 33829* | Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆)) | ||
| Theorem | idlsrgmulrval 33830 | 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 33831 | Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ∈ 𝐵) | ||
| Theorem | idlsrgmulrss1 33832 | 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 33833 | 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 33834 | 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 33835 | The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Mnd) | ||
| Theorem | idlsrgcmnd 33836 | The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ CMnd) | ||
| Theorem | rprmval 33837* | The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))}) | ||
| Theorem | isrprm 33838* | 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 | rprmcl 33839 | A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | rprmdvds 33840 | If a ring prime 𝑄 divides a product 𝑋 · 𝑌, then it divides either 𝑋 or 𝑌. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∥ (𝑋 · 𝑌)) ⇒ ⊢ (𝜑 → (𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑌)) | ||
| Theorem | rprmnz 33841 | A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑄 ≠ 0 ) | ||
| Theorem | rprmnunit 33842 | A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈) | ||
| Theorem | rsprprmprmidl 33843 | In a commutative ring, ideals generated by prime elements are prime ideals. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ (RPrime‘𝑅)) ⇒ ⊢ (𝜑 → (𝐾‘{𝑃}) ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | rsprprmprmidlb 33844 | An ideal generated by a single element is a prime iff that element is prime. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑃 ↔ (𝐾‘{𝑋}) ∈ (PrmIdeal‘𝑅))) | ||
| Theorem | rprmndvdsr1 33845 | A ring prime element does not divide the ring multiplicative identity. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → ¬ 𝑄 ∥ 1 ) | ||
| Theorem | rprmasso 33846 | In an integral domain, the associate of a prime is a prime. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∥ 𝑌) & ⊢ (𝜑 → 𝑌 ∥ 𝑋) ⇒ ⊢ (𝜑 → 𝑌 ∈ 𝑃) | ||
| Theorem | rprmasso2 33847 | In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∥ 𝑌) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑌 ∥ 𝑋) | ||
| Theorem | rprmasso3 33848* | In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∥ 𝑌) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ 𝑈 (𝑡 · 𝑋) = 𝑌) | ||
| Theorem | unitmulrprm 33849 | A ring unit multiplied by a ring prime is a ring prime. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐼 · 𝑄) ∈ 𝑃) | ||
| Theorem | rprmndvdsru 33850 | A ring prime element does not divide any ring unit. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) ⇒ ⊢ (𝜑 → ¬ 𝑄 ∥ 𝑇) | ||
| Theorem | rprmirredlem 33851 | Lemma for rprmirred 33852. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑄 ≠ 0 ) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈)) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 = (𝑋 · 𝑌)) & ⊢ (𝜑 → 𝑄 ∥ 𝑋) ⇒ ⊢ (𝜑 → 𝑌 ∈ 𝑈) | ||
| Theorem | rprmirred 33852 | In an integral domain, ring primes are irreducible. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝐼 = (Irred‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝐼) | ||
| Theorem | rprmirredb 33853 | In a principal ideal domain, the converse of rprmirred 33852 holds, i.e. irreducible elements are prime. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝐼 = (Irred‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ PID) ⇒ ⊢ (𝜑 → 𝐼 = 𝑃) | ||
| Theorem | rprmdvdspow 33854 | If a prime element divides a ring "power", it divides the term. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝑀) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑄 ∥ (𝑁 ↑ 𝑋)) ⇒ ⊢ (𝜑 → 𝑄 ∥ 𝑋) | ||
| Theorem | rprmdvdsprod 33855* | If a prime element 𝑄 divides a product, then it divides one term. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 finSupp 1 ) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ (𝜑 → 𝑄 ∥ (𝑀 Σg 𝐹)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐹 supp 1 )𝑄 ∥ (𝐹‘𝑥)) | ||
| Theorem | 1arithidomlem1 33856* | Lemma for 1arithidom 33858. (Contributed by Thierry Arnoux, 30-May-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐽 = (0..^(♯‘𝐹)) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺)) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → ∀𝑔 ∈ Word 𝑃(∃𝑘 ∈ 𝑈 (𝑀 Σg 𝐹) = (𝑘 · (𝑀 Σg 𝑔)) → ∃𝑤∃𝑢 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑤:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ 𝑔 = (𝑢 ∘f · (𝐹 ∘ 𝑤))))) & ⊢ (𝜑 → 𝐻 ∈ Word 𝑃) & ⊢ (𝜑 → ∃𝑘 ∈ 𝑈 (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑘 · (𝑀 Σg 𝐻))) & ⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐻))) & ⊢ (𝜑 → 𝑄(∥r‘𝑅)(𝐻‘𝐾)) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) & ⊢ (𝜑 → (𝑇 · 𝑄) = (𝐻‘𝐾)) & ⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) & ⊢ (𝜑 → (𝐻 ∘ 𝑆) = (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻‘𝐾)”⟩)) & ⊢ (𝜑 → 𝑁 ∈ 𝑈) & ⊢ (𝜑 → (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑁 · (𝑀 Σg 𝐻))) ⇒ ⊢ (𝜑 → ∃𝑐∃𝑑 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑐:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = (𝑑 ∘f · (𝐹 ∘ 𝑐)))) | ||
| Theorem | 1arithidomlem2 33857* | Lemma for 1arithidom 33858: induction step. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐽 = (0..^(♯‘𝐹)) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺)) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → ∀𝑔 ∈ Word 𝑃(∃𝑘 ∈ 𝑈 (𝑀 Σg 𝐹) = (𝑘 · (𝑀 Σg 𝑔)) → ∃𝑤∃𝑢 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑤:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ 𝑔 = (𝑢 ∘f · (𝐹 ∘ 𝑤))))) & ⊢ (𝜑 → 𝐻 ∈ Word 𝑃) & ⊢ (𝜑 → ∃𝑘 ∈ 𝑈 (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑘 · (𝑀 Σg 𝐻))) & ⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐻))) & ⊢ (𝜑 → 𝑄(∥r‘𝑅)(𝐻‘𝐾)) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) & ⊢ (𝜑 → (𝑇 · 𝑄) = (𝐻‘𝐾)) & ⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) & ⊢ (𝜑 → (𝐻 ∘ 𝑆) = (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻‘𝐾)”⟩)) & ⊢ (𝜑 → 𝑁 ∈ 𝑈) & ⊢ (𝜑 → (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑁 · (𝑀 Σg 𝐻))) & ⊢ (𝜑 → 𝐷 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))) & ⊢ (𝜑 → 𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹))) & ⊢ (𝜑 → ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = (𝐷 ∘f · (𝐹 ∘ 𝐶))) ⇒ ⊢ (𝜑 → (((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ ◡𝑆):(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩)))–1-1-onto→(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) ∧ 𝐻 = (((𝐷 ++ ⟨“𝑇”⟩) ∘ ◡𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ ◡𝑆))))) | ||
| Theorem | 1arithidom 33858* | Uniqueness of prime factorizations in an integral domain 𝑅. Given two equal products 𝐹 and 𝐺 of prime elements, 𝐹 and 𝐺 are equal up to a renumbering 𝑤 and a multiplication by units 𝑢. See also 1arith 17012. Chapter VII, Paragraph 3, Section 3, Proposition 2 of [BourbakiCAlg2], p. 228. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐽 = (0..^(♯‘𝐹)) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺)) ⇒ ⊢ (𝜑 → ∃𝑤∃𝑢 ∈ (𝑈 ↑m 𝐽)(𝑤:𝐽–1-1-onto→𝐽 ∧ 𝐺 = (𝑢 ∘f · (𝐹 ∘ 𝑤)))) | ||
| Syntax | cufd 33859 | Class of unique factorization domains. |
| class UFD | ||
| Definition | df-ufd 33860* | Define the class of unique factorization domains. A unique factorization domain (UFD for short), is an integral domain such that every nonzero 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.) Exclude the 0 prime ideal. (Revised by Thierry Arnoux, 9-May-2025.) Exclude the 0 ring. (Revised by Thierry Arnoux, 14-Jun-2025.) |
| ⊢ UFD = {𝑟 ∈ IDomn ∣ ∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅} | ||
| Theorem | isufd 33861* | The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐼 = (PrmIdeal‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅)) | ||
| Theorem | ufdprmidl 33862* | In a unique factorization domain 𝑅, a nonzero prime ideal 𝐽 contains a prime element 𝑝. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐼 = (PrmIdeal‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ UFD) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) & ⊢ (𝜑 → 𝐽 ≠ { 0 }) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 𝑝 ∈ 𝐽) | ||
| Theorem | ufdidom 33863 | A nonzero unique factorization domain is an integral domain. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ UFD) ⇒ ⊢ (𝜑 → 𝑅 ∈ IDomn) | ||
| Theorem | pidufd 33864 | Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ PID) ⇒ ⊢ (𝜑 → 𝑅 ∈ UFD) | ||
| Theorem | 1arithufdlem1 33865* | Lemma for 1arithufd 33869. The set 𝑆 of elements which can be written as a product of primes is not empty. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ UFD) & ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing) & ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)} ⇒ ⊢ (𝜑 → 𝑆 ≠ ∅) | ||
| Theorem | 1arithufdlem2 33866* | Lemma for 1arithufd 33869. The set 𝑆 of elements which can be written as a product of primes is multiplicatively closed. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ UFD) & ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing) & ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)} & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑆) | ||
| Theorem | 1arithufdlem3 33867* | Lemma for 1arithufd 33869. If a product (𝑌 · 𝑋) can be written as a product of primes, with 𝑋 non-unit, nonzero, so can 𝑋. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ UFD) & ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing) & ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)} & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑆) | ||
| Theorem | 1arithufdlem4 33868* | Lemma for 1arithufd 33869. Nonzero ring, non-field case. Those trivial cases are handled in the final proof. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ UFD) & ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing) & ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)} & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑆) | ||
| Theorem | 1arithufd 33869* | Existence of a factorization into irreducible elements in a unique factorization domain. Any nonzero, non-unit element 𝑋 of a UFD 𝑅 can be written as a product of primes 𝑓. As shown in 1arithidom 33858, that factorization is unique, up to the order of the factors and multiplication by units. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ UFD) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ Word 𝑃𝑋 = (𝑀 Σg 𝑓)) | ||
| Theorem | dfufd2lem 33870 | Lemma for dfufd2 33871. (Contributed by Thierry Arnoux, 6-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐼 ∈ (PrmIdeal‘𝑅)) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ 𝐼) & ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼 ∩ 𝑃) ≠ ∅) | ||
| Theorem | dfufd2 33871* | Alternative definition of unique factorization domain (UFD). This is often the textbook definition. Chapter VII, Paragraph 3, Section 3, Proposition 2 of [BourbakiCAlg2], p. 228. (Contributed by Thierry Arnoux, 6-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓))) | ||
| Theorem | zringidom 33872 | The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ ℤring ∈ IDomn | ||
| Theorem | zringpid 33873 | The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ ℤring ∈ PID | ||
| Theorem | dfprm3 33874 | The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ ℙ = (ℕ ∩ (RPrime‘ℤring)) | ||
| Theorem | zringfrac 33875* | The field of fractions of the ring of integers is isomorphic to the field of the rational numbers. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ ∼ = (ℤring ~RL (ℤ ∖ {0})) & ⊢ 𝐹 = (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ) ⇒ ⊢ 𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤring)) | ||
| Theorem | assaassd 33876 | Left-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
| Theorem | assaassrd 33877 | Right-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))) | ||
| Theorem | 0ringmon1p 33878 | There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → 𝑀 = ∅) | ||
| Theorem | fply1 33879 | 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 | ply1lvec 33880 | In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑃 ∈ LVec) | ||
| Theorem | evls1fn 33881 | Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → 𝑂 Fn 𝑈) | ||
| Theorem | evls1dm 33882 | The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → dom 𝑂 = 𝑈) | ||
| Theorem | evls1fvf 33883 | The subring evaluation function for a univariate polynomial as a function, with domain and codomain. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑂‘𝑄):𝐵⟶𝐵) | ||
| Theorem | evl1fvf 33884 | The univariate polynomial evaluation function as a function, with domain and codomain. (Contributed by Thierry Arnoux, 8-Jun-2025.) |
| ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑂‘𝑄):𝐵⟶𝐵) | ||
| Theorem | evl1fpws 33885* | Evaluation of a univariate polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.) |
| ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) & ⊢ · = (.r‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝐴 = (coe1‘𝑀) ⇒ ⊢ (𝜑 → (𝑂‘𝑀) = (𝑥 ∈ 𝐵 ↦ (𝑅 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) | ||
| Theorem | ressply1evls1 33886 | Subring evaluation of a univariate polynomial is the same as the subring evaluation in the bigger ring. (Contributed by Thierry Arnoux, 14-Nov-2025.) |
| ⊢ 𝐺 = (𝐸 ↾s 𝑅) & ⊢ 𝑂 = (𝐸 evalSub1 𝑆) & ⊢ 𝑄 = (𝐺 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝐾 = (𝐸 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐸 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝐸)) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝐺)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑄‘𝐹) = ((𝑂‘𝐹) ↾ 𝑅)) | ||
| Theorem | ressdeg1 33887 | The degree of a univariate polynomial in a structure restriction. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
| ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝐷‘𝑃) = ((deg1‘𝐻)‘𝑃)) | ||
| Theorem | ressply10g 33888 | 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 33889 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
| ⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑁 = (Monic1p‘𝐻) ⇒ ⊢ (𝜑 → 𝑁 = (𝐵 ∩ 𝑀)) | ||
| Theorem | ressply1invg 33890 | 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 33891 | 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 | ressasclcl 33892 | Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ 𝐵) | ||
| Theorem | evls1subd 33893 | Univariate polynomial evaluation of a difference of polynomials. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐷 = (-g‘𝑊) & ⊢ − = (-g‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑀𝐷𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) − ((𝑄‘𝑁)‘𝐶))) | ||
| Theorem | deg1le0eq0 33894 | A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 26307. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑂 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 0) ⇒ ⊢ (𝜑 → (𝐹 = 𝑂 ↔ ((coe1‘𝐹)‘0) = 0 )) | ||
| Theorem | ply1asclunit 33895 | A nonzero scalar polynomial over a field 𝐹 is a unit. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑃 = (Poly1‘𝐹) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐴‘𝑌) ∈ (Unit‘𝑃)) | ||
| Theorem | ply1unit 33896 | In a field 𝐹, a polynomial 𝐶 is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit 33895. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝐹) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ 𝐷 = (deg1‘𝐹) & ⊢ (𝜑 → 𝐶 ∈ (Base‘𝑃)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (Unit‘𝑃) ↔ (𝐷‘𝐶) = 0)) | ||
| Theorem | evl1deg1 33897 | Evaluation of a univariate polynomial of degree 1. (Contributed by Thierry Arnoux, 8-Jun-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐶 = (coe1‘𝑀) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐴 = (𝐶‘1) & ⊢ 𝐵 = (𝐶‘0) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) & ⊢ (𝜑 → (𝐷‘𝑀) = 1) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · 𝑋) + 𝐵)) | ||
| Theorem | evl1deg2 33898 | Evaluation of a univariate polynomial of degree 2. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝐹 = (coe1‘𝑀) & ⊢ 𝐸 = (deg1‘𝑅) & ⊢ 𝐴 = (𝐹‘2) & ⊢ 𝐵 = (𝐹‘1) & ⊢ 𝐶 = (𝐹‘0) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) & ⊢ (𝜑 → (𝐸‘𝑀) = 2) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐵 · 𝑋) + 𝐶))) | ||
| Theorem | evl1deg3 33899 | Evaluation of a univariate polynomial of degree 3. (Contributed by Thierry Arnoux, 14-Jun-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝐹 = (coe1‘𝑀) & ⊢ 𝐸 = (deg1‘𝑅) & ⊢ 𝐴 = (𝐹‘3) & ⊢ 𝐵 = (𝐹‘2) & ⊢ 𝐶 = (𝐹‘1) & ⊢ 𝐷 = (𝐹‘0) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) & ⊢ (𝜑 → (𝐸‘𝑀) = 3) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = (((𝐴 · (3 ↑ 𝑋)) + (𝐵 · (2 ↑ 𝑋))) + ((𝐶 · 𝑋) + 𝐷))) | ||
| Theorem | evls1monply1 33900 | Subring evaluation of a scaled monomial. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝑋 = (var1‘𝑈) & ⊢ ↑ = (.g‘(mulGrp‘𝑊)) & ⊢ ∧ = (.g‘(mulGrp‘𝑆)) & ⊢ ∗ = ( ·𝑠 ‘𝑊) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑄‘(𝐴 ∗ (𝑁 ↑ 𝑋)))‘𝑌) = (𝐴 · (𝑁 ∧ 𝑌))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |