P. 455 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45401-45500   *Has distinct variable group(s)

Type	Label	Description
Statement
20.41.17.2  Internal binary operations In this subsection, "internal binary operations" obeying different laws are defined.
Syntax	cintop 45401	Extend class notation with class of internal (binary) operations for a set.
class intOp
Syntax	cclintop 45402	Extend class notation with class of closed operations for a set.
class clIntOp
Syntax	cassintop 45403	Extend class notation with class of associative operations for a set.
class assIntOp
Definition	df-intop 45404*	Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020.)
⊢ intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚)))
Definition	df-clintop 45405	Function mapping a set to the class of all closed (internal binary) operations for this set, see definition in section 1.2 of [Hall] p. 2, definition in section I.1 of [Bruck] p. 1, or definition 1 in [BourbakiAlg1] p. 1, where it is called "a law of composition". (Contributed by AV, 20-Jan-2020.)
⊢ clIntOp = (𝑚 ∈ V ↦ (𝑚 intOp 𝑚))
Definition	df-assintop 45406*	Function mapping a set to the class of all associative (closed internal binary) operations for this set, see definition 5 in [BourbakiAlg1] p. 4, where it is called "an associative law of composition". (Contributed by AV, 20-Jan-2020.)
⊢ assIntOp = (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚})
Theorem	intopval 45407	The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 intOp 𝑁) = (𝑁 ↑m (𝑀 × 𝑀)))
Theorem	intop 45408	An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ (𝑀 intOp 𝑁) → ⚬ :(𝑀 × 𝑀)⟶𝑁)
Theorem	clintopval 45409	The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( clIntOp ‘𝑀) = (𝑀 ↑m (𝑀 × 𝑀)))
Theorem	assintopval 45410*	The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ ( clIntOp ‘𝑀) ∣ 𝑜 assLaw 𝑀})
Theorem	assintopmap 45411*	The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ (𝑀 ↑m (𝑀 × 𝑀)) ∣ 𝑜 assLaw 𝑀})
Theorem	isclintop 45412	The predicate "is a closed (internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( ⚬ ∈ ( clIntOp ‘𝑀) ↔ ⚬ :(𝑀 × 𝑀)⟶𝑀))
Theorem	clintop 45413	A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ :(𝑀 × 𝑀)⟶𝑀)
Theorem	assintop 45414	An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ⚬ assLaw 𝑀))
Theorem	isassintop 45415*	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 45416	The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ clLaw 𝑀)
Theorem	assintopcllaw 45417	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 45418	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 45419*	An associative (closed internal binary) operation for a set is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))
20.41.17.3  Alternative definitions for magmas and semigroups
Syntax	cmgm2 45420	Extend class notation with class of all magmas.
class MgmALT
Syntax	ccmgm2 45421	Extend class notation with class of all commutative magmas.
class CMgmALT
Syntax	csgrp2 45422	Extend class notation with class of all semigroups.
class SGrpALT
Syntax	ccsgrp2 45423	Extend class notation with class of all commutative semigroups.
class CSGrpALT
Definition	df-mgm2 45424	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 45425	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 45426	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 45427	A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.)
⊢ CSGrpALT = {𝑔 ∈ SGrpALT ∣ (+g‘𝑔) comLaw (Base‘𝑔)}
Theorem	ismgmALT 45428	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 45429	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 45430	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 45431	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 45432	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm)
Theorem	sgrp2sgrp 45433	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ SGrpALT ↔ 𝑀 ∈ Smgrp)
20.41.18  Categories (extension)
20.41.18.1  Subcategories (extension)
Theorem	idfusubc0 45434*	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 45435*	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 45436*	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 𝐶)𝐺)
20.41.19  Rings (extension)
20.41.19.1  Nonzero rings (extension)
Theorem	lmod0rng 45437	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 45438	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 45439	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 45440	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 45441	In a zero ring, a ring which is not a nonzero ring, the unit equals the zero element. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ (Ring ∖ NzRing) → 1 = 0 )
Theorem	nrhmzr 45442	There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝑍 ∈ (Ring ∖ NzRing) ∧ 𝑅 ∈ NzRing) → (𝑍 RingHom 𝑅) = ∅)
20.41.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 45443	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng0 45444*	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 45445*	The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
Theorem	rngabl 45446	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)
Theorem	rngmgp 45447	A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝐺 ∈ Smgrp)
Theorem	ringrng 45448	A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020.)
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng)
Theorem	ringssrng 45449	The unital rings are (non-unital) rings. (Contributed by AV, 20-Mar-2020.)
⊢ Ring ⊆ Rng
Theorem	isringrng 45450*	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 45451	Distributive law for the multiplication operation of a nonunital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Theorem	rngcl 45452	Closure of the multiplication operation of a nonunital ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	rnglz 45453	The zero of a nonunital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 )
20.41.19.3  Rng homomorphisms
Syntax	crngh 45454	non-unital ring homomorphisms.
class RngHomo
Syntax	crngs 45455	non-unital ring isomorphisms.
class RngIsom
Definition	df-rnghomo 45456*	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 45457*	Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)
⊢ RngIsom = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHomo 𝑠) ∣ ◡𝑓 ∈ (𝑠 RngHomo 𝑟)})
Theorem	rnghmrcl 45458	Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → (𝑅 ∈ Rng ∧ 𝑆 ∈ Rng))
Theorem	rnghmfn 45459	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 45460*	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 45461*	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 45462	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 45463	A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑀 MgmHom 𝑁))
Theorem	rnghmval2 45464	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 45465	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 45466	Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V))
Theorem	rnghmghm 45467	A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	rnghmf 45468	A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹:𝐵⟶𝐶)
Theorem	rnghmmul 45469	A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵)))
Theorem	isrnghm2d 45470*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆))
Theorem	isrnghmd 45471*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)))    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ⨣ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆))
Theorem	rnghmf1o 45472	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 45473	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 45474	An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	rngimrnghm 45475	An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆))
Theorem	rnghmco 45476	The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑇 RngHomo 𝑈) ∧ 𝐺 ∈ (𝑆 RngHomo 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RngHomo 𝑈))
Theorem	idrnghm 45477	The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → ( I ↾ 𝐵) ∈ (𝑅 RngHomo 𝑅))
Theorem	c0mgm 45478*	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 45479*	The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇))
Theorem	c0ghm 45480*	The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → 𝐻 ∈ (𝑆 GrpHom 𝑇))
Theorem	c0rhm 45481*	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 45482*	The constant mapping to zero is a nonunital ring homomorphism from any nonunital ring to the zero ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RngHomo 𝑇))
Theorem	c0snmgmhm 45483*	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 45484*	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 45485*	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 45486*	The constant mapping to zero is a nonunital ring homomorphism from the zero ring to any nonunital ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )    ⇒   ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑇 RngHomo 𝑆))
20.41.19.4  Ring homomorphisms (extension)
Theorem	rhmfn 45487	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 45488	The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.)
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))
Theorem	rhmisrnghm 45489	Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆))
20.41.19.5  Ideals as non-unital rings
Theorem	lidldomn1 45490*	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 45491	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 45492	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 45493	A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel)
Theorem	lidlmmgm 45494	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 45495	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 45496	A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng)
Theorem	zlidlring 45497	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 45498	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 45499	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)
20.41.19.6  The non-unital ring of even integers
Theorem	0even 45500*	0 is an even integer. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 0 ∈ 𝐸