P. 204 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20301-20400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	srgpcomp 20301	If two elements of a semiring commute, they also commute if one of the elements is raised to a higher power. (Contributed by AV, 23-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    ⇒   ⊢ (𝜑 → ((𝐾 ↑ 𝐵) × 𝐴) = (𝐴 × (𝐾 ↑ 𝐵)))
Theorem	srgpcompp 20302	If two elements of a semiring commute, they also commute if the elements are raised to a higher power. (Contributed by AV, 23-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((𝑁 ↑ 𝐴) × (𝐾 ↑ 𝐵)) × 𝐴) = (((𝑁 + 1) ↑ 𝐴) × (𝐾 ↑ 𝐵)))
Theorem	srgpcomppsc 20303	If two elements of a semiring commute, they also commute if the elements are raised to a higher power and a scalar multiplication is involved. (Contributed by AV, 23-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ · = (.g‘𝑅)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐶 · ((𝑁 ↑ 𝐴) × (𝐾 ↑ 𝐵))) × 𝐴) = (𝐶 · (((𝑁 + 1) ↑ 𝐴) × (𝐾 ↑ 𝐵))))
Theorem	srglmhm 20304*	Left-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringlghm 20396. (Contributed by AV, 23-Aug-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 MndHom 𝑅))
Theorem	srgrmhm 20305*	Right-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringrghm 20397. (Contributed by AV, 23-Aug-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) ∈ (𝑅 MndHom 𝑅))
Theorem	srgsummulcr 20306*	A finite semiring sum multiplied by a constant, analogous to gsummulc1 20398. (Contributed by AV, 23-Aug-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌))
Theorem	sgsummulcl 20307*	A finite semiring sum multiplied by a constant, analogous to gsummulc2 20399. (Contributed by AV, 23-Aug-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑌 · 𝑋))) = (𝑌 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋))))
Theorem	srg1expzeq1 20308	The exponentiation (by a nonnegative integer) of the multiplicative identity of a semiring, analogous to mulgnn0z 19168. (Contributed by AV, 25-Nov-2019.)
⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0) → (𝑁 · 1 ) = 1 )
10.3.4.1  The binomial theorem for semirings In this section, we prove the binomial theorem for semirings, srgbinom 20314, which is a generalization of the binomial theorem for complex numbers, binom 15886: (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)). Note that the binomial theorem also holds in the non-unital case (that is, in a "rg") and actually, the additive identity is not needed in its proof either. Therefore, it can be proven in even more general cases. An example is the "rg" (resp. "rg without a zero") of integrable nonnegative (resp. positive) functions on ℝ. Special cases of the binomial theorem are csrgbinom 20315 (binomial theorem for commutative semirings) and crngbinom 20418 (binomial theorem for commutative rings).
Theorem	srgbinomlem1 20309	Lemma 1 for srgbinomlem 20313. (Contributed by AV, 23-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ (𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0)) → ((𝐷 ↑ 𝐴) × (𝐸 ↑ 𝐵)) ∈ 𝑆)
Theorem	srgbinomlem2 20310	Lemma 2 for srgbinomlem 20313. (Contributed by AV, 23-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0)) → (𝐶 · ((𝐷 ↑ 𝐴) × (𝐸 ↑ 𝐵))) ∈ 𝑆)
Theorem	srgbinomlem3 20311*	Lemma 3 for srgbinomlem 20313. (Contributed by AV, 23-Aug-2019.) (Proof shortened by AV, 27-Oct-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))
Theorem	srgbinomlem4 20312*	Lemma 4 for srgbinomlem 20313. (Contributed by AV, 24-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))
Theorem	srgbinomlem 20313*	Lemma for srgbinom 20314. Inductive step, analogous to binomlem 15885. (Contributed by AV, 24-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 + 1) ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))
Theorem	srgbinom 20314*	The binomial theorem for commuting elements of a semiring: (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)) (generalization of binom 15886). (Contributed by AV, 24-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    ⇒   ⊢ (((𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))
Theorem	csrgbinom 20315*	The binomial theorem for commutative semirings. (Contributed by AV, 24-Aug-2019.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    ⇒   ⊢ (((𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵))))))
10.3.5  Unital rings
Syntax	crg 20316	Extend class notation with class of all (unital) rings.
class Ring
Syntax	ccrg 20317	Extend class notation with class of all (unital) commutative rings.
class CRing
Definition	df-ring 20318*	Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition 1 in [BourbakiAlg1] p. 92 or definition of a ring with identity in part Preliminaries of [Roman] p. 19. So that the additive structure must be abelian (see ringcom 20364), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. Therefore, it can be shown that a unital ring is a non-unital ring (ringrng 20369) only after ringabl 20365 was proven. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ Ring = {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
Definition	df-cring 20319	Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ CRing = {𝑓 ∈ Ring ∣ (mulGrp‘𝑓) ∈ CMnd}
Theorem	isring 20320*	The predicate "is a (unital) ring". Definition of "ring with unit" in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
Theorem	ringgrp 20321	A ring is a group. (Contributed by NM, 15-Sep-2011.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
Theorem	ringmgp 20322	A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
Theorem	iscrng 20323	A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd))
Theorem	crngmgp 20324	A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
Theorem	ringgrpd 20325	A ring is a group. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Grp)
Theorem	ringmnd 20326	A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
Theorem	ringmgm 20327	A ring is a magma. (Contributed by AV, 31-Jan-2020.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mgm)
Theorem	crngring 20328	A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
Theorem	crngringd 20329	A commutative ring is a ring. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	crnggrpd 20330	A commutative ring is a group. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Grp)
Theorem	mgpf 20331	Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ (mulGrp ↾ Ring):Ring⟶Mnd
Theorem	ringdilem 20332	Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))))
Theorem	ringcl 20333	Closure of the multiplication operation of a ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	crngcom 20334	A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑌 · 𝑋))
Theorem	iscrng2 20335*	A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 · 𝑦) = (𝑦 · 𝑥)))
Theorem	ringass 20336	Associative law for multiplication in a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍)))
Theorem	ringideu 20337*	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 20338	Multiplication is commutative in a commutative ring. (Contributed by SN, 8-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑌 · 𝑋))
Theorem	crngbascntr 20339	The base set of a commutative ring is its center. (Contributed by SN, 21-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑍 = (Cntr‘(mulGrp‘𝐺))    ⇒   ⊢ (𝐺 ∈ CRing → 𝐵 = 𝑍)
Theorem	ringassd 20340	Associative law for multiplication in a ring. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍)))
Theorem	crng12d 20341	Commutative/associative law that swaps the first two factors in a triple product in a commutative ring. See also mul12d 11420. (Contributed by SN, 8-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 · 𝑍)) = (𝑌 · (𝑋 · 𝑍)))
Theorem	crng32d 20342	Commutative/associative law that swaps the last two factors in a triple product in a commutative ring. See also mul32d 11421. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) · 𝑍) = ((𝑋 · 𝑍) · 𝑌))
Theorem	ringcld 20343	Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	ringdi 20344	Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)))
Theorem	ringdir 20345	Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Theorem	ringdid 20346	Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)))
Theorem	ringdird 20347	Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Theorem	ringdi22 20348	Expand the product of two sums in a ring. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) · (𝑍 + 𝑇)) = (((𝑋 · 𝑍) + (𝑌 · 𝑍)) + ((𝑋 · 𝑇) + (𝑌 · 𝑇))))
Theorem	ringidcl 20349	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 20350	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 20351	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 20352	Lemma for ringlidm 20353 and ringridm 20354. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋))
Theorem	ringlidm 20353	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 20354	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 20355*	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 20356	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 20357	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 20358*	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 20359	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 20293 for rings. (Revised by AV, 5-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵) → (𝐴 + 𝐴) = (( 1 + 1 ) · 𝐴))
Theorem	ringadd2 20360*	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 20361	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 20362	Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	ringcomlem 20363	Lemma for ringcom 20364. This (formerly) part of the proof for ringcom 20364 is also applicable for semirings (without using the commutativity of the addition given per definition of a semiring), see srgcom4lem 20296. (Contributed by Gérard Lang, 4-Dec-2014.) Variant of rglcom4d 20294 for rings. (Revised by AV, 5-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑋) + (𝑌 + 𝑌)) = ((𝑋 + 𝑌) + (𝑋 + 𝑌)))
Theorem	ringcom 20364	Commutativity of the additive group of a ring. (See also lmodcom 21010.) 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 20365	A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel)
Theorem	ringcmn 20366	A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
Theorem	ringabld 20367	A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Abel)
Theorem	ringcmnd 20368	A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CMnd)
Theorem	ringrng 20369	A unital ring is a non-unital ring. (Contributed by AV, 6-Jan-2020.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng)
Theorem	ringssrng 20370	The unital rings are non-unital rings. (Contributed by AV, 20-Mar-2020.)
⊢ Ring ⊆ Rng
Theorem	isringrng 20371*	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 20372*	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 20373*	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 20374	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 20375*	Properties that determine a ring. (Contributed by NM, 2-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    &   ⊢ (𝜑 → 1 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	iscrngd 20376*	Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    &   ⊢ (𝜑 → 1 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) = (𝑦 · 𝑥))    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	ringlz 20377	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 20378	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 20379	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 20380	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 20381	Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing)
Theorem	ring1eq0 20382	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 20383	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 20384*	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 20385*	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 20386	Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 38573 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘ 1 ) · 𝑋) = (𝑁‘𝑋))
Theorem	ringnegr 20387	Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 38574 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑁‘ 1 )) = (𝑁‘𝑋))
Theorem	ringmneg1 20388	Negation of a product in a ring. (mulneg1 11651 analog.) Compared with rngmneg1 20246, 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 20389	Negation of a product in a ring. (mulneg2 11652 analog.) Compared with rngmneg2 20247, 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 20390	Double negation of a product in a ring. (mul2neg 11654 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌))
Theorem	ringsubdi 20391	Ring multiplication distributes over subtraction. (subdi 11648 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍)))
Theorem	ringsubdir 20392	Ring multiplication distributes over subtraction. (subdir 11649 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍)))
Theorem	mulgass2 20393	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))
Theorem	ring1 20394	The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Ring)
Theorem	ringn0 20395	Rings exist. (Contributed by AV, 29-Apr-2019.)
⊢ Ring ≠ ∅
Theorem	ringlghm 20396*	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 20397*	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 20398*	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 20399*	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 20400*	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 )