P. 205 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20401-20500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	crng4 20401	Commutative/associative law for commutative rings. See also mul4d 11449. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by AV, 20-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) · (𝑍 · 𝑈)) = ((𝑋 · 𝑍) · (𝑌 · 𝑈)))
Theorem	ringdi 20402	Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)))
Theorem	ringdir 20403	Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Theorem	ringdid 20404	Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)))
Theorem	ringdird 20405	Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Theorem	ringdi22 20406	Expand the product of two sums in a ring. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) · (𝑍 + 𝑇)) = (((𝑋 · 𝑍) + (𝑌 · 𝑍)) + ((𝑋 · 𝑇) + (𝑌 · 𝑇))))
Theorem	ringidcl 20407	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 20408	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 20409	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 20410	Lemma for ringlidm 20411 and ringridm 20412. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋))
Theorem	ringlidm 20411	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 20412	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 20413*	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 20414	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 20415	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 20416*	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 20417	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 20350 for rings. (Revised by AV, 5-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵) → (𝐴 + 𝐴) = (( 1 + 1 ) · 𝐴))
Theorem	ringadd2 20418*	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 20419	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 20420	Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	ringcomlem 20421	Lemma for ringcom 20422. This (formerly) part of the proof for ringcom 20422 is also applicable for semirings (without using the commutativity of the addition given per definition of a semiring), see srgcom4lem 20353. (Contributed by Gérard Lang, 4-Dec-2014.) Variant of rglcom4d 20351 for rings. (Revised by AV, 5-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑋) + (𝑌 + 𝑌)) = ((𝑋 + 𝑌) + (𝑋 + 𝑌)))
Theorem	ringcom 20422	Commutativity of the additive group of a ring. (See also lmodcom 21093.) 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 20423	A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel)
Theorem	ringcmn 20424	A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
Theorem	ringabld 20425	A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Abel)
Theorem	ringcmnd 20426	A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CMnd)
Theorem	ringrng 20427	A unital ring is a non-unital ring. (Contributed by AV, 6-Jan-2020.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng)
Theorem	ringssrng 20428	The unital rings are non-unital rings. (Contributed by AV, 20-Mar-2020.)
⊢ Ring ⊆ Rng
Theorem	isringrng 20429*	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	dfring2 20430*	The predicate "is a unital ring" based on a ring being abelian. Definition of "ring with unit" in [Lang] p. 83. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by AV, 8-Aug-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
Theorem	ringpropd 20431*	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 20432*	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 20433	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 20434*	Properties that determine a ring. (Contributed by NM, 2-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    &   ⊢ (𝜑 → 1 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	iscrngd 20435*	Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    &   ⊢ (𝜑 → 1 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) = (𝑦 · 𝑥))    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	ringlz 20436	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 20437	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 20438	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 20439	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 20440	Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing)
Theorem	ring1eq0 20441	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 20442	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 20443*	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 20444*	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 20445	Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 38678 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘ 1 ) · 𝑋) = (𝑁‘𝑋))
Theorem	ringnegr 20446	Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 38679 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑁‘ 1 )) = (𝑁‘𝑋))
Theorem	ringmneg1 20447	Negation of a product in a ring. (mulneg1 11677 analog.) Compared with rngmneg1 20303, 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 20448	Negation of a product in a ring. (mulneg2 11678 analog.) Compared with rngmneg2 20304, 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 20449	Double negation of a product in a ring. (mul2neg 11680 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌))
Theorem	ringsubdi 20450	Ring multiplication distributes over subtraction. (subdi 11674 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍)))
Theorem	ringsubdir 20451	Ring multiplication distributes over subtraction. (subdir 11675 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍)))
Theorem	mulgass2 20452	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))
Theorem	ring1 20453	The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Ring)
Theorem	ringn0 20454	Rings exist. (Contributed by AV, 29-Apr-2019.)
⊢ Ring ≠ ∅
Theorem	ringlghm 20455*	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 20456*	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	gsummulc1 20457*	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 20458*	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 20459*	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 20460*	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 20461	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 20462	A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Ring)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Ring)
Theorem	prdscrngd 20463	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 20464	Value of the ring unity in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Ring)    ⇒   ⊢ (𝜑 → (1r ∘ 𝑅) = (1r‘𝑌))
Theorem	pwsring 20465	A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Ring)
Theorem	pws1 20466	Value of the ring unity in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 1 }) = (1r‘𝑌))
Theorem	pwscrng 20467	A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CRing)
Theorem	pwsmgp 20468	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 20469*	The projection given by pwspjmhm 18940 is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑇 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑀 MndHom 𝑇))
Theorem	pwsexpg 20470	Value of a group exponentiation in a structure power. Compare pwsmulg 19243. (Contributed by SN, 30-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑇 = (mulGrp‘𝑅)    &   ⊢ ∙ = (.g‘𝑀)    &   ⊢ · = (.g‘𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝑁 ∙ 𝑋)‘𝐴) = (𝑁 · (𝑋‘𝐴)))
Theorem	pwsgprod 20471*	Finite products in a power structure are taken componentwise. Compare pwsgsum 20110. (Contributed by SN, 30-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑇 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 )    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))))
Theorem	imasring 20472*	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 20473	The image of a ring under an injection is a ring (imasmndf1 18885 analog). (Contributed by AV, 27-Feb-2025.)
⊢ 𝑈 = (𝐹 “s 𝑅)    &   ⊢ 𝑉 = (Base‘𝑅)    ⇒   ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Ring) → 𝑈 ∈ Ring)
Theorem	xpsringd 20474	A product of two rings is a ring (xpsmnd 18886 analog). (Contributed by AV, 28-Feb-2025.)
⊢ 𝑌 = (𝑆 ×s 𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Ring)
Theorem	xpsring1d 20475	The multiplicative identity element of a binary product of rings. (Contributed by AV, 16-Mar-2025.)
⊢ 𝑌 = (𝑆 ×s 𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (1r‘𝑌) = ⟨(1r‘𝑆), (1r‘𝑅)⟩)
Theorem	qusring2 20476*	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 20477*	The binomial theorem for commutative rings (special case of csrgbinom 20372): (𝐴 + 𝐵)↑𝑁 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𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))
10.3.6  Opposite ring
Syntax	coppr 20478	The opposite ring operation.
class oppr
Definition	df-oppr 20479	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 20480	Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ 𝑂 = (𝑅 sSet ⟨(.r‘ndx), tpos · ⟩)
Theorem	opprmulfval 20481	Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (.r‘𝑂)    ⇒   ⊢ ∙ = tpos ·
Theorem	opprmul 20482	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 20483	In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 20559). (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (.r‘𝑂)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∙ 𝑌))
Theorem	opprlem 20484	Lemma for opprbas 20485 and oppradd 20486. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (.r‘ndx)    ⇒   ⊢ (𝐸‘𝑅) = (𝐸‘𝑂)
Theorem	opprbas 20485	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 20486	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 20487	An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝑂 ∈ Rng)
Theorem	opprrngb 20488	A class is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 20487. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng ↔ 𝑂 ∈ Rng)
Theorem	opprring 20489	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 20490	Bidirectional form of opprring 20489. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring ↔ 𝑂 ∈ Ring)
Theorem	oppr0 20491	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ 0 = (0g‘𝑂)
Theorem	oppr1 20492	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ 1 = (1r‘𝑂)
Theorem	opprneg 20493	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 20494	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (SubGrp‘𝑅) = (SubGrp‘𝑂)
Theorem	mulgass3 20495	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁 · 𝑌)) = (𝑁 · (𝑋 × 𝑌)))
10.3.7  Divisibility
Syntax	cdsr 20496	Ring divisibility relation.
class ∥r
Syntax	cui 20497	Units in a ring.
class Unit
Syntax	cir 20498	Ring irreducibles.
class Irred
Definition	df-dvdsr 20499*	Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through (∥r‘(oppr‘𝑅)). (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ ∥r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑤) ∧ ∃𝑧 ∈ (Base‘𝑤)(𝑧(.r‘𝑤)𝑥) = 𝑦)})
Definition	df-unit 20500	Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ Unit = (𝑤 ∈ V ↦ (◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤))) “ {(1r‘𝑤)}))