P. 491 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49001-49100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clintop 49001	A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ :(𝑀 × 𝑀)⟶𝑀)
Theorem	assintop 49002	An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ⚬ assLaw 𝑀))
Theorem	isassintop 49003*	The predicate "is an associative (closed internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( ⚬ ∈ ( assIntOp ‘𝑀) ↔ ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))
Theorem	clintopcllaw 49004	The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ clLaw 𝑀)
Theorem	assintopcllaw 49005	The closure low holds for an associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ⚬ clLaw 𝑀)
Theorem	assintopasslaw 49006	The associative low holds for a associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ⚬ assLaw 𝑀)
Theorem	assintopass 49007*	An associative (closed internal binary) operation for a set is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))
21.49.17.3  Alternative definitions for magmas and semigroups
Syntax	cmgm2 49008	Extend class notation with class of all magmas.
class MgmALT
Syntax	ccmgm2 49009	Extend class notation with class of all commutative magmas.
class CMgmALT
Syntax	csgrp2 49010	Extend class notation with class of all semigroups.
class SGrpALT
Syntax	ccsgrp2 49011	Extend class notation with class of all commutative semigroups.
class CSGrpALT
Definition	df-mgm2 49012	A magma is a set equipped with a closed operation. Definition 1 of [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by AV, 6-Jan-2020.)
⊢ MgmALT = {𝑚 ∣ (+g‘𝑚) clLaw (Base‘𝑚)}
Definition	df-cmgm2 49013	A commutative magma is a magma with a commutative operation. Definition 8 of [BourbakiAlg1] p. 7. (Contributed by AV, 20-Jan-2020.)
⊢ CMgmALT = {𝑚 ∈ MgmALT ∣ (+g‘𝑚) comLaw (Base‘𝑚)}
Definition	df-sgrp2 49014	A semigroup is a magma with an associative operation. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4, or of a semigroup in section 1.3 of [Hall] p. 7. (Contributed by AV, 6-Jan-2020.)
⊢ SGrpALT = {𝑔 ∈ MgmALT ∣ (+g‘𝑔) assLaw (Base‘𝑔)}
Definition	df-csgrp2 49015	A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.)
⊢ CSGrpALT = {𝑔 ∈ SGrpALT ∣ (+g‘𝑔) comLaw (Base‘𝑔)}
Theorem	ismgmALT 49016	The predicate "is a magma". (Contributed by AV, 16-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ MgmALT ↔ ⚬ clLaw 𝐵))
Theorem	iscmgmALT 49017	The predicate "is a commutative magma". (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ CMgmALT ↔ (𝑀 ∈ MgmALT ∧ ⚬ comLaw 𝐵))
Theorem	issgrpALT 49018	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 49019	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 49020	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm)
Theorem	sgrp2sgrp 49021	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ SGrpALT ↔ 𝑀 ∈ Smgrp)
21.49.18  Rings (extension)
21.49.18.1  Nonzero rings (extension)
Theorem	lmod0rng 49022	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 49023	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‘𝑅))
21.49.18.2  Ideals as non-unital rings
Theorem	lidldomn1 49024*	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 49025	A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel)
Theorem	lidlrng 49026	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 49027	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 49028	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 49029	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.49.18.3  The non-unital ring of even integers
Theorem	0even 49030*	0 is an even integer. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 0 ∈ 𝐸
Theorem	1neven 49031*	1 is not an even integer. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 1 ∉ 𝐸
Theorem	2even 49032*	2 is an even integer. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 2 ∈ 𝐸
Theorem	2zlidl 49033*	The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑈 = (LIdeal‘ℤring)    ⇒   ⊢ 𝐸 ∈ 𝑈
Theorem	2zrng 49034*	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 48968. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑈 = (LIdeal‘ℤring)    &   ⊢ 𝑅 = (ℤring ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	2zrngbas 49035*	The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝐸 = (Base‘𝑅)
Theorem	2zrngadd 49036*	The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ + = (+g‘𝑅)
Theorem	2zrng0 49037*	The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 0 = (0g‘𝑅)
Theorem	2zrngamgm 49038*	R is an (additive) magma. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Mgm
Theorem	2zrngasgrp 49039*	R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Smgrp
Theorem	2zrngamnd 49040*	R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Mnd
Theorem	2zrngacmnd 49041*	R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ CMnd
Theorem	2zrngagrp 49042*	R is an (additive) group. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Grp
Theorem	2zrngaabl 49043*	R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Abel
Theorem	2zrngmul 49044*	The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ · = (.r‘𝑅)
Theorem	2zrngmmgm 49045*	R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑀 ∈ Mgm
Theorem	2zrngmsgrp 49046*	R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑀 ∈ Smgrp
Theorem	2zrngALT 49047*	The ring of integers restricted to the even integers is a non-unital ring, the "ring of even integers". Alternate version of 2zrng 49034, 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 49043) and a multiplicative semigroup (see 2zrngmsgrp 49046). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	2zrngnmlid 49048*	R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑏 ∈ 𝐸 ∃𝑎 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎
Theorem	2zrngnmrid 49049*	R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎
Theorem	2zrngnmlid2 49050*	R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎
Theorem	2zrngnring 49051*	R is not a unital ring. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑅 ∉ Ring
21.49.18.4  A constructed not unital ring
Theorem	cznrnglem 49052	Lemma for cznrng 49054: 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 49053	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 49054*	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 49055*	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.49.18.5  The category of non-unital rings (alternate definition) As an alternative to df-rngc 20725, the "category of non-unital rings" can be defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, according to dfrngc2 20736.
Syntax	crngcALTV 49056	Extend class notation to include the category Rng. (New usage is discouraged.)
class RngCatALTV
Definition	df-rngcALTV 49057*	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 49058*	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	rngcbasALTV 49059	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 49060*	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 49061	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 49062	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 49063*	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 49064	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 49065*	Lemma for rngccatALTV 49066. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ ( I ↾ (Base‘𝑥)))))
Theorem	rngccatALTV 49066	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	rngcidALTV 49067	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 49068	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 49069	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 49070	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 49071*	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 49072	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	rngcrescrhmALTV 49073	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → (𝐶 ↾cat 𝐻) = ((𝐶 ↾s 𝑅) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rhmsubcALTVlem1 49074	Lemma 1 for rhmsubcALTV 49078. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅))
Theorem	rhmsubcALTVlem2 49075	Lemma 2 for rhmsubcALTV 49078. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	rhmsubcALTVlem3 49076*	Lemma 3 for rhmsubcALTV 49078. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcALTVlem4 49077*	Lemma 4 for rhmsubcALTV 49078. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(RngCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcALTV 49078	According to df-subc 17873, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17901 and subcss2 17904). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘(RngCatALTV‘𝑈)))
Theorem	rhmsubcALTVcat 49079	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → ((RngCatALTV‘𝑈) ↾cat 𝐻) ∈ Cat)
21.49.18.6  The category of (unital) rings (alternate definition) As an alternative to df-ringc 20754, the "category of unital rings" can be defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, according to dfringc2 20765.
Syntax	cringcALTV 49080	Extend class notation to include the category Ring. (New usage is discouraged.)
class RingCatALTV
Definition	df-ringcALTV 49081*	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 49082*	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	funcringcsetcALTV2lem1 49083*	Lemma 1 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋))
Theorem	funcringcsetcALTV2lem2 49084*	Lemma 2 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈)
Theorem	funcringcsetcALTV2lem3 49085*	Lemma 3 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
Theorem	funcringcsetcALTV2lem4 49086*	Lemma 4 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))
Theorem	funcringcsetcALTV2lem5 49087*	Lemma 5 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ (𝑋 RingHom 𝑌)))
Theorem	funcringcsetcALTV2lem6 49088*	Lemma 6 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐻 ∈ (𝑋 RingHom 𝑌)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻)
Theorem	funcringcsetcALTV2lem7 49089*	Lemma 7 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝑅)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋)))
Theorem	funcringcsetcALTV2lem8 49090*	Lemma 8 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑅)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌)))
Theorem	funcringcsetcALTV2lem9 49091*	Lemma 9 for funcringcsetcALTV2 49092. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑅)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑅)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(⟨𝑋, 𝑌⟩(comp‘𝑅)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))
Theorem	funcringcsetcALTV2 49092*	The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	ringcbasALTV 49093	Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))
Theorem	ringchomfvalALTV 49094*	Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RingHom 𝑦)))
Theorem	ringchomALTV 49095	Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	elringchomALTV 49096	A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	ringccofvalALTV 49097*	Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))
Theorem	ringccoALTV 49098	Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋 RingHom 𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌 RingHom 𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	ringccatidALTV 49099*	Lemma for ringccatALTV 49100. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ ( I ↾ (Base‘𝑥)))))
Theorem	ringccatALTV 49100	The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)