P. 207 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20601-20700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvrcan1 20601	A cancellation law for division. (divcan1 11953 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · 𝑌) = 𝑋)
Theorem	dvrcan3 20602	A cancellation law for division. (divcan3 11970 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 · 𝑌) / 𝑌) = 𝑋)
Theorem	dvreq1 20603	Equality in terms of ratio equal to ring unity. (diveq1 11973 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) = 1 ↔ 𝑋 = 𝑌))
Theorem	dvrdir 20604	Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 + 𝑌) / 𝑍) = ((𝑋 / 𝑍) + (𝑌 / 𝑍)))
Theorem	rdivmuldivd 20605	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 20606	Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = ( 1 / 𝑋))
Theorem	rngidpropd 20607*	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	dvdsrpropd 20608*	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‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (∥r‘𝐾) = (∥r‘𝐿))
Theorem	unitpropd 20609*	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‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (Unit‘𝐾) = (Unit‘𝐿))
Theorem	invrpropd 20610*	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‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (invr‘𝐾) = (invr‘𝐿))
Theorem	isirred 20611*	An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑁 = (𝐵 ∖ 𝑈)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋))
Theorem	isnirred 20612*	The property of being a non-irreducible (reducible) element in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑁 = (𝐵 ∖ 𝑈)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (¬ 𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝑈 ∨ ∃𝑥 ∈ 𝑁 ∃𝑦 ∈ 𝑁 (𝑥 · 𝑦) = 𝑋)))
Theorem	isirred2 20613*	Expand out the class difference from isirred 20611. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑋 → (𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈))))
Theorem	opprirred 20614	Irreducibility is symmetric, so the irreducible elements of the opposite ring are the same as the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (oppr‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    ⇒   ⊢ 𝐼 = (Irred‘𝑆)
Theorem	irredn0 20615	The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 0 )
Theorem	irredcl 20616	An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ 𝐵)
Theorem	irrednu 20617	An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐼 → ¬ 𝑋 ∈ 𝑈)
Theorem	irredn1 20618	The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 1 )
Theorem	irredrmul 20619	The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	irredlmul 20620	The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼) → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	irredmul 20621	If product of two elements is irreducible, then one of the elements must be a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 · 𝑌) ∈ 𝐼) → (𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈))
Theorem	irredneg 20622	The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼)
Theorem	irrednegb 20623	An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝐼 ↔ (𝑁‘𝑋) ∈ 𝐼))
10.3.8  Ring primes
Syntax	crpm 20624	Syntax for the ring primes function.
class RPrime
Definition	df-rprm 20625*	Define the function associating with a ring its set of prime elements. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma 16852. Prime elements are closely related to irreducible elements (see df-irred 20551). (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ RPrime = (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))})
10.3.9  Homomorphisms of non-unital rings
Syntax	crnghm 20626	non-unital ring homomorphisms.
class RngHom
Syntax	crngim 20627	non-unital ring isomorphisms.
class RngIso
Definition	df-rnghm 20628*	Define the set of non-unital ring homomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)
⊢ RngHom = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))})
Definition	df-rngim 20629*	Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)
⊢ RngIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RngHom 𝑟)})
Theorem	rnghmrcl 20630	Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → (𝑅 ∈ Rng ∧ 𝑆 ∈ Rng))
Theorem	rnghmfn 20631	The mapping of two non-unital rings to the non-unital ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
⊢ RngHom Fn (Rng × Rng)
Theorem	rnghmval 20632*	The set of the non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 22-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∗ = (.r‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑆)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) → (𝑅 RngHom 𝑆) = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ✚ (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) ∗ (𝑓‘𝑦)))})
Theorem	isrnghm 20633*	A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∗ = (.r‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) ↔ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦)))))
Theorem	isrnghmmul 20634	A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) ↔ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ (𝑀 MgmHom 𝑁))))
Theorem	rnghmmgmhm 20635	A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹 ∈ (𝑀 MgmHom 𝑁))
Theorem	rnghmval2 20636	The non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 1-Mar-2020.)
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) → (𝑅 RngHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MgmHom (mulGrp‘𝑆))))
Theorem	isrngim 20637	An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RngIso 𝑆) ↔ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RngHom 𝑅))))
Theorem	rngimrcl 20638	Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V))
Theorem	rnghmghm 20639	A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	rnghmf 20640	A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹:𝐵⟶𝐶)
Theorem	rnghmmul 20641	A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵)))
Theorem	isrnghm2d 20642*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑆))
Theorem	isrnghmd 20643*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑆))
Theorem	rnghmf1o 20644	A non-unital ring homomorphism is bijective iff its converse is also a non-unital ring homomorphism. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 RngHom 𝑅)))
Theorem	isrngim2 20645	An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RngIso 𝑆) ↔ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶)))
Theorem	rngimf1o 20646	An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	rngimrnghm 20647	An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → 𝐹 ∈ (𝑅 RngHom 𝑆))
Theorem	rngimcnv 20648	The converse of an isomorphism of non-unital rings is an isomorphism of non-unital rings. (Contributed by AV, 27-Feb-2025.)
⊢ (𝐹 ∈ (𝑆 RngIso 𝑇) → ◡𝐹 ∈ (𝑇 RngIso 𝑆))
Theorem	rnghmco 20649	The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑇 RngHom 𝑈) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RngHom 𝑈))
Theorem	idrnghm 20650	The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → ( I ↾ 𝐵) ∈ (𝑅 RngHom 𝑅))
Theorem	c0mgm 20651*	The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MgmHom 𝑇))
Theorem	c0mhm 20652*	The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇))
Theorem	c0ghm 20653*	The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → 𝐻 ∈ (𝑆 GrpHom 𝑇))
Theorem	c0snmgmhm 20654*	The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ (♯‘𝐵) = 1) → 𝐻 ∈ (𝑇 MgmHom 𝑆))
Theorem	c0snmhm 20655*	The constant mapping to zero is a monoid homomorphism from the trivial monoid (consisting of the zero only) to any monoid. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    &   ⊢ 𝑍 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = {𝑍}) → 𝐻 ∈ (𝑇 MndHom 𝑆))
Theorem	c0snghm 20656*	The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    &   ⊢ 𝑍 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = {𝑍}) → 𝐻 ∈ (𝑇 GrpHom 𝑆))
Theorem	rngisomfv1 20657	If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the function value of the ring unity of the unital ring is an element of the base set of the non-unital ring. (Contributed by AV, 27-Feb-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → (𝐹‘ 1 ) ∈ 𝐵)
Theorem	rngisom1 20658*	If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the function value of the ring unity of the unital ring is a ring unity of the non-unital ring. (Contributed by AV, 27-Feb-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → ∀𝑥 ∈ 𝐵 (((𝐹‘ 1 ) · 𝑥) = 𝑥 ∧ (𝑥 · (𝐹‘ 1 )) = 𝑥))
Theorem	rngisomring 20659	If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then both rings are unital. (Contributed by AV, 27-Feb-2025.)
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → 𝑆 ∈ Ring)
Theorem	rngisomring1 20660	If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the ring unity of the second ring is the function value of the ring unity of the first ring for the isomorphism. (Contributed by AV, 16-Mar-2025.)
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → (1r‘𝑆) = (𝐹‘(1r‘𝑅)))
10.3.10  Ring homomorphisms
Syntax	crh 20661	Extend class notation with the ring homomorphisms.
class RingHom
Syntax	crs 20662	Extend class notation with the ring isomorphisms.
class RingIso
Syntax	cric 20663	Extend class notation with the ring isomorphism relation.
class ≃𝑟
Definition	df-rhm 20664*	Define the set of ring homomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))})
Definition	df-rim 20665*	Define the set of ring isomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)})
Theorem	dfrhm2 20666*	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	rhmval0 20667*	The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by AV, 24-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ((𝑓‘ 1 ) = 𝑁 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) × (𝑓‘𝑦))))})
Theorem	isrhm0 20668*	The predicate "is a ring homomorphism from 𝑅 to 𝑆". (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by AV, 24-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝐹 ∈ (𝑅 RingHom 𝑆) ↔ (𝐹:𝐵⟶𝐶 ∧ (𝐹‘ 1 ) = 𝑁 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))))))
Theorem	rhmrcl1 20669	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring)
Theorem	rhmrcl2 20670	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring)
Theorem	isrhm 20671	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 20672	A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑀 MndHom 𝑁))
Theorem	rhmisrnghm 20673	Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 RngHom 𝑆))
Theorem	rimrcl 20674	Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V))
Theorem	isrim0 20675	A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 19441. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅)))
Theorem	rhmghm 20676	A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	rhmf 20677	A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶)
Theorem	rhmcl 20678	Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.) (Revised by AV, 10-Jan-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝐴 ∈ 𝐵) → (𝐹‘𝐴) ∈ 𝐶)
Theorem	rimcnv 20679	The converse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → ◡𝐹 ∈ (𝑆 RingIso 𝑅))
Theorem	rhmadd 20680	Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.) (Revised by AV, 10-Jan-2025.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵)))
Theorem	rhmsub 20681	Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.) (Revised by AV, 10-Jan-2025.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ 𝑁 = (-g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 − 𝐵)) = ((𝐹‘𝐴)𝑁(𝐹‘𝐵)))
Theorem	rhmmul 20682	A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵)))
Theorem	isrhm2d 20683*	Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	isrhmd 20684*	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	rhm0 20685	A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.) (Revised by AV, 23-Jul-2026.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘ 0 ) = 𝑍)
Theorem	rhm1 20686	Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘ 1 ) = 𝑁)
Theorem	idrhm 20687	The identity homomorphism on a ring. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → ( I ↾ 𝐵) ∈ (𝑅 RingHom 𝑅))
Theorem	crngrhmfo 20688	The image of a surjective homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.) (Revised by AV, 19-Jul-2026.)
⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:dom 𝐹–onto→𝐵) → 𝑆 ∈ CRing)
Theorem	rhmf1o 20689	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 𝑅)))
Theorem	isrim 20690	An isomorphism of rings is a bijective homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 12-Jan-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	rimf1o 20691	An isomorphism of rings is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by AV, 22-Oct-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	rimval 20692*	The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by AV, 24-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝑅 RingIso 𝑆) = {𝑓 ∈ (𝑅 RingHom 𝑆) ∣ 𝑓:𝐵–1-1-onto→𝐶}
Theorem	rimrhm 20693	A ring isomorphism is a homomorphism. Compare gimghm 19440. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	rimrcl1 20694	Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑅 ∈ Ring)
Theorem	rimrcl2 20695	Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑆 ∈ Ring)
Theorem	rimgim 20696	An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 GrpIso 𝑆))
Theorem	rimisrngim 20697	Each unital ring isomorphism is a non-unital ring isomorphism. (Contributed by AV, 30-Mar-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RngIso 𝑆))
Theorem	rhmfn 20698	The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
⊢ RingHom Fn (Ring × Ring)
Theorem	rimfn 20699	The mapping of two rings to the ring isomorphisms between them is a function. (Contributed by AV, 24-Jul-2025.)
⊢ RingIso Fn (V × V)
Theorem	rhmval 20700	The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.)
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))