P. 209 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
10.3.13.2  Subrings of unital rings
Syntax	csubrg 20801	Extend class notation with all subrings of a ring.
class SubRing
Definition	df-subrg 20802*	Define a subring of a ring as a set of elements that is a ring in its own right and contains the multiplicative identity. The additional constraint is necessary because the multiplicative identity of a ring, unlike the additive identity of a ring/group or the multiplicative identity of a field, cannot be identified by a local property. Thus, it is possible for a subset of a ring to be a ring while not containing the true identity if it contains a false identity. For instance, the subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity ⟨1, 0⟩ which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ SubRing = (𝑤 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ((𝑤 ↾s 𝑠) ∈ Ring ∧ (1r‘𝑤) ∈ 𝑠)})
Theorem	issubrg 20803	The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))
Theorem	subrgss 20804	A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)
Theorem	subrgid 20805	Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅))
Theorem	subrgring 20806	A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)
Theorem	subrgcrng 20807	A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ CRing)
Theorem	subrgrcl 20808	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
Theorem	subrgsubg 20809	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
Theorem	subrgsubrng 20810	A subring of a unital ring is a subring of a non-unital ring. (Contributed by AV, 30-Mar-2025.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubRng‘𝑅))
Theorem	subrg0 20811	A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 0 = (0g‘𝑆))
Theorem	subrg1cl 20812	A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴)
Theorem	subrgbas 20813	Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	subrg1 20814	A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 = (1r‘𝑆))
Theorem	subrgacl 20815	A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴)
Theorem	subrgmcl 20816	A subring is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.)
⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴)
Theorem	subrgsubm 20817	A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubMnd‘𝑀))
Theorem	subrgdvds 20818	If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 𝐸 = (∥r‘𝑆)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 ⊆ ∥ )
Theorem	subrguss 20819	A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑉 = (Unit‘𝑆)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ⊆ 𝑈)
Theorem	subrginv 20820	A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝐽 = (invr‘𝑆)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋))
Theorem	subrgdv 20821	A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝐸 = (/r‘𝑆)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋𝐸𝑌))
Theorem	subrgunit 20822	An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑉 = (Unit‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ (𝐼‘𝑋) ∈ 𝐴)))
Theorem	subrgugrp 20823	The units of a subring form a subgroup of the unit group of the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑉 = (Unit‘𝑆)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ∈ (SubGrp‘𝐺))
Theorem	issubrg2 20824*	Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)))
Theorem	opprsubrg 20825	Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (SubRing‘𝑅) = (SubRing‘𝑂)
Theorem	subrgnzr 20826	A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing)
Theorem	subrgint 20827	The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubRing‘𝑅))
Theorem	subrgin 20828	The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRing‘𝑅))
Theorem	subrgmre 20829	The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (Moore‘𝐵))
Theorem	subsubrg 20830	A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	subsubrg2 20831	The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (SubRing‘𝑆) = ((SubRing‘𝑅) ∩ 𝒫 𝐴))
Theorem	issubrg3 20832	A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ 𝑆 ∈ (SubMnd‘𝑀))))
Theorem	resrhm 20833	Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝑋 ∈ (SubRing‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 RingHom 𝑇))
Theorem	resrhm2b 20834	Restriction of the codomain of a (ring) homomorphism. resghm2b 19428 analog. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubRing‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 RingHom 𝑇) ↔ 𝐹 ∈ (𝑆 RingHom 𝑈)))
Theorem	rhmeql 20835	The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝐺 ∈ (𝑆 RingHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubRing‘𝑆))
Theorem	rhmima 20836	The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRing‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubRing‘𝑁))
Theorem	rnrhmsubrg 20837	The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.)
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ (SubRing‘𝑁))
Theorem	cntzsubr 20838	Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅))
Theorem	pwsdiagrhm 20839*	Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 RingHom 𝑌))
Theorem	subrgpropd 20840*	If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (SubRing‘𝐾) = (SubRing‘𝐿))
Theorem	rhmpropd 20841*	Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐽))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐽)𝑦) = (𝑥(.r‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝑀)𝑦))    ⇒   ⊢ (𝜑 → (𝐽 RingHom 𝐾) = (𝐿 RingHom 𝑀))
10.3.13.3  Subrings generated by a subset
Syntax	crgspn 20842	Extend class notation with span of a set of elements over a ring.
class RingSpan
Definition	df-rgspn 20843*	The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
Theorem	rgspnval 20844*	Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    ⇒   ⊢ (𝜑 → 𝑈 = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
Theorem	rgspncl 20845	The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑅))
Theorem	rgspnssid 20846	The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
Theorem	rgspnmin 20847	The ring-span is contained in all subrings which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝑈 ⊆ 𝑆)
10.3.14  Categories of rings
10.3.14.1  The category of non-unital rings The "category of non-unital rings" RngCat is the category of all non-unital rings Rng in a universe and non-unital ring homomorphisms RngHom between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to non-unital rings and the morphisms to the non-unital ring homomorphisms, while the composition of morphisms is preserved, see df-rngc 20849. Alternately, the category of non-unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see dfrngc2 20860. Since we consider only "small categories" (i.e. categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are a subset of the non-unital rings (relativized to a subset or "universe" 𝑢) (𝑢 ∩ Rng), see rngcbas 20853, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHom ↾ (𝐵 × 𝐵)), see rngchomfval 20854, whereas the composition is the ordinary composition of functions, see rngccofval 20858 and rngcco 20859. By showing that the non-unital ring homomorphisms between non-unital rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rnghmsscmap 20862, it can be shown that the non-unital ring homomorphisms between non-unital rings are a subcategory (Subcat) of the category of extensible structures, see rnghmsubcsetc 20865. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 20866 with the identity function as identity arrow, see rngcid 20867.
Syntax	crngc 20848	Extend class notation to include the category Rng.
class RngCat
Definition	df-rngc 20849	Definition of the category Rng, relativized to a subset 𝑢. This is the category of all non-unital rings in 𝑢 and homomorphisms between these rings. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ RngCat = (𝑢 ∈ V ↦ ((ExtStrCat‘𝑢) ↾cat ( RngHom ↾ ((𝑢 ∩ Rng) × (𝑢 ∩ Rng)))))
Theorem	rngcval 20850	Value of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐶 = ((ExtStrCat‘𝑈) ↾cat 𝐻))
Theorem	rnghmresfn 20851	The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020.)
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝐵 × 𝐵))
Theorem	rnghmresel 20852	An element of the non-unital ring homomorphisms restricted to a subset of non-unital rings is a non-unital ring homomorphisms. (Contributed by AV, 9-Mar-2020.)
⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐹 ∈ (𝑋𝐻𝑌)) → 𝐹 ∈ (𝑋 RngHom 𝑌))
Theorem	rngcbas 20853	Set of objects of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))
Theorem	rngchomfval 20854	Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))
Theorem	rngchom 20855	Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RngHom 𝑌))
Theorem	elrngchom 20856	A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	rngchomfeqhom 20857	The functionalized Hom-set operation equals the Hom-set operation in the category of non-unital rings (in a universe). (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = (Hom ‘𝐶))
Theorem	rngccofval 20858	Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈)))
Theorem	rngcco 20859	Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))    &   ⊢ (𝜑 → 𝐺:(Base‘𝑌)⟶(Base‘𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	dfrngc2 20860	Alternate definition of the category of non-unital rings (in a universe). (Contributed by AV, 16-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈)))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	rnghmsscmap2 20861*	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of non-unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Rng ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RngHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
Theorem	rnghmsscmap 20862*	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of extensible structures (in the same universe). (Contributed by AV, 9-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Rng ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RngHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
Theorem	rnghmsubcsetclem1 20863	Lemma 1 for rnghmsubcsetc 20865. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rnghmsubcsetclem2 20864*	Lemma 2 for rnghmsubcsetc 20865. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rnghmsubcsetc 20865	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶))
Theorem	rngccat 20866	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 9-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	rngcid 20867	The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 10-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑆 = (Base‘𝑋)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑆))
Theorem	rngcsect 20868	A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Base‘𝑋)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngHom 𝑌) ∧ 𝐺 ∈ (𝑌 RngHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))))
Theorem	rngcinv 20869	An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngIso 𝑌) ∧ 𝐺 = ◡𝐹)))
Theorem	rngciso 20870	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIso 𝑌)))
Theorem	rngcifuestrc 20871*	The "inclusion functor" from the category of non-unital rings into the category of extensible structures. (Contributed by AV, 30-Mar-2020.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 = ( I ↾ 𝐵))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝐸)𝐺)
Theorem	funcrngcsetc 20872*	The "natural forgetful functor" from the category of non-unital rings into the category of sets which sends each non-unital ring to its underlying set (base set) and the morphisms (non-unital ring homomorphisms) to mappings of the corresponding base sets. An alternate proof is provided in funcrngcsetcALT 20873, using cofuval2 18042 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 20871, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18303. (Contributed by AV, 26-Mar-2020.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	funcrngcsetcALT 20873*	Alternate proof of funcrngcsetc 20872, using cofuval2 18042 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 20871, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18303. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 20872. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	zrinitorngc 20874	The zero ring is an initial object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (InitO‘𝐶))
Theorem	zrtermorngc 20875	The zero ring is a terminal object in the category of non-unital rings. (Contributed by AV, 17-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (TermO‘𝐶))
Theorem	zrzeroorngc 20876	The zero ring is a zero object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (ZeroO‘𝐶))
10.3.14.2  The category of (unital) rings The "category of unital rings" RingCat is the category of all (unital) rings Ring in a universe and (unital) ring homomorphisms RingHom between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to (unital) rings and the morphisms to the (unital) ring homomorphisms, while the composition of morphisms is preserved, see df-ringc 20878. Alternately, the category of unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see dfringc2 20889. In the following, we omit the predicate "unital", so that "ring" and "ring homomorphism" (without predicate) always mean "unital ring" and "unital ring homomorphism". Since we consider only "small categories" (i.e., categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are a subset of the rings (relativized to a subset or "universe" 𝑢) (𝑢 ∩ Ring), see ringcbas 20882, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom ↾ (𝐵 × 𝐵)), see ringchomfval 20883, whereas the composition is the ordinary composition of functions, see ringccofval 20887 and ringcco 20888. By showing that the ring homomorphisms between rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rhmsscmap 20891, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 20894. It follows that the category of rings RingCat is actually a category, see ringccat 20895 with the identity function as identity arrow, see ringcid 20896. Furthermore, it is shown that the ring homomorphisms between rings are a subcategory subset of the non-unital ring homomorphisms between non-unital rings, see rhmsscrnghm 20897, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 20900. By this, the restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings, see rngcresringcat 20901: ((RngCat‘𝑈) ↾cat ( RingHom ↾ (𝐵 × 𝐵))) = (RingCat‘𝑈)). Finally, it is shown that the "natural forgetful functor" from the category of rings into the category of sets is the function which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets, see funcringcsetc 20906.
Syntax	cringc 20877	Extend class notation to include the category Ring.
class RingCat
Definition	df-ringc 20878	Definition of the category Ring, relativized to a subset 𝑢. See also the note in [Lang] p. 91, and the item Rng in [Adamek] p. 478. This is the category of all unital rings in 𝑢 and homomorphisms between these rings. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ RingCat = (𝑢 ∈ V ↦ ((ExtStrCat‘𝑢) ↾cat ( RingHom ↾ ((𝑢 ∩ Ring) × (𝑢 ∩ Ring)))))
Theorem	ringcval 20879	Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐶 = ((ExtStrCat‘𝑈) ↾cat 𝐻))
Theorem	rhmresfn 20880	The class of unital ring homomorphisms restricted to subsets of unital rings is a function. (Contributed by AV, 10-Mar-2020.)
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝐵 × 𝐵))
Theorem	rhmresel 20881	An element of the unital ring homomorphisms restricted to a subset of unital rings is a unital ring homomorphism. (Contributed by AV, 10-Mar-2020.)
⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐹 ∈ (𝑋𝐻𝑌)) → 𝐹 ∈ (𝑋 RingHom 𝑌))
Theorem	ringcbas 20882	Set of objects of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))
Theorem	ringchomfval 20883	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))
Theorem	ringchom 20884	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	elringchom 20885	A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	ringchomfeqhom 20886	The functionalized Hom-set operation equals the Hom-set operation in the category of unital rings (in a universe). (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = (Hom ‘𝐶))
Theorem	ringccofval 20887	Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈)))
Theorem	ringcco 20888	Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))    &   ⊢ (𝜑 → 𝐺:(Base‘𝑌)⟶(Base‘𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	dfringc2 20889	Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈)))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	rhmsscmap2 20890*	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the mappings between base sets of unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
Theorem	rhmsscmap 20891*	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the mappings between base sets of extensible structures (in the same universe). (Contributed by AV, 9-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
Theorem	rhmsubcsetclem1 20892	Lemma 1 for rhmsubcsetc 20894. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcsetclem2 20893*	Lemma 2 for rhmsubcsetc 20894. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcsetc 20894	The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶))
Theorem	ringccat 20895	The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	ringcid 20896	The identity arrow in the category of unital rings is the identity function. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 10-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑆 = (Base‘𝑋)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑆))
Theorem	rhmsscrnghm 20897	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the non-unital ring homomorphisms between non-unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝑆 = (Rng ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat ( RngHom ↾ (𝑆 × 𝑆)))
Theorem	rhmsubcrngclem1 20898	Lemma 1 for rhmsubcrngc 20900. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcrngclem2 20899*	Lemma 2 for rhmsubcrngc 20900. (Contributed by AV, 12-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcrngc 20900	The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of non-unital rings. (Contributed by AV, 12-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶))