P. 465 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46401-46500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inclfusubc 46401*	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.43.19  Rings (extension)
21.43.19.1  Nonzero rings (extension)
Theorem	lmod0rng 46402	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 46403	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	0ringdif 46404	A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ (Ring ∖ NzRing) ↔ (𝑅 ∈ Ring ∧ 𝐵 = { 0 }))
Theorem	0ringbas 46405	The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ (Ring ∖ NzRing) → 𝐵 = { 0 })
Theorem	0ring1eq0 46406	In a zero ring, a ring which is not a nonzero ring, the ring unity equals the zero element. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ (Ring ∖ NzRing) → 1 = 0 )
Theorem	nrhmzr 46407	There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝑍 ∈ (Ring ∖ NzRing) ∧ 𝑅 ∈ NzRing) → (𝑍 RingHom 𝑅) = ∅)
21.43.19.2  Non-unital rings ("rngs") According to Wikipedia, "... in abstract algebra, a rng (or pseudo-ring or non-unital ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 6-Jan-2020).
Syntax	crng 46408	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng 46409*	Define class of all non-unital rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.)
⊢ Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ Smgrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
Theorem	isrng 46410*	The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
Theorem	rngabl 46411	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)
Theorem	rngmgp 46412	A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝐺 ∈ Smgrp)
Theorem	ringrng 46413	A unital ring is a non-unital ring. (Contributed by AV, 6-Jan-2020.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng)
Theorem	ringssrng 46414	The unital rings are non-unital rings. (Contributed by AV, 20-Mar-2020.)
⊢ Ring ⊆ Rng
Theorem	isringrng 46415*	The predicate "is a unital ring" as extension of the predicate "is a non-unital ring". (Contributed by AV, 17-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Rng ∧ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑦 ∧ (𝑦 · 𝑥) = 𝑦)))
Theorem	rngdir 46416	Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Theorem	rngcl 46417	Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	rnglz 46418	The zero of a non-unital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 )
21.43.19.3  Rng homomorphisms
Syntax	crngh 46419	non-unital ring homomorphisms.
class RngHomo
Syntax	crngs 46420	non-unital ring isomorphisms.
class RngIsom
Definition	df-rnghomo 46421*	Define the set of non-unital ring homomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)
⊢ RngHomo = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))})
Definition	df-rngisom 46422*	Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)
⊢ RngIsom = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHomo 𝑠) ∣ ◡𝑓 ∈ (𝑠 RngHomo 𝑟)})
Theorem	rnghmrcl 46423	Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → (𝑅 ∈ Rng ∧ 𝑆 ∈ Rng))
Theorem	rnghmfn 46424	The mapping of two non-unital rings to the non-unital ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
⊢ RngHomo Fn (Rng × Rng)
Theorem	rnghmval 46425*	The set of the non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 22-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∗ = (.r‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑆)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) → (𝑅 RngHomo 𝑆) = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ✚ (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) ∗ (𝑓‘𝑦)))})
Theorem	isrnghm 46426*	A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∗ = (.r‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) ↔ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦)))))
Theorem	isrnghmmul 46427	A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) ↔ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ (𝑀 MgmHom 𝑁))))
Theorem	rnghmmgmhm 46428	A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑀 MgmHom 𝑁))
Theorem	rnghmval2 46429	The non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 1-Mar-2020.)
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) → (𝑅 RngHomo 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MgmHom (mulGrp‘𝑆))))
Theorem	isrngisom 46430	An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RngIsom 𝑆) ↔ (𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ ◡𝐹 ∈ (𝑆 RngHomo 𝑅))))
Theorem	rngimrcl 46431	Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V))
Theorem	rnghmghm 46432	A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	rnghmf 46433	A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹:𝐵⟶𝐶)
Theorem	rnghmmul 46434	A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵)))
Theorem	isrnghm2d 46435*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆))
Theorem	isrnghmd 46436*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆))
Theorem	rnghmf1o 46437	A non-unital ring homomorphism is bijective iff its converse is also a non-unital ring homomorphism. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 RngHomo 𝑅)))
Theorem	isrngim 46438	An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RngIsom 𝑆) ↔ (𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶)))
Theorem	rngimf1o 46439	An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	rngimrnghm 46440	An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆))
Theorem	rnghmco 46441	The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑇 RngHomo 𝑈) ∧ 𝐺 ∈ (𝑆 RngHomo 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RngHomo 𝑈))
Theorem	idrnghm 46442	The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → ( I ↾ 𝐵) ∈ (𝑅 RngHomo 𝑅))
Theorem	c0mgm 46443*	The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MgmHom 𝑇))
Theorem	c0mhm 46444*	The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇))
Theorem	c0ghm 46445*	The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → 𝐻 ∈ (𝑆 GrpHom 𝑇))
Theorem	c0rhm 46446*	The constant mapping to zero is a ring homomorphism from any ring to the zero ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Ring ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RingHom 𝑇))
Theorem	c0rnghm 46447*	The constant mapping to zero is a non-unital ring homomorphism from any non-unital ring to the zero ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RngHomo 𝑇))
Theorem	c0snmgmhm 46448*	The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ (♯‘𝐵) = 1) → 𝐻 ∈ (𝑇 MgmHom 𝑆))
Theorem	c0snmhm 46449*	The constant mapping to zero is a monoid homomorphism from the trivial monoid (consisting of the zero only) to any monoid. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    &   ⊢ 𝑍 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = {𝑍}) → 𝐻 ∈ (𝑇 MndHom 𝑆))
Theorem	c0snghm 46450*	The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    &   ⊢ 𝑍 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = {𝑍}) → 𝐻 ∈ (𝑇 GrpHom 𝑆))
Theorem	zrrnghm 46451*	The constant mapping to zero is a non-unital ring homomorphism from the zero ring to any non-unital ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑇 RngHomo 𝑆))
21.43.19.4  Ring homomorphisms (extension)
Theorem	rhmfn 46452	The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
⊢ RingHom Fn (Ring × Ring)
Theorem	rhmval 46453	The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.)
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))
Theorem	rhmisrnghm 46454	Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆))
21.43.19.5  Ideals as non-unital rings
Theorem	lidldomn1 46455*	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	lidlssbas 46456	The base set of the restriction of the ring to a (left) ideal is a subset of the base set of the ring. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅))
Theorem	lidlbas 46457	A (left) ideal of a ring is the base set of the restriction of the ring to this ideal. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) = 𝑈)
Theorem	lidlabl 46458	A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel)
Theorem	lidlmmgm 46459	The multiplicative group of a (left) ideal of a ring is a magma. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Mgm)
Theorem	lidlmsgrp 46460	The multiplicative group of a (left) ideal of a ring is a semigroup. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Smgrp)
Theorem	lidlrng 46461	A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng)
Theorem	zlidlring 46462	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 46463	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 46464	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.43.19.6  The non-unital ring of even integers
Theorem	0even 46465*	0 is an even integer. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 0 ∈ 𝐸
Theorem	1neven 46466*	1 is not an even integer. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 1 ∉ 𝐸
Theorem	2even 46467*	2 is an even integer. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 2 ∈ 𝐸
Theorem	2zlidl 46468*	The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑈 = (LIdeal‘ℤring)    ⇒   ⊢ 𝐸 ∈ 𝑈
Theorem	2zrng 46469*	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 46345. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑈 = (LIdeal‘ℤring)    &   ⊢ 𝑅 = (ℤring ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	2zrngbas 46470*	The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝐸 = (Base‘𝑅)
Theorem	2zrngadd 46471*	The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ + = (+g‘𝑅)
Theorem	2zrng0 46472*	The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 0 = (0g‘𝑅)
Theorem	2zrngamgm 46473*	R is an (additive) magma. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Mgm
Theorem	2zrngasgrp 46474*	R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Smgrp
Theorem	2zrngamnd 46475*	R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Mnd
Theorem	2zrngacmnd 46476*	R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ CMnd
Theorem	2zrngagrp 46477*	R is an (additive) group. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Grp
Theorem	2zrngaabl 46478*	R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ 𝑅 ∈ Abel
Theorem	2zrngmul 46479*	The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    ⇒   ⊢ · = (.r‘𝑅)
Theorem	2zrngmmgm 46480*	R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑀 ∈ Mgm
Theorem	2zrngmsgrp 46481*	R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑀 ∈ Smgrp
Theorem	2zrngALT 46482*	The ring of integers restricted to the even integers is a non-unital ring, the "ring of even integers". Alternate version of 2zrng 46469, 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 46478) and a multiplicative semigroup (see 2zrngmsgrp 46481). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	2zrngnmlid 46483*	R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑏 ∈ 𝐸 ∃𝑎 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎
Theorem	2zrngnmrid 46484*	R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎
Theorem	2zrngnmlid2 46485*	R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎
Theorem	2zrngnring 46486*	R is not a unital ring. (Contributed by AV, 6-Jan-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    &   ⊢ 𝑅 = (ℂfld ↾s 𝐸)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ 𝑅 ∉ Ring
21.43.19.7  A constructed not unital ring
Theorem	cznrnglem 46487	Lemma for cznrng 46489: 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 46488	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 46489*	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 46490*	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.43.19.8  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 RngHomo 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 46493. 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 46494 or dfrngc2 46506. 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 46499, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHomo ↾ (𝐵 × 𝐵)), see rngchomfval 46500, whereas the composition is the ordinary composition of functions, see rngccofval 46504 and rngcco 46505. 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 46508, 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 46511. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 46512 with the identity function as identity arrow, see rngcid 46513.
Syntax	crngc 46491	Extend class notation to include the category Rng.
class RngCat
Syntax	crngcALTV 46492	Extend class notation to include the category Rng. (New usage is discouraged.)
class RngCatALTV
Definition	df-rngc 46493	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 ( RngHomo ↾ ((𝑢 ∩ Rng) × (𝑢 ∩ Rng)))))
Definition	df-rngcALTV 46494*	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), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})
Theorem	rngcvalALTV 46495*	Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHomo 𝑦)))    &   ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	rngcval 46496	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))    &   ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐶 = ((ExtStrCat‘𝑈) ↾cat 𝐻))
Theorem	rnghmresfn 46497	The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020.)
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝐵 × 𝐵))
Theorem	rnghmresel 46498	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.)
⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐹 ∈ (𝑋𝐻𝑌)) → 𝐹 ∈ (𝑋 RngHomo 𝑌))
Theorem	rngcbas 46499	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 46500	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 ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵)))