P. 138 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13701-13800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opprvalg 13701	Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑂 = (𝑅 sSet ⟨(.r‘ndx), tpos · ⟩))
Theorem	opprmulfvalg 13702	Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (.r‘𝑂)    ⇒   ⊢ (𝑅 ∈ 𝑉 → ∙ = tpos · )
Theorem	opprmulg 13703	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 13704	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 13705	Existence of the opposite ring. If you know that 𝑅 is a ring, see opprring 13711. (Contributed by Jim Kingdon, 10-Jan-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑂 ∈ V)
Theorem	opprsllem 13706	Lemma for opprbasg 13707 and oppraddg 13708. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝐸‘ndx) ≠ (.r‘ndx)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝐸‘𝑅) = (𝐸‘𝑂))
Theorem	opprbasg 13707	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 13708	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 13709	An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝑂 ∈ Rng)
Theorem	opprrngbg 13710	A set is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 13709. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rng ↔ 𝑂 ∈ Rng))
Theorem	opprring 13711	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 13712	Bidirectional form of opprring 13711. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Ring ↔ 𝑂 ∈ Ring))
Theorem	oppr0g 13713	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 0 = (0g‘𝑂))
Theorem	oppr1g 13714	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 1 = (1r‘𝑂))
Theorem	opprnegg 13715	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 13716	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (SubGrp‘𝑅) = (SubGrp‘𝑂))
Theorem	mulgass3 13717	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 13718	Ring divisibility relation.
class ∥r
Syntax	cui 13719	Units in a ring.
class Unit
Syntax	cir 13720	Ring irreducibles.
class Irred
Definition	df-dvdsr 13721*	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 13722	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 13723*	Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧})
Theorem	reldvdsrsrg 13724	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 13725*	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 13726*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → · = (.r‘𝑅))    ⇒   ⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)))
Theorem	dvdsr2d 13727*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))
Theorem	dvdsrmuld 13728	A left-multiple of 𝑋 is divisible by 𝑋. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∥ (𝑌 · 𝑋))
Theorem	dvdsrcld 13729	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → ∥ = (∥r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝑋 ∥ 𝑌)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	dvdsrex 13730	Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.)
⊢ (𝑅 ∈ SRing → (∥r‘𝑅) ∈ V)
Theorem	dvdsrcl2 13731	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∥ 𝑌) → 𝑌 ∈ 𝐵)
Theorem	dvdsrid 13732	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 13733	Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋) → 𝑌 ∥ 𝑋)
Theorem	dvdsrmul1 13734	The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∥ 𝑌) → (𝑋 · 𝑍) ∥ (𝑌 · 𝑍))
Theorem	dvdsrneg 13735	An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∥ (𝑁‘𝑋))
Theorem	dvdsr01 13736	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 13737	Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 0 ∥ 𝑋 ↔ 𝑋 = 0 ))
Theorem	isunitd 13738	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 13739	The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 1 ∈ 𝑈)
Theorem	unitcld 13740	A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	unitssd 13741	The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    ⇒   ⊢ (𝜑 → 𝑈 ⊆ 𝐵)
Theorem	opprunitd 13742	Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝑆 = (oppr‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑈 = (Unit‘𝑆))
Theorem	crngunit 13743	Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∥ 1 ))
Theorem	dvdsunit 13744	A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ∧ 𝑋 ∈ 𝑈) → 𝑌 ∈ 𝑈)
Theorem	unitmulcl 13745	The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝑈)
Theorem	unitmulclb 13746	Reversal of unitmulcl 13745 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) ∈ 𝑈 ↔ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)))
Theorem	unitgrpbasd 13747	The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.)
⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    ⇒   ⊢ (𝜑 → 𝑈 = (Base‘𝐺))
Theorem	unitgrp 13748	The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp)
Theorem	unitabl 13749	The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐺 ∈ Abel)
Theorem	unitgrpid 13750	The identity of the group of units of a ring is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 1 = (0g‘𝐺))
Theorem	unitsubm 13751	The group of units is a submonoid of the multiplicative monoid of the ring. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ∈ (SubMnd‘𝑀))
Syntax	cinvr 13752	Extend class notation with multiplicative inverse.
class invr
Definition	df-invr 13753	Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
⊢ invr = (𝑟 ∈ V ↦ (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟))))
Theorem	invrfvald 13754	Multiplicative inverse function for a ring. (Contributed by NM, 21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈))    &   ⊢ (𝜑 → 𝐼 = (invr‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝐼 = (invg‘𝐺))
Theorem	unitinvcl 13755	The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ 𝑈)
Theorem	unitinvinv 13756	The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘(𝐼‘𝑋)) = 𝑋)
Theorem	ringinvcl 13757	The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ 𝐵)
Theorem	unitlinv 13758	A unit times its inverse is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	unitrinv 13759	A unit times its inverse is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	1rinv 13760	The inverse of the ring unity is the ring unity. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼‘ 1 ) = 1 )
Theorem	0unit 13761	The additive identity is a unit if and only if 1 = 0, i.e. we are in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ 1 = 0 ))
Theorem	unitnegcl 13762	The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈)
Syntax	cdvr 13763	Extend class notation with ring division.
class /r
Definition	df-dvr 13764*	Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦))))
Theorem	dvrfvald 13765*	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof shortened by AV, 2-Mar-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝐼 = (invr‘𝑅))    &   ⊢ (𝜑 → / = (/r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ SRing)    ⇒   ⊢ (𝜑 → / = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))))
Theorem	dvrvald 13766	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝐼 = (invr‘𝑅))    &   ⊢ (𝜑 → / = (/r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 / 𝑌) = (𝑋 · (𝐼‘𝑌)))
Theorem	dvrcl 13767	Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝐵)
Theorem	unitdvcl 13768	The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝑈)
Theorem	dvrid 13769	A ring element divided by itself is the ring unity. (dividap 8745 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 / 𝑋) = 1 )
Theorem	dvr1 13770	A ring element divided by the ring unity is itself. (div1 8747 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 / 1 ) = 𝑋)
Theorem	dvrass 13771	An associative law for division. (divassap 8734 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑌) / 𝑍) = (𝑋 · (𝑌 / 𝑍)))
Theorem	dvrcan1 13772	A cancellation law for division. (divcanap1 8725 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · 𝑌) = 𝑋)
Theorem	dvrcan3 13773	A cancellation law for division. (divcanap3 8742 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 · 𝑌) / 𝑌) = 𝑋)
Theorem	dvreq1 13774	Equality in terms of ratio equal to ring unity. (diveqap1 8749 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) = 1 ↔ 𝑋 = 𝑌))
Theorem	dvrdir 13775	Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 + 𝑌) / 𝑍) = ((𝑋 / 𝑍) + (𝑌 / 𝑍)))
Theorem	rdivmuldivd 13776	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 30-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = ((𝑋 · 𝑍) / (𝑌 · 𝑊)))
Theorem	ringinvdv 13777	Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = ( 1 / 𝑋))
Theorem	rngidpropdg 13778*	The ring unity depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (1r‘𝐾) = (1r‘𝐿))
Theorem	dvdsrpropdg 13779*	The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ SRing)    &   ⊢ (𝜑 → 𝐿 ∈ SRing)    ⇒   ⊢ (𝜑 → (∥r‘𝐾) = (∥r‘𝐿))
Theorem	unitpropdg 13780*	The set of units depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ Ring)    &   ⊢ (𝜑 → 𝐿 ∈ Ring)    ⇒   ⊢ (𝜑 → (Unit‘𝐾) = (Unit‘𝐿))
Theorem	invrpropdg 13781*	The ring inverse function depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ Ring)    &   ⊢ (𝜑 → 𝐿 ∈ Ring)    ⇒   ⊢ (𝜑 → (invr‘𝐾) = (invr‘𝐿))
7.3.8  Ring homomorphisms
Syntax	crh 13782	Extend class notation with the ring homomorphisms.
class RingHom
Syntax	crs 13783	Extend class notation with the ring isomorphisms.
class RingIso
Definition	df-rhm 13784*	Define the set of ring homomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))})
Definition	df-rim 13785*	Define the set of ring isomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)})
Theorem	dfrhm2 13786*	The property of a ring homomorphism can be decomposed into separate homomorphic conditions for addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠))))
Theorem	rhmrcl1 13787	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring)
Theorem	rhmrcl2 13788	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring)
Theorem	rhmex 13789	Set existence for ring homomorphism. (Contributed by Jim Kingdon, 16-May-2025.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝑅 RingHom 𝑆) ∈ V)
Theorem	isrhm 13790	A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) ↔ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ (𝑀 MndHom 𝑁))))
Theorem	rhmmhm 13791	A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑀 MndHom 𝑁))
Theorem	rimrcl 13792	Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V))
Theorem	isrim0 13793	A ring isomorphism is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅)))
Theorem	rhmghm 13794	A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	rhmf 13795	A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶)
Theorem	rhmmul 13796	A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵)))
Theorem	isrhm2d 13797*	Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	isrhmd 13798*	Demonstration of ring homomorphism. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	rhm1 13799	Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘ 1 ) = 𝑁)
Theorem	rhmf1o 13800	A ring homomorphism is bijective iff its converse is also a ring homomorphism. (Contributed by AV, 22-Oct-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 RingHom 𝑅)))