P. 470 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46901-47000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	issgrpALT 46901	The predicate "is a semigroup". (Contributed by AV, 16-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ SGrpALT ↔ (𝑀 ∈ MgmALT ∧ ⚬ assLaw 𝐵))
Theorem	iscsgrpALT 46902	The predicate "is a commutative semigroup". (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ CSGrpALT ↔ (𝑀 ∈ SGrpALT ∧ ⚬ comLaw 𝐵))
Theorem	mgm2mgm 46903	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm)
Theorem	sgrp2sgrp 46904	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ SGrpALT ↔ 𝑀 ∈ Smgrp)
21.45.18  Categories (extension)
21.45.18.1  Subcategories (extension)
Theorem	idfusubc0 46905*	The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.)
⊢ 𝑆 = (𝐶 ↾cat 𝐽)    &   ⊢ 𝐼 = (idfunc‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 = ⟨( I ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥(Hom ‘𝑆)𝑦)))⟩)
Theorem	idfusubc 46906*	The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.)
⊢ 𝑆 = (𝐶 ↾cat 𝐽)    &   ⊢ 𝐼 = (idfunc‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 = ⟨( I ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥𝐽𝑦)))⟩)
Theorem	inclfusubc 46907*	The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ 𝑆 = (𝐶 ↾cat 𝐽)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = ( I ↾ 𝐵))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥𝐽𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑆 Func 𝐶)𝐺)
21.45.19  Rings (extension)
21.45.19.1  Nonzero rings (extension)
Theorem	lmod0rng 46908	If the scalar ring of a module is the zero ring, the module is the zero module, i.e. the base set of the module is the singleton consisting of the identity element only. (Contributed by AV, 17-Apr-2019.)
⊢ ((𝑀 ∈ LMod ∧ ¬ (Scalar‘𝑀) ∈ NzRing) → (Base‘𝑀) = {(0g‘𝑀)})
Theorem	nzrneg1ne0 46909	The additive inverse of the 1 in a nonzero ring is not zero ( -1 =/= 0 ). (Contributed by AV, 29-Apr-2019.)
⊢ (𝑅 ∈ NzRing → ((invg‘𝑅)‘(1r‘𝑅)) ≠ (0g‘𝑅))
Theorem	nrhmzr 46910	There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝑍 ∈ (Ring ∖ NzRing) ∧ 𝑅 ∈ NzRing) → (𝑍 RingHom 𝑅) = ∅)
21.45.19.2  Ideals as non-unital rings
Theorem	lidldomn1 46911*	If a (left) ideal (which is not the zero ideal) of a domain has a multiplicative identity element, the identity element is the identity of the domain. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → 𝐼 = 1 ))
Theorem	lidlabl 46912	A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel)
Theorem	lidlrng 46913	A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) (Proof shortened by AV, 11-Mar-2025.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng)
Theorem	zlidlring 46914	The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Ring)
Theorem	uzlidlring 46915	Only the zero (left) ideal or the unit (left) ideal of a domain is a unital ring. (Contributed by AV, 18-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿) → (𝐼 ∈ Ring ↔ (𝑈 = { 0 } ∨ 𝑈 = 𝐵)))
Theorem	lidldomnnring 46916	A (left) ideal of a domain which is neither the zero ideal nor the unit ideal is not a unital ring. (Contributed by AV, 18-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵)) → 𝐼 ∉ Ring)
21.45.19.3  The non-unital ring of even integers
Theorem	0even 46917*	0 is an even integer. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 0 ∈ 𝐸
Theorem	1neven 46918*	1 is not an even integer. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 1 ∉ 𝐸
Theorem	2even 46919*	2 is an even integer. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 2 ∈ 𝐸
Theorem	2zlidl 46920*	The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑈 = (LIdeal‘ℤring)    ⇒   ⊢ 𝐸 ∈ 𝑈
Theorem	2zrng 46921*	The ring of integers restricted to the even integers is a non-unital ring, the "ring of even integers". Remark: the structure of the complementary subset of the set of integers, the odd integers, is not even a magma, see oddinmgm 46851. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑈 = (LIdeal‘ℤring)    &   ⊢ 𝑅 = (ℤring ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	2zrngbas 46922*	The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝐸 = (Base‘𝑅)
Theorem	2zrngadd 46923*	The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ + = (+g‘𝑅)
Theorem	2zrng0 46924*	The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 0 = (0g‘𝑅)
Theorem	2zrngamgm 46925*	R is an (additive) magma. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Mgm
Theorem	2zrngasgrp 46926*	R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Smgrp
Theorem	2zrngamnd 46927*	R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Mnd
Theorem	2zrngacmnd 46928*	R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ CMnd
Theorem	2zrngagrp 46929*	R is an (additive) group. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Grp
Theorem	2zrngaabl 46930*	R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Abel
Theorem	2zrngmul 46931*	The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ · = (.r‘𝑅)
Theorem	2zrngmmgm 46932*	R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑀 ∈ Mgm
Theorem	2zrngmsgrp 46933*	R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑀 ∈ Smgrp
Theorem	2zrngALT 46934*	The ring of integers restricted to the even integers is a non-unital ring, the "ring of even integers". Alternate version of 2zrng 46921, based on a restriction of the field of the complex numbers. The proof is based on the facts that the ring of even integers is an additive abelian group (see 2zrngaabl 46930) and a multiplicative semigroup (see 2zrngmsgrp 46933). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	2zrngnmlid 46935*	R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑏 ∈ 𝐸 ∃𝑎 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎
Theorem	2zrngnmrid 46936*	R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎
Theorem	2zrngnmlid2 46937*	R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎
Theorem	2zrngnring 46938*	R is not a unital ring. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑅 ∉ Ring
21.45.19.4  A constructed not unital ring
Theorem	cznrnglem 46939	Lemma for cznrng 46941: The base set of the ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is the base set of the ℤ/nℤ structure. (Contributed by AV, 16-Feb-2020.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑋 = (𝑌 sSet ⟨(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)⟩)    ⇒   ⊢ 𝐵 = (Base‘𝑋)
Theorem	cznabel 46940	The ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is an abelian group. (Contributed by AV, 16-Feb-2020.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑋 = (𝑌 sSet ⟨(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)⟩)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵) → 𝑋 ∈ Abel)
Theorem	cznrng 46941*	The ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is a non-unital ring. (Contributed by AV, 17-Feb-2020.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑋 = (𝑌 sSet ⟨(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)⟩)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑋 ∈ Rng)
Theorem	cznnring 46942*	The ring constructed from a ℤ/nℤ structure with 1 < 𝑛 by replacing the (multiplicative) ring operation by a constant operation is not a unital ring. (Contributed by AV, 17-Feb-2020.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑋 = (𝑌 sSet ⟨(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)⟩)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐶 ∈ 𝐵) → 𝑋 ∉ Ring)
21.45.19.5  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 46945. 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 df-rngcALTV 46946 or dfrngc2 46958. 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 46951, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHom ↾ (𝐵 × 𝐵)), see rngchomfval 46952, whereas the composition is the ordinary composition of functions, see rngccofval 46956 and rngcco 46957. 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 46960, 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 46963. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 46964 with the identity function as identity arrow, see rngcid 46965.
Syntax	crngc 46943	Extend class notation to include the category Rng.
class RngCat
Syntax	crngcALTV 46944	Extend class notation to include the category Rng. (New usage is discouraged.)
class RngCatALTV
Definition	df-rngc 46945	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)))))
Definition	df-rngcALTV 46946*	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. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ RngCatALTV = (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Rng) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})
Theorem	rngcvalALTV 46947*	Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHom 𝑦)))    &   ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	rngcval 46948	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 46949	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 46950	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 46951	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 46952	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 46953	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 46954	A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	rngchomfeqhom 46955	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 46956	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 46957	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 46958	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 46959*	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 46960*	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 46961	Lemma 1 for rnghmsubcsetc 46963. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rnghmsubcsetclem2 46962*	Lemma 2 for rnghmsubcsetc 46963. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rnghmsubcsetc 46963	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 46964	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 46965	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 46966	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 46967	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 46968	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIso 𝑌)))
Theorem	rngcbasALTV 46969	Set of objects of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))
Theorem	rngchomfvalALTV 46970*	Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHom 𝑦)))
Theorem	rngchomALTV 46971	Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RngHom 𝑌))
Theorem	elrngchomALTV 46972	A morphism of non-unital rings is a function. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	rngccofvalALTV 46973*	Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))
Theorem	rngccoALTV 46974	Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋 RngHom 𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌 RngHom 𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	rngccatidALTV 46975*	Lemma for rngccatALTV 46976. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ ( I ↾ (Base‘𝑥)))))
Theorem	rngccatALTV 46976	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	rngcidALTV 46977	The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑆 = (Base‘𝑋)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑆))
Theorem	rngcsectALTV 46978	A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Base‘𝑋)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngHom 𝑌) ∧ 𝐺 ∈ (𝑌 RngHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))))
Theorem	rngcinvALTV 46979	An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngIso 𝑌) ∧ 𝐺 = ◡𝐹)))
Theorem	rngcisoALTV 46980	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIso 𝑌)))
Theorem	rngchomffvalALTV 46981*	The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) in maps-to notation for an operation. (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐹 = (Homf ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHom 𝑦)))
Theorem	rngchomrnghmresALTV 46982	The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) as restriction of the non-unital ring homomorphisms. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Rng ∩ 𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐹 = (Homf ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐹 = ( RngHom ↾ (𝐵 × 𝐵)))
Theorem	rngcifuestrc 46983*	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 46984*	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 46985, using cofuval2 17841 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 46983, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18105. (Contributed by AV, 26-Mar-2020.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	funcrngcsetcALT 46985*	Alternate proof of funcrngcsetc 46984, using cofuval2 17841 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 46983, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18105. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 46984. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	zrinitorngc 46986	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 46987	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 46988	The zero ring is a zero object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (ZeroO‘𝐶))
21.45.19.6  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 46991. 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 47004. 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 46997, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom ↾ (𝐵 × 𝐵)), see ringchomfval 46998, whereas the composition is the ordinary composition of functions, see ringccofval 47002 and ringcco 47003. By showing that the ring homomorphisms between rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rhmsscmap 47006, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 47009. It follows that the category of rings RingCat is actually a category, see ringccat 47010 with the identity function as identity arrow, see ringcid 47011. 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 47012, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 47015. 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 47016: ((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 47021.
Syntax	cringc 46989	Extend class notation to include the category Ring.
class RingCat
Syntax	cringcALTV 46990	Extend class notation to include the category Ring. (New usage is discouraged.)
class RingCatALTV
Definition	df-ringc 46991	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)))))
Definition	df-ringcALTV 46992*	Definition of the category Ring, relativized to a subset 𝑢. This is the category of all 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.) (New usage is discouraged.)
⊢ RingCatALTV = (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Ring) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})
Theorem	ringcvalALTV 46993*	Value of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RingHom 𝑦)))    &   ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	ringcval 46994	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 46995	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 46996	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 46997	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 46998	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 46999	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	elringchom 47000	A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))