P. 205 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Definition	df-dvr 20401*	Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦))))
Theorem	dvrfval 20402*	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‘𝑅)    ⇒   ⊢ / = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))
Theorem	dvrval 20403	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋 · (𝐼‘𝑌)))
Theorem	dvrcl 20404	Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝐵)
Theorem	unitdvcl 20405	The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) ∈ 𝑈)
Theorem	dvrid 20406	A ring element divided by itself is the ring unity. (divid 11953 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 / 𝑋) = 1 )
Theorem	dvr1 20407	A ring element divided by the ring unity is itself. (div1 11957 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 / 1 ) = 𝑋)
Theorem	dvrass 20408	An associative law for division. (divass 11940 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑌) / 𝑍) = (𝑋 · (𝑌 / 𝑍)))
Theorem	dvrcan1 20409	A cancellation law for division. (divcan1 11931 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · 𝑌) = 𝑋)
Theorem	dvrcan3 20410	A cancellation law for division. (divcan3 11948 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 · 𝑌) / 𝑌) = 𝑋)
Theorem	dvreq1 20411	Equality in terms of ratio equal to ring unity. (diveq1 11952 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) = 1 ↔ 𝑋 = 𝑌))
Theorem	dvrdir 20412	Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 + 𝑌) / 𝑍) = ((𝑋 / 𝑍) + (𝑌 / 𝑍)))
Theorem	rdivmuldivd 20413	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 20414	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 20415*	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 20416*	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 20417*	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 20418*	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 20419*	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 20420*	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 20421*	Expand out the class difference from isirred 20419. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑋 → (𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈))))
Theorem	opprirred 20422	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 20423	The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 0 )
Theorem	irredcl 20424	An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ 𝐵)
Theorem	irrednu 20425	An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐼 → ¬ 𝑋 ∈ 𝑈)
Theorem	irredn1 20426	The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → 𝑋 ≠ 1 )
Theorem	irredrmul 20427	The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	irredlmul 20428	The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼) → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	irredmul 20429	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 20430	The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼)
Theorem	irrednegb 20431	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 20432	Syntax for the ring primes function.
class RPrime
Definition	df-rprm 20433*	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 16750. Prime elements are closely related to irreducible elements (see df-irred 20359). (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ RPrime = (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))})
10.3.9  Homomorphisms of non-unital rings
Syntax	crnghm 20434	non-unital ring homomorphisms.
class RngHom
Syntax	crngim 20435	non-unital ring isomorphisms.
class RngIso
Definition	df-rnghm 20436*	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 20437*	Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)
⊢ RngIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RngHom 𝑟)})
Theorem	rnghmrcl 20438	Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → (𝑅 ∈ Rng ∧ 𝑆 ∈ Rng))
Theorem	rnghmfn 20439	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 20440*	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 20441*	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 20442	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 20443	A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹 ∈ (𝑀 MgmHom 𝑁))
Theorem	rnghmval2 20444	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 20445	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 20446	Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V))
Theorem	rnghmghm 20447	A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	rnghmf 20448	A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHom 𝑆) → 𝐹:𝐵⟶𝐶)
Theorem	rnghmmul 20449	A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵)))
Theorem	isrnghm2d 20450*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑆))
Theorem	isrnghmd 20451*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHom 𝑆))
Theorem	rnghmf1o 20452	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 20453	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 20454	An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	rngimrnghm 20455	An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngIso 𝑆) → 𝐹 ∈ (𝑅 RngHom 𝑆))
Theorem	rngimcnv 20456	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 20457	The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑇 RngHom 𝑈) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RngHom 𝑈))
Theorem	idrnghm 20458	The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → ( I ↾ 𝐵) ∈ (𝑅 RngHom 𝑅))
Theorem	c0mgm 20459*	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 20460*	The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇))
Theorem	c0ghm 20461*	The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → 𝐻 ∈ (𝑆 GrpHom 𝑇))
Theorem	c0snmgmhm 20462*	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 20463*	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 20464*	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 20465	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 20466*	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 20467	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 20468	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 20469	Extend class notation with the ring homomorphisms.
class RingHom
Syntax	crs 20470	Extend class notation with the ring isomorphisms.
class RingIso
Syntax	cric 20471	Extend class notation with the ring isomorphism relation.
class ≃𝑟
Definition	df-rhm 20472*	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 20473*	Define the set of ring isomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)})
Theorem	dfrhm2 20474*	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‘𝑠))))
Definition	df-ric 20475	Define the ring isomorphism relation, analogous to df-gic 19278: Two (unital) rings are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic rings share all global ring properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by AV, 24-Dec-2019.)
⊢ ≃𝑟 = (◡ RingIso “ (V ∖ 1o))
Theorem	rhmrcl1 20476	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring)
Theorem	rhmrcl2 20477	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring)
Theorem	isrhm 20478	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 20479	A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑀 MndHom 𝑁))
Theorem	rhmisrnghm 20480	Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 RngHom 𝑆))
Theorem	isrim0OLD 20481	Obsolete version of isrim0 20483 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅))))
Theorem	rimrcl 20482	Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V))
Theorem	isrim0 20483	A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 19283. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅)))
Theorem	rhmghm 20484	A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	rhmf 20485	A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶)
Theorem	rhmmul 20486	A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵)))
Theorem	isrhm2d 20487*	Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	isrhmd 20488*	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 20489	Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘ 1 ) = 𝑁)
Theorem	idrhm 20490	The identity homomorphism on a ring. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → ( I ↾ 𝐵) ∈ (𝑅 RingHom 𝑅))
Theorem	rhmf1o 20491	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 20492	An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 12-Jan-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	isrimOLD 20493	Obsolete version of isrim 20492 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶)))
Theorem	rimf1o 20494	An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	rimrhmOLD 20495	Obsolete version of rimrhm 20496 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	rimrhm 20496	A ring isomorphism is a homomorphism. Compare gimghm 19282. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	rimgim 20497	An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 GrpIso 𝑆))
Theorem	rimisrngim 20498	Each unital ring isomorphism is a non-unital ring isomorphism. (Contributed by AV, 30-Mar-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RngIso 𝑆))
Theorem	rhmfn 20499	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	rhmval 20500	The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.)
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))