P. 145 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14401-14500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ringcl 14401	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 14402	A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑌 · 𝑋))
Theorem	iscrng2 14403*	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 14404	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 14405*	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	ringcld 14406	Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	ringdi 14407	Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)))
Theorem	ringdir 14408	Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Theorem	ringidcl 14409	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	ring0cl 14410	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 14411	Lemma for ringlidm 14412 and ringridm 14413. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋))
Theorem	ringlidm 14412	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 14413	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 14414*	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	ringid 14415*	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	ringadd2 14416*	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.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ∃𝑥 ∈ 𝐵 (𝑋 + 𝑋) = ((𝑥 + 𝑥) · 𝑋))
Theorem	ringo2times 14417	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.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵) → (𝐴 + 𝐴) = (( 1 + 1 ) · 𝐴))
Theorem	ringidss 14418	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 14419	Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	ringcom 14420	Commutativity of the additive group of a ring. (Contributed by Gérard Lang, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	ringabl 14421	A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel)
Theorem	ringcmn 14422	A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
Theorem	ringabld 14423	A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Abel)
Theorem	ringcmnd 14424	A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CMnd)
Theorem	ringrng 14425	A unital ring is a non-unital ring. (Contributed by AV, 6-Jan-2020.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng)
Theorem	ringssrng 14426	The unital rings are non-unital rings. (Contributed by AV, 20-Mar-2020.)
⊢ Ring ⊆ Rng
Theorem	ringpropd 14427*	If two structures have the same group components (properties), 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 14428*	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 14429	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 14430*	Properties that determine a ring. (Contributed by NM, 2-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    &   ⊢ (𝜑 → 1 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	iscrngd 14431*	Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    &   ⊢ (𝜑 → 1 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) = (𝑦 · 𝑥))    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	ringlz 14432	The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 )
Theorem	ringrz 14433	The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 )
Theorem	ringlzd 14434	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 14435	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 14436	Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing)
Theorem	ring1eq0 14437	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	ringinvnz1ne0 14438*	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 14439*	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 14440	Negation in a ring is the same as left multiplication by -1. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘ 1 ) · 𝑋) = (𝑁‘𝑋))
Theorem	ringnegr 14441	Negation in a ring is the same as right multiplication by -1. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑁‘ 1 )) = (𝑁‘𝑋))
Theorem	ringmneg1 14442	Negation of a product in a ring. (mulneg1 8724 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) · 𝑌) = (𝑁‘(𝑋 · 𝑌)))
Theorem	ringmneg2 14443	Negation of a product in a ring. (mulneg2 8725 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑁‘𝑌)) = (𝑁‘(𝑋 · 𝑌)))
Theorem	ringm2neg 14444	Double negation of a product in a ring. (mul2neg 8727 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌))
Theorem	ringsubdi 14445	Ring multiplication distributes over subtraction. (subdi 8714 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍)))
Theorem	ringsubdir 14446	Ring multiplication distributes over subtraction. (subdir 8715 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍)))
Theorem	mulgass2 14447	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))
Theorem	ring1 14448	The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Ring)
Theorem	ringn0 14449	The class of rings is not empty (it is also inhabited, as shown at ring1 14448). (Contributed by AV, 29-Apr-2019.)
⊢ Ring ≠ ∅
Theorem	ringlghm 14450*	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 14451*	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	ringressid 14452	A ring restricted to its base set is a ring. It will usually be the original ring exactly, of course, but to show that needs additional conditions such as those in strressid 13478. (Contributed by Jim Kingdon, 28-Feb-2025.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Ring → (𝐺 ↾s 𝐵) ∈ Ring)
Theorem	imasring 14453*	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 14454	The image of a ring under an injection is a ring. (Contributed by AV, 27-Feb-2025.)
⊢ 𝑈 = (𝐹 “s 𝑅)    &   ⊢ 𝑉 = (Base‘𝑅)    ⇒   ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Ring) → 𝑈 ∈ Ring)
Theorem	qusring2 14455*	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‘𝑈)))
7.3.6  Opposite ring
Syntax	coppr 14456	The opposite ring operation.
class oppr
Definition	df-oppr 14457	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	opprvalg 14458	Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑂 = (𝑅 sSet ⟨(.r‘ndx), tpos · ⟩))
Theorem	opprmulfvalg 14459	Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (.r‘𝑂)    ⇒   ⊢ (𝑅 ∈ 𝑉 → ∙ = tpos · )
Theorem	opprmulg 14460	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 14461	In a commutative ring, the opposite ring is equivalent to the original ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (.r‘𝑂)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∙ 𝑌))
Theorem	opprex 14462	Existence of the opposite ring. If you know that 𝑅 is a ring, see opprring 14468. (Contributed by Jim Kingdon, 10-Jan-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑂 ∈ V)
Theorem	opprsllem 14463	Lemma for opprbasg 14464 and oppraddg 14465. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝐸‘ndx) ≠ (.r‘ndx)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝐸‘𝑅) = (𝐸‘𝑂))
Theorem	opprbasg 14464	Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐵 = (Base‘𝑂))
Theorem	oppraddg 14465	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 14466	An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝑂 ∈ Rng)
Theorem	opprrngbg 14467	A set is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 14466. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rng ↔ 𝑂 ∈ Rng))
Theorem	opprring 14468	An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring)
Theorem	opprringbg 14469	Bidirectional form of opprring 14468. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Ring ↔ 𝑂 ∈ Ring))
Theorem	opprringb 14470	Bidirectional form of opprring 14468. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring ↔ 𝑂 ∈ Ring)
Theorem	oppr0g 14471	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 0 = (0g‘𝑂))
Theorem	oppr1g 14472	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 1 = (1r‘𝑂))
Theorem	opprnegg 14473	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	opprsubgg 14474	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (SubGrp‘𝑅) = (SubGrp‘𝑂))
Theorem	mulgass3 14475	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁 · 𝑌)) = (𝑁 · (𝑋 × 𝑌)))
7.3.7  Divisibility
Syntax	cdsr 14476	Ring divisibility relation.
class ∥r
Syntax	cui 14477	Units in a ring.
class Unit
Syntax	cir 14478	Ring irreducibles.
class Irred
Definition	df-dvdsr 14479*	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 14480	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‘𝑤)}))
Definition	df-irred 14481*	Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧})
Theorem	reldvdsr 14482	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ Rel ∥
Theorem	reldvdsrsrg 14483	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
⊢ (𝑅 ∈ SRing → Rel (∥r‘𝑅))
Theorem	dvdsrvald 14484*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → · = (.r‘𝑅))    ⇒   ⊢ (𝜑 → ∥ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)})
Theorem	dvdsrd 14485*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → · = (.r‘𝑅))    ⇒   ⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)))
Theorem	dvdsr2d 14486*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))
Theorem	dvdsrmuld 14487	A left-multiple of 𝑋 is divisible by 𝑋. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∥ (𝑌 · 𝑋))
Theorem	dvdsrcld 14488	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝑋 ∥ 𝑌)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	dvdsrex 14489	Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.)
⊢ (𝑅 ∈ SRing → (∥r‘𝑅) ∈ V)
Theorem	dvdsrcl2 14490	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∥ 𝑌) → 𝑌 ∈ 𝐵)
Theorem	dvdsrid 14491	An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ 𝑋)
Theorem	dvdsrtr 14492	Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋) → 𝑌 ∥ 𝑋)
Theorem	dvdsrmul1 14493	The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∥ 𝑌) → (𝑋 · 𝑍) ∥ (𝑌 · 𝑍))
Theorem	dvdsrneg 14494	An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ (𝑁‘𝑋))
Theorem	dvdsr01 14495	In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning.) (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ 0 )
Theorem	dvdsr02 14496	Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 ∥ 𝑋 ↔ 𝑋 = 0 ))
Theorem	isunitd 14497	Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.)
⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 1 = (1r‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑆 = (oppr‘𝑅))    &   ⊢ (𝜑 → 𝐸 = (∥r‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )))
Theorem	1unit 14498	The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 1 ∈ 𝑈)
Theorem	unitcld 14499	A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	unitssd 14500	The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    ⇒   ⊢ (𝜑 → 𝑈 ⊆ 𝐵)