P. 429 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42801-42900   *Has distinct variable group(s)

Type	Label	Description
Statement
20.36.14.2  Magmas and Semigroups (extension)
Theorem	plusfreseq 42801	If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily a magma), the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ⨣ = (+𝑓‘𝑀)    ⇒   ⊢ (∅ ∉ ran ⨣ → ( + ↾ (𝐵 × 𝐵)) = ⨣ )
Theorem	mgmplusfreseq 42802	If the empty set is not contained in the base set of a magma, the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ⨣ = (+𝑓‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mgm ∧ ∅ ∉ 𝐵) → ( + ↾ (𝐵 × 𝐵)) = ⨣ )
Theorem	0mgm 42803	A set with an empty base set is always a magma". (Contributed by AV, 25-Feb-2020.)
⊢ (Base‘𝑀) = ∅    ⇒   ⊢ (𝑀 ∈ 𝑉 → 𝑀 ∈ Mgm)
Theorem	mgmpropd 42804*	If two structures have the same (nonempty) base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a magma iff the other one is. (Contributed by AV, 25-Feb-2020.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Mgm ↔ 𝐿 ∈ Mgm))
Theorem	ismgmd 42805*	Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mgm)
20.36.14.3  Magma homomorphisms and submagmas
Syntax	cmgmhm 42806	Hom-set generator class for magmas.
class MgmHom
Syntax	csubmgm 42807	Class function taking a magma to its lattice of submagmas.
class SubMgm
Definition	df-mgmhm 42808*	A magma homomorphism is a function on the base sets which preserves the binary operation. (Contributed by AV, 24-Feb-2020.)
⊢ MgmHom = (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))})
Definition	df-submgm 42809*	A submagma is a subset of a magma which is closed under the operation. Such subsets are themselves magmas. (Contributed by AV, 24-Feb-2020.)
⊢ SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡})
Theorem	mgmhmrcl 42810	Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020.)
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm))
Theorem	submgmrcl 42811	Reverse closure for submagmas. (Contributed by AV, 24-Feb-2020.)
⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑀 ∈ Mgm)
Theorem	ismgmhm 42812*	Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))))
Theorem	mgmhmf 42813	A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → 𝐹:𝐵⟶𝐶)
Theorem	mgmhmpropd 42814*	Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020.)
⊢ (𝜑 → 𝐵 = (Base‘𝐽))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐶 ≠ ∅)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦))    ⇒   ⊢ (𝜑 → (𝐽 MgmHom 𝐾) = (𝐿 MgmHom 𝑀))
Theorem	mgmhmlin 42815	A magma homomorphism preserves the binary operation. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)))
Theorem	mgmhmf1o 42816	A magma homomorphism is bijective iff its converse is also a magma homomorphism. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 MgmHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 MgmHom 𝑅)))
Theorem	idmgmhm 42817	The identity homomorphism on a magma. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → ( I ↾ 𝐵) ∈ (𝑀 MgmHom 𝑀))
Theorem	issubmgm 42818*	Expand definition of a submagma. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)))
Theorem	issubmgm2 42819	Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm)))
Theorem	rabsubmgmd 42820*	Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mgm)    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) → 𝜂)    &   ⊢ (𝑧 = 𝑥 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑧 = (𝑥 + 𝑦) → (𝜓 ↔ 𝜂))    ⇒   ⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMgm‘𝑀))
Theorem	submgmss 42821	Submagmas are subsets of the base set. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑆 ⊆ 𝐵)
Theorem	submgmid 42822	Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → 𝐵 ∈ (SubMgm‘𝑀))
Theorem	submgmcl 42823	Submagmas are closed under the monoid operation. (Contributed by AV, 26-Feb-2020.)
⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑆 ∈ (SubMgm‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	submgmmgm 42824	Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝐻 ∈ Mgm)
Theorem	submgmbas 42825	The base set of a submagma. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑆 = (Base‘𝐻))
Theorem	subsubmgm 42826	A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMgm‘𝐺) → (𝐴 ∈ (SubMgm‘𝐻) ↔ (𝐴 ∈ (SubMgm‘𝐺) ∧ 𝐴 ⊆ 𝑆)))
Theorem	resmgmhm 42827	Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝑋 ∈ (SubMgm‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MgmHom 𝑇))
Theorem	resmgmhm2 42828	One direction of resmgmhm2b 42829. (Contributed by AV, 26-Feb-2020.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑈) ∧ 𝑋 ∈ (SubMgm‘𝑇)) → 𝐹 ∈ (𝑆 MgmHom 𝑇))
Theorem	resmgmhm2b 42829	Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ 𝐹 ∈ (𝑆 MgmHom 𝑈)))
Theorem	mgmhmco 42830	The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑇 MgmHom 𝑈) ∧ 𝐺 ∈ (𝑆 MgmHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MgmHom 𝑈))
Theorem	mgmhmima 42831	The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMgm‘𝑁))
Theorem	mgmhmeql 42832	The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝐺 ∈ (𝑆 MgmHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMgm‘𝑆))
Theorem	submgmacs 42833	Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mgm → (SubMgm‘𝐺) ∈ (ACS‘𝐵))
Theorem	ismhm0 42834	Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑌 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ (𝐹‘ 0 ) = 𝑌)))
Theorem	mhmismgmhm 42835	Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝐹 ∈ (𝑅 MgmHom 𝑆))
20.36.14.4  Examples and counterexamples for magmas, semigroups and monoids (extension)
Theorem	opmpt2ismgm 42836*	A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑀 ∈ Mgm)
Theorem	copissgrp 42837*	A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑀 ∈ SGrp)
Theorem	copisnmnd 42838*	A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 1 < (♯‘𝐵))    ⇒   ⊢ (𝜑 → 𝑀 ∉ Mnd)
Theorem	0nodd 42839*	0 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 0 ∉ 𝑂
Theorem	1odd 42840*	1 is an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 1 ∈ 𝑂
Theorem	2nodd 42841*	2 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 2 ∉ 𝑂
Theorem	oddibas 42842*	Lemma 1 for oddinmgm 42844: The base set of M is the set of all odd integers. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    &   ⊢ 𝑀 = (ℂfld ↾s 𝑂)    ⇒   ⊢ 𝑂 = (Base‘𝑀)
Theorem	oddiadd 42843*	Lemma 2 for oddinmgm 42844: The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    &   ⊢ 𝑀 = (ℂfld ↾s 𝑂)    ⇒   ⊢ + = (+g‘𝑀)
Theorem	oddinmgm 42844*	The structure of all odd integers together with the addition of complex numbers is not a magma. Remark: the structure of the complementary subset of the set of integers, the even integers, is a magma, actually an abelian group, see 2zrngaabl 42973, and even a non-unital ring, see 2zrng 42964. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    &   ⊢ 𝑀 = (ℂfld ↾s 𝑂)    ⇒   ⊢ 𝑀 ∉ Mgm
Theorem	nnsgrpmgm 42845	The structure of positive integers together with the addition of complex numbers is a magma. (Contributed by AV, 4-Feb-2020.)
⊢ 𝑀 = (ℂfld ↾s ℕ)    ⇒   ⊢ 𝑀 ∈ Mgm
Theorem	nnsgrp 42846	The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝑀 = (ℂfld ↾s ℕ)    ⇒   ⊢ 𝑀 ∈ SGrp
Theorem	nnsgrpnmnd 42847	The structure of positive integers together with the addition of complex numbers is not a monoid. (Contributed by AV, 4-Feb-2020.)
⊢ 𝑀 = (ℂfld ↾s ℕ)    ⇒   ⊢ 𝑀 ∉ Mnd
20.36.15  Magmas and internal binary operations (alternate approach) With df-mpt2 6929, binary operations are defined by a rule, and with df-ov 6927, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation (19-Jan-2020), "... a binary operation on a set 𝑆 is a mapping of the elements of the Cartesian product 𝑆 × 𝑆 to S: 𝑓:𝑆 × 𝑆⟶𝑆. Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, we call binary operations mapping the elements of the Cartesian product 𝑆 × 𝑆 internal binary operations, see df-intop 42864. If, in addition, the result is also contained in the set 𝑆, the operation is called closed internal binary operation, see df-clintop 42865. Therefore, a "binary operation on a set 𝑆" according to Wikipedia is a "closed internal binary operation" in our terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations ). Taking a step back, we define "laws" applicable for "binary operations" (which even need not to be functions), according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7. These laws are used, on the one hand, to specialize internal binary operations (see df-clintop 42865 and df-assintop 42866), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obey these laws, are defined afterwards. Notice that in [BourbakiAlg1] p. 1, p. 4 and p. 7, these operations are called "laws" by themselves. In the following, an alternate definition df-cllaw 42851 for an internal binary operation is provided, which does not require function-ness, but only closure. Therefore, this definition could be used as binary operation (Slot 2) defined for a magma as extensible structure, see mgmplusgiopALT 42859, or for an alternate definition df-mgm2 42884 for a magma as extensible structure. Similar results are obtained for an associative operation (defining semigroups).
20.36.15.1  Laws for internal binary operations In this subsection, the "laws" applicable for "binary operations" according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7 are defined. These laws are called "internal laws" in [BourbakiAlg1] p. xxi.
Syntax	ccllaw 42848	Extend class notation for the closure law.
class clLaw
Syntax	casslaw 42849	Extend class notation for the associative law.
class assLaw
Syntax	ccomlaw 42850	Extend class notation for the commutative law.
class comLaw
Definition	df-cllaw 42851*	The closure law for binary operations, see definitions of laws A0. and M0. in section 1.1 of [Hall] p. 1, or definition 1 in [BourbakiAlg1] p. 1: the value of a binary operation applied to two operands of a given sets is an element of this set. By this definition, the closure law is expressed as binary relation: a binary operation is related to a set by clLaw if the closure law holds for this binary operation regarding this set. Note that the binary operation needs not to be a function. (Contributed by AV, 7-Jan-2020.)
⊢ clLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) ∈ 𝑚}
Definition	df-comlaw 42852*	The commutative law for binary operations, see definitions of laws A2. and M2. in section 1.1 of [Hall] p. 1, or definition 8 in [BourbakiAlg1] p. 7: the value of a binary operation applied to two operands equals the value of a binary operation applied to the two operands in reversed order. By this definition, the commutative law is expressed as binary relation: a binary operation is related to a set by comLaw if the commutative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by AV, 7-Jan-2020.)
⊢ comLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)}
Definition	df-asslaw 42853*	The associative law for binary operations, see definitions of laws A1. and M1. in section 1.1 of [Hall] p. 1, or definition 5 in [BourbakiAlg1] p. 4: the value of a binary operation applied the value of the binary operation applied to two operands and a third operand equals the value of the binary operation applied to the first operand and the value of the binary operation applied to the second and third operand. By this definition, the associative law is expressed as binary relation: a binary operation is related to a set by assLaw if the associative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.)
⊢ assLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
Theorem	iscllaw 42854*	The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.)
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ clLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) ∈ 𝑀))
Theorem	iscomlaw 42855*	The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.)
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ comLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) = (𝑦 ⚬ 𝑥)))
Theorem	clcllaw 42856	Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.)
⊢ (( ⚬ clLaw 𝑀 ∧ 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀) → (𝑋 ⚬ 𝑌) ∈ 𝑀)
Theorem	isasslaw 42857*	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.)
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ assLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
Theorem	asslawass 42858*	Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.)
⊢ ( ⚬ assLaw 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))
Theorem	mgmplusgiopALT 42859	Slot 2 (group operation) of a magma as extensible structure is a closed operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑀 ∈ Mgm → (+g‘𝑀) clLaw (Base‘𝑀))
Theorem	sgrpplusgaopALT 42860	Slot 2 (group operation) of a semigroup as extensible structure is an associative operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ SGrp → (+g‘𝐺) assLaw (Base‘𝐺))
20.36.15.2  Internal binary operations In this subsection, "internal binary operations" obeying different laws are defined.
Syntax	cintop 42861	Extend class notation with class of internal (binary) operations for a set.
class intOp
Syntax	cclintop 42862	Extend class notation with class of closed operations for a set.
class clIntOp
Syntax	cassintop 42863	Extend class notation with class of associative operations for a set.
class assIntOp
Definition	df-intop 42864*	Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020.)
⊢ intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑𝑚 (𝑚 × 𝑚)))
Definition	df-clintop 42865	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 42866*	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 42867	The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 intOp 𝑁) = (𝑁 ↑𝑚 (𝑀 × 𝑀)))
Theorem	intop 42868	An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ (𝑀 intOp 𝑁) → ⚬ :(𝑀 × 𝑀)⟶𝑁)
Theorem	clintopval 42869	The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( clIntOp ‘𝑀) = (𝑀 ↑𝑚 (𝑀 × 𝑀)))
Theorem	assintopval 42870*	The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ ( clIntOp ‘𝑀) ∣ 𝑜 assLaw 𝑀})
Theorem	assintopmap 42871*	The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ (𝑀 ↑𝑚 (𝑀 × 𝑀)) ∣ 𝑜 assLaw 𝑀})
Theorem	isclintop 42872	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 42873	A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ :(𝑀 × 𝑀)⟶𝑀)
Theorem	assintop 42874	An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ⚬ assLaw 𝑀))
Theorem	isassintop 42875*	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 42876	The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ clLaw 𝑀)
Theorem	assintopcllaw 42877	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 42878	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 42879*	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.36.15.3  Alternative definitions for Magmas and Semigroups
Syntax	cmgm2 42880	Extend class notation with class of all magmas.
class MgmALT
Syntax	ccmgm2 42881	Extend class notation with class of all commutative magmas.
class CMgmALT
Syntax	csgrp2 42882	Extend class notation with class of all semigroups.
class SGrpALT
Syntax	ccsgrp2 42883	Extend class notation with class of all commutative semigroups.
class CSGrpALT
Definition	df-mgm2 42884	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 42885	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 42886	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 42887	A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.)
⊢ CSGrpALT = {𝑔 ∈ SGrpALT ∣ (+g‘𝑔) comLaw (Base‘𝑔)}
Theorem	ismgmALT 42888	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 42889	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 42890	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 42891	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 42892	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm)
Theorem	sgrp2sgrp 42893	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ SGrpALT ↔ 𝑀 ∈ SGrp)
20.36.16  Categories (extension)
20.36.16.1  Subcategories (extension)
Theorem	idfusubc0 42894*	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 42895*	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 42896*	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.36.17  Rings (extension)
20.36.17.1  Nonzero rings (extension)
Theorem	lmod0rng 42897	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 42898	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 42899	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 42900	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 })