HomeTheorem List (p. 203 of 502)
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. 203 of 502) | < 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-31005) |
Hilbert Space Explorer
(31006-32528) |
Users' Mathboxes
(32529-50158) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ringideu 20201* | The unity element of a ring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑢) = 𝑥)) | ||
| Theorem | crngcomd 20202 | Multiplication is commutative in a commutative ring. (Contributed by SN, 8-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑌 · 𝑋)) | ||
| Theorem | crngbascntr 20203 | The base set of a commutative ring is its center. (Contributed by SN, 21-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntr‘(mulGrp‘𝐺)) ⇒ ⊢ (𝐺 ∈ CRing → 𝐵 = 𝑍) | ||
| Theorem | ringassd 20204 | Associative law for multiplication in a ring. (Contributed by SN, 14-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍))) | ||
| Theorem | crng12d 20205 | Commutative/associative law that swaps the first two factors in a triple product in a commutative ring. See also mul12d 11354. (Contributed by SN, 8-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑌 · 𝑍)) = (𝑌 · (𝑋 · 𝑍))) | ||
| Theorem | crng32d 20206 | Commutative/associative law that swaps the last two factors in a triple product in a commutative ring. See also mul32d 11355. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) · 𝑍) = ((𝑋 · 𝑍) · 𝑌)) | ||
| Theorem | ringcld 20207 | Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) | ||
| Theorem | ringdi 20208 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) | ||
| Theorem | ringdir 20209 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
| Theorem | ringdid 20210 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) | ||
| Theorem | ringdird 20211 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
| Theorem | ringidcl 20212 | The unity element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵) | ||
| Theorem | ringidcld 20213 | The unity element of a ring belongs to the base set of the ring, deduction version. (Contributed by SN, 16-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 1 ∈ 𝐵) | ||
| Theorem | ring0cl 20214 | The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) | ||
| Theorem | ringidmlem 20215 | Lemma for ringlidm 20216 and ringridm 20217. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋)) | ||
| Theorem | ringlidm 20216 | The unity element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 1 · 𝑋) = 𝑋) | ||
| Theorem | ringridm 20217 | The unity element of a ring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 · 1 ) = 𝑋) | ||
| Theorem | isringid 20218* | Properties showing that an element 𝐼 is the unity element of a ring. (Contributed by NM, 7-Aug-2013.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ((𝐼 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥)) ↔ 1 = 𝐼)) | ||
| Theorem | ringlidmd 20219 | The unity element of a ring is a left multiplicative identity. (Contributed by SN, 14-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 1 · 𝑋) = 𝑋) | ||
| Theorem | ringridmd 20220 | The unity element of a ring is a right multiplicative identity. (Contributed by SN, 14-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 1 ) = 𝑋) | ||
| Theorem | ringid 20221* | The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ∃𝑢 ∈ 𝐵 ((𝑢 · 𝑋) = 𝑋 ∧ (𝑋 · 𝑢) = 𝑋)) | ||
| Theorem | ringo2times 20222 | A ring element plus itself is two times the element. "Two" in an arbitrary unital ring is the sum of the unity element with itself. (Contributed by AV, 24-Aug-2021.) Variant of o2timesd 20157 for rings. (Revised by AV, 5-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵) → (𝐴 + 𝐴) = (( 1 + 1 ) · 𝐴)) | ||
| Theorem | ringadd2 20223* | A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.) (Proof shortened by AV, 1-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ∃𝑥 ∈ 𝐵 (𝑋 + 𝑋) = ((𝑥 + 𝑥) · 𝑋)) | ||
| Theorem | ringidss 20224 | A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
| ⊢ 𝑀 = ((mulGrp‘𝑅) ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 1 = (0g‘𝑀)) | ||
| Theorem | ringacl 20225 | Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
| Theorem | ringcomlem 20226 | Lemma for ringcom 20227. This (formerly) part of the proof for ringcom 20227 is also applicable for semirings (without using the commutativity of the addition given per definition of a semiring), see srgcom4lem 20160. (Contributed by Gérard Lang, 4-Dec-2014.) Variant of rglcom4d 20158 for rings. (Revised by AV, 5-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑋) + (𝑌 + 𝑌)) = ((𝑋 + 𝑌) + (𝑋 + 𝑌))) | ||
| Theorem | ringcom 20227 | Commutativity of the additive group of a ring. (See also lmodcom 20871.) This proof requires the existence of a multiplicative identity, and the existence of additive inverses. Therefore, this proof is not applicable for semirings. (Contributed by Gérard Lang, 4-Dec-2014.) (Proof shortened by AV, 1-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | ringabl 20228 | A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.) |
| ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel) | ||
| Theorem | ringcmn 20229 | A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) | ||
| Theorem | ringabld 20230 | A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑅 ∈ Abel) | ||
| Theorem | ringcmnd 20231 | A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑅 ∈ CMnd) | ||
| Theorem | ringrng 20232 | A unital ring is a non-unital ring. (Contributed by AV, 6-Jan-2020.) |
| ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng) | ||
| Theorem | ringssrng 20233 | The unital rings are non-unital rings. (Contributed by AV, 20-Mar-2020.) |
| ⊢ Ring ⊆ Rng | ||
| Theorem | isringrng 20234* | The predicate "is a unital ring" as extension of the predicate "is a non-unital ring". (Contributed by AV, 17-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Rng ∧ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑦 ∧ (𝑦 · 𝑥) = 𝑦))) | ||
| Theorem | ringpropd 20235* | If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a ring iff the other one is. (Contributed by Mario Carneiro, 6-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Ring ↔ 𝐿 ∈ Ring)) | ||
| Theorem | crngpropd 20236* | If two structures have the same group components (properties), one is a commutative ring iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ CRing ↔ 𝐿 ∈ CRing)) | ||
| Theorem | ringprop 20237 | If two structures have the same ring components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) |
| ⊢ (Base‘𝐾) = (Base‘𝐿) & ⊢ (+g‘𝐾) = (+g‘𝐿) & ⊢ (.r‘𝐾) = (.r‘𝐿) ⇒ ⊢ (𝐾 ∈ Ring ↔ 𝐿 ∈ Ring) | ||
| Theorem | isringd 20238* | Properties that determine a ring. (Contributed by NM, 2-Aug-2013.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) & ⊢ (𝜑 → 1 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥) ⇒ ⊢ (𝜑 → 𝑅 ∈ Ring) | ||
| Theorem | iscrngd 20239* | Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) & ⊢ (𝜑 → 1 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) ⇒ ⊢ (𝜑 → 𝑅 ∈ CRing) | ||
| Theorem | ringlz 20240 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (Proof shortened by AV, 30-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) | ||
| Theorem | ringrz 20241 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (Proof shortened by AV, 30-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 ) | ||
| Theorem | ringlzd 20242 | The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 0 · 𝑋) = 0 ) | ||
| Theorem | ringrzd 20243 | The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 0 ) = 0 ) | ||
| Theorem | ringsrg 20244 | Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) | ||
| Theorem | ring1eq0 20245 | If one and zero are equal, then any two elements of a ring are equal. Alternately, every ring has one distinct from zero except the zero ring containing the single element {0}. (Contributed by Mario Carneiro, 10-Sep-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( 1 = 0 → 𝑋 = 𝑌)) | ||
| Theorem | ring1ne0 20246 | If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 1 < (♯‘𝐵)) → 1 ≠ 0 ) | ||
| Theorem | ringinvnz1ne0 20247* | In a unital ring, a left invertible element is different from zero iff 1 ≠ 0. (Contributed by FL, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 (𝑎 · 𝑋) = 1 ) ⇒ ⊢ (𝜑 → (𝑋 ≠ 0 ↔ 1 ≠ 0 )) | ||
| Theorem | ringinvnzdiv 20248* | In a unital ring, a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010.) (Revised by Jeff Madsen, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 (𝑎 · 𝑋) = 1 ) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑌 = 0 )) | ||
| Theorem | ringnegl 20249 | Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 38186 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘ 1 ) · 𝑋) = (𝑁‘𝑋)) | ||
| Theorem | ringnegr 20250 | Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 38187 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑁‘ 1 )) = (𝑁‘𝑋)) | ||
| Theorem | ringmneg1 20251 | Negation of a product in a ring. (mulneg1 11585 analog.) Compared with rngmneg1 20114, the proof is shorter making use of the existence of a ring unity. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) · 𝑌) = (𝑁‘(𝑋 · 𝑌))) | ||
| Theorem | ringmneg2 20252 | Negation of a product in a ring. (mulneg2 11586 analog.) Compared with rngmneg2 20115, the proof is shorter making use of the existence of a ring unity. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑁‘𝑌)) = (𝑁‘(𝑋 · 𝑌))) | ||
| Theorem | ringm2neg 20253 | Double negation of a product in a ring. (mul2neg 11588 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌)) | ||
| Theorem | ringsubdi 20254 | Ring multiplication distributes over subtraction. (subdi 11582 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍))) | ||
| Theorem | ringsubdir 20255 | Ring multiplication distributes over subtraction. (subdir 11583 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍))) | ||
| Theorem | mulgass2 20256 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ × = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌))) | ||
| Theorem | ring1 20257 | The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.) |
| ⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩} ⇒ ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Ring) | ||
| Theorem | ringn0 20258 | Rings exist. (Contributed by AV, 29-Apr-2019.) |
| ⊢ Ring ≠ ∅ | ||
| Theorem | ringlghm 20259* | Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 GrpHom 𝑅)) | ||
| Theorem | ringrghm 20260* | Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) ∈ (𝑅 GrpHom 𝑅)) | ||
| Theorem | gsummulc1OLD 20261* | Obsolete version of gsummulc1 20263 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌)) | ||
| Theorem | gsummulc2OLD 20262* | Obsolete version of gsummulc2 20264 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑌 · 𝑋))) = (𝑌 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)))) | ||
| Theorem | gsummulc1 20263* | A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) Remove unused hypothesis. (Revised by SN, 7-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌)) | ||
| Theorem | gsummulc2 20264* | A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) Remove unused hypothesis. (Revised by SN, 7-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑌 · 𝑋))) = (𝑌 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)))) | ||
| Theorem | gsummgp0 20265* | If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019.) |
| ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅)) & ⊢ ((𝜑 ∧ 𝑛 = 𝑖) → 𝐴 = 𝐵) & ⊢ (𝜑 → ∃𝑖 ∈ 𝑁 𝐵 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ 𝐴)) = 0 ) | ||
| Theorem | gsumdixp 20266* | Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.) (Revised by AV, 10-Jul-2019.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑋) finSupp 0 ) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑌) finSupp 0 ) ⇒ ⊢ (𝜑 → ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ 𝑋)) · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌))) = (𝑅 Σg (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)))) | ||
| Theorem | prdsmulrcl 20267 | A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015.) (Proof shortened by AV, 30-Mar-2025.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵) | ||
| Theorem | prdsringd 20268 | A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Ring) ⇒ ⊢ (𝜑 → 𝑌 ∈ Ring) | ||
| Theorem | prdscrngd 20269 | A product of commutative rings is a commutative ring. Since the resulting ring will have zero divisors in all nontrivial cases, this cannot be strengthened much further. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶CRing) ⇒ ⊢ (𝜑 → 𝑌 ∈ CRing) | ||
| Theorem | prds1 20270 | Value of the ring unity in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Ring) ⇒ ⊢ (𝜑 → (1r ∘ 𝑅) = (1r‘𝑌)) | ||
| Theorem | pwsring 20271 | A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Ring) | ||
| Theorem | pws1 20272 | Value of the ring unity in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 1 }) = (1r‘𝑌)) | ||
| Theorem | pwscrng 20273 | A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CRing) | ||
| Theorem | pwsmgp 20274 | The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (𝑀 ↑s 𝐼) & ⊢ 𝑁 = (mulGrp‘𝑌) & ⊢ 𝐵 = (Base‘𝑁) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ + = (+g‘𝑁) & ⊢ ✚ = (+g‘𝑍) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 = 𝐶 ∧ + = ✚ )) | ||
| Theorem | pwspjmhmmgpd 20275* | The projection given by pwspjmhm 18767 is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑀 MndHom 𝑇)) | ||
| Theorem | pwsexpg 20276 | Value of a group exponentiation in a structure power. Compare pwsmulg 19061. (Contributed by SN, 30-Jul-2024.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ ∙ = (.g‘𝑀) & ⊢ · = (.g‘𝑇) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑋)‘𝐴) = (𝑁 · (𝑋‘𝐴))) | ||
| Theorem | pwsgprod 20277* | Finite products in a power structure are taken componentwise. Compare pwsgsum 19923. (Contributed by SN, 30-Jul-2024.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) | ||
| Theorem | imasring 20278* | The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑈 ∈ Ring ∧ (𝐹‘ 1 ) = (1r‘𝑈))) | ||
| Theorem | imasringf1 20279 | The image of a ring under an injection is a ring (imasmndf1 18713 analog). (Contributed by AV, 27-Feb-2025.) |
| ⊢ 𝑈 = (𝐹 “s 𝑅) & ⊢ 𝑉 = (Base‘𝑅) ⇒ ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Ring) → 𝑈 ∈ Ring) | ||
| Theorem | xpsringd 20280 | A product of two rings is a ring (xpsmnd 18714 analog). (Contributed by AV, 28-Feb-2025.) |
| ⊢ 𝑌 = (𝑆 ×s 𝑅) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑌 ∈ Ring) | ||
| Theorem | xpsring1d 20281 | The multiplicative identity element of a binary product of rings. (Contributed by AV, 16-Mar-2025.) |
| ⊢ 𝑌 = (𝑆 ×s 𝑅) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (1r‘𝑌) = ⟨(1r‘𝑆), (1r‘𝑅)⟩) | ||
| Theorem | qusring2 20282* | The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞))) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑈 ∈ Ring ∧ [ 1 ] ∼ = (1r‘𝑈))) | ||
| Theorem | crngbinom 20283* | The binomial theorem for commutative rings (special case of csrgbinom 20179): (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)). (Contributed by AV, 24-Aug-2019.) |
| ⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) | ||
| Syntax | coppr 20284 | The opposite ring operation. |
| class oppr | ||
| Definition | df-oppr 20285 | Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ oppr = (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.r‘ndx), tpos (.r‘𝑓)⟩)) | ||
| Theorem | opprval 20286 | Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ 𝑂 = (𝑅 sSet ⟨(.r‘ndx), tpos · ⟩) | ||
| Theorem | opprmulfval 20287 | Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (.r‘𝑂) ⇒ ⊢ ∙ = tpos · | ||
| Theorem | opprmul 20288 | Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (.r‘𝑂) ⇒ ⊢ (𝑋 ∙ 𝑌) = (𝑌 · 𝑋) | ||
| Theorem | crngoppr 20289 | In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 20365). (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (.r‘𝑂) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∙ 𝑌)) | ||
| Theorem | opprlem 20290 | Lemma for opprbas 20291 and oppradd 20292. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (.r‘ndx) ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑂) | ||
| Theorem | opprbas 20291 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
| Theorem | oppradd 20292 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ + = (+g‘𝑂) | ||
| Theorem | opprrng 20293 | An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → 𝑂 ∈ Rng) | ||
| Theorem | opprrngb 20294 | A class is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 20293. (Contributed by AV, 15-Feb-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng ↔ 𝑂 ∈ Rng) | ||
| Theorem | opprring 20295 | An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) (Proof shortened by AV, 30-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring) | ||
| Theorem | opprringb 20296 | Bidirectional form of opprring 20295. (Contributed by Mario Carneiro, 6-Dec-2014.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring ↔ 𝑂 ∈ Ring) | ||
| Theorem | oppr0 20297 | Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 0 = (0g‘𝑂) | ||
| Theorem | oppr1 20298 | Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ 1 = (1r‘𝑂) | ||
| Theorem | opprneg 20299 | The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ 𝑁 = (invg‘𝑂) | ||
| Theorem | opprsubg 20300 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (SubGrp‘𝑅) = (SubGrp‘𝑂) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |