P. 471 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47001-47100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	upwlkbprop 47001	Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 29-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(UPWalks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
Theorem	upwlkwlk 47002	A simple walk is a walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 27-Feb-2021.)
⊢ (𝐹(UPWalks‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	upgrwlkupwlk 47003	In a pseudograph, a walk is a simple walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 2-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → 𝐹(UPWalks‘𝐺)𝑃)
Theorem	upgrwlkupwlkb 47004	In a pseudograph, the definitions for a walk and a simple walk are equivalent. (Contributed by AV, 30-Dec-2020.)
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ 𝐹(UPWalks‘𝐺)𝑃))
Theorem	upgrisupwlkALT 47005*	Alternate proof of upgriswlk 29367 using the definition of UPGraph and related theorems. (Contributed by AV, 2-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
21.45.15.4  Edges of graphs expressed as sets of unordered pairs
Theorem	upgredgssspr 47006	The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 24-Nov-2021.)
⊢ (𝐺 ∈ UPGraph → (Edg‘𝐺) ⊆ (Pairs‘(Vtx‘𝐺)))
Theorem	uspgropssxp 47007*	The set 𝐺 of "simple pseudographs" for a fixed set 𝑉 of vertices is a subset of a Cartesian product. For more details about the class 𝐺 of all "simple pseudographs" see comments on uspgrbisymrel 47017. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ⊆ (𝑊 × 𝑃))
Theorem	uspgrsprfv 47008*	The value of the function 𝐹 which maps a "simple pseudograph" for a fixed set 𝑉 of vertices to the set of edges (i.e. range of the edge function) of the graph. Solely for 𝐺 as defined here, the function 𝐹 is a bijection between the "simple pseudographs" and the subsets of the set of pairs 𝑃 over the fixed set 𝑉 of vertices, see uspgrbispr 47014. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑋 ∈ 𝐺 → (𝐹‘𝑋) = (2nd ‘𝑋))
Theorem	uspgrsprf 47009*	The mapping 𝐹 is a function from the "simple pseudographs" with a fixed set of vertices 𝑉 into the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ 𝐹:𝐺⟶𝑃
Theorem	uspgrsprf1 47010*	The mapping 𝐹 is a one-to-one function from the "simple pseudographs" with a fixed set of vertices 𝑉 into the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 25-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ 𝐹:𝐺–1-1→𝑃
Theorem	uspgrsprfo 47011*	The mapping 𝐹 is a function from the "simple pseudographs" with a fixed set of vertices 𝑉 onto the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 25-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝐺–onto→𝑃)
Theorem	uspgrsprf1o 47012*	The mapping 𝐹 is a bijection between the "simple pseudographs" with a fixed set of vertices 𝑉 and the subsets of the set of pairs over the set 𝑉. See also the comments on uspgrbisymrel 47017. (Contributed by AV, 25-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝐺–1-1-onto→𝑃)
Theorem	uspgrex 47013*	The class 𝐺 of all "simple pseudographs" with a fixed set of vertices 𝑉 is a set. (Contributed by AV, 26-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ∈ V)
Theorem	uspgrbispr 47014*	There is a bijection between the "simple pseudographs" with a fixed set of vertices 𝑉 and the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 26-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ∃𝑓 𝑓:𝐺–1-1-onto→𝑃)
Theorem	uspgrspren 47015*	The set 𝐺 of the "simple pseudographs" with a fixed set of vertices 𝑉 and the class 𝑃 of subsets of the set of pairs over the fixed set 𝑉 are equinumerous. (Contributed by AV, 27-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑃)
Theorem	uspgrymrelen 47016*	The set 𝐺 of the "simple pseudographs" with a fixed set of vertices 𝑉 and the class 𝑅 of the symmetric relations on the fixed set 𝑉 are equinumerous. For more details about the class 𝐺 of all "simple pseudographs" see comments on uspgrbisymrel 47017. (Contributed by AV, 27-Nov-2021.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑅)
Theorem	uspgrbisymrel 47017*	There is a bijection between the "simple pseudographs" for a fixed set 𝑉 of vertices and the class 𝑅 of the symmetric relations on the fixed set 𝑉. The simple pseudographs, which are graphs without hyper- or multiedges, but which may contain loops, are expressed as ordered pairs of the vertices and the edges (as proper or improper unordered pairs of vertices, not as indexed edges!) in this theorem. That class 𝐺 of such simple pseudographs is a set (if 𝑉 is a set, see uspgrex 47013) of equivalence classes of graphs abstracting from the index sets of their edge functions. Solely for this abstraction, there is a bijection between the "simple pseudographs" as members of 𝐺 and the symmetric relations 𝑅 on the fixed set 𝑉 of vertices. This theorem would not hold for 𝐺 = {𝑔 ∈ USPGraph ∣ (Vtx‘𝑔) = 𝑉} and even not for 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ⟨𝑣, 𝑒⟩ ∈ USPGraph)}, because these are much bigger classes. (Proposed by Gerard Lang, 16-Nov-2021.) (Contributed by AV, 27-Nov-2021.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ∃𝑓 𝑓:𝐺–1-1-onto→𝑅)
Theorem	uspgrbisymrelALT 47018*	Alternate proof of uspgrbisymrel 47017 not using the definition of equinumerosity. (Contributed by AV, 26-Nov-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ∃𝑓 𝑓:𝐺–1-1-onto→𝑅)
21.45.16  Monoids (extension)
21.45.16.1  Auxiliary theorems
Theorem	ovn0dmfun 47019	If a class operation value for two operands is not the empty set, then the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 6924. (Contributed by AV, 27-Jan-2020.)
⊢ ((𝐴𝐹𝐵) ≠ ∅ → (⟨𝐴, 𝐵⟩ ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {⟨𝐴, 𝐵⟩})))
Theorem	xpsnopab 47020*	A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020.)
⊢ ({𝑋} × 𝐶) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶)}
Theorem	xpiun 47021*	A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.)
⊢ (𝐵 × 𝐶) = ∪ 𝑥 ∈ 𝐵 {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶)}
Theorem	ovn0ssdmfun 47022*	If a class' operation value for two operands is not the empty set, the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 6924. (Contributed by AV, 27-Jan-2020.)
⊢ (∀𝑎 ∈ 𝐷 ∀𝑏 ∈ 𝐸 (𝑎𝐹𝑏) ≠ ∅ → ((𝐷 × 𝐸) ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ (𝐷 × 𝐸))))
Theorem	fnxpdmdm 47023	The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020.)
⊢ (𝐹 Fn (𝐴 × 𝐴) → dom dom 𝐹 = 𝐴)
Theorem	cnfldsrngbas 47024	The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ⊆ ℂ → 𝑆 = (Base‘𝑅))
Theorem	cnfldsrngadd 47025	The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ 𝑉 → + = (+g‘𝑅))
Theorem	cnfldsrngmul 47026	The ring multiplication operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ 𝑉 → · = (.r‘𝑅))
21.45.16.2  Magmas, Semigroups and Monoids (extension)
Theorem	plusfreseq 47027	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 47028	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 47029	A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020.)
⊢ (Base‘𝑀) = ∅    ⇒   ⊢ (𝑀 ∈ 𝑉 → 𝑀 ∈ Mgm)
21.45.16.3  Examples and counterexamples for magmas, semigroups and monoids (extension)
Theorem	opmpoismgm 47030*	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 47031*	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‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑀 ∈ Smgrp)
Theorem	copisnmnd 47032*	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 47033*	0 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 0 ∉ 𝑂
Theorem	1odd 47034*	1 is an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 1 ∈ 𝑂
Theorem	2nodd 47035*	2 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 2 ∉ 𝑂
Theorem	oddibas 47036*	Lemma 1 for oddinmgm 47038: 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 47037*	Lemma 2 for oddinmgm 47038: 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 47038*	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 47113, and even a non-unital ring, see 2zrng 47104. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    &   ⊢ 𝑀 = (ℂfld ↾s 𝑂)    ⇒   ⊢ 𝑀 ∉ Mgm
Theorem	nnsgrpmgm 47039	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 47040	The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝑀 = (ℂfld ↾s ℕ)    ⇒   ⊢ 𝑀 ∈ Smgrp
Theorem	nnsgrpnmnd 47041	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
Theorem	nn0mnd 47042	The set of nonnegative integers under (complex) addition is a monoid. Example in [Lang] p. 6. Remark: 𝑀 could have also been written as (ℂfld ↾s ℕ0). (Contributed by AV, 27-Dec-2023.)
⊢ 𝑀 = {⟨(Base‘ndx), ℕ0⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ 𝑀 ∈ Mnd
21.45.16.4  Group sum operation (extension 1)
Theorem	gsumsplit2f 47043*	Split a group sum into two parts. (Contributed by AV, 4-Sep-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)) + (𝐺 Σg (𝑘 ∈ 𝐷 ↦ 𝑋))))
Theorem	gsumdifsndf 47044*	Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.)
⊢ Ⅎ𝑘𝑌    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp (0g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ (𝐴 ∖ {𝑀}) ↦ 𝑋)) + 𝑌))
Theorem	gsumfsupp 47045	A group sum of a family can be restricted to the support of that family without changing its value, provided that that support is finite. This corresponds to the definition of an (infinite) product in [Lang] p. 5, last two formulas. (Contributed by AV, 27-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (𝐹 supp 0 )    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐼)) = (𝐺 Σg 𝐹))
21.45.17  Magmas and internal binary operations (alternate approach) With df-mpo 7406, binary operations are defined by a rule, and with df-ov 7404, 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 47062. If, in addition, the result is also contained in the set 𝑆, the operation is called closed internal binary operation, see df-clintop 47063. 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 47063 ). 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 47063 and df-assintop 47064), 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 47049 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 47057, or for an alternate definition df-mgm2 47082 for a magma as extensible structure. Similar results are obtained for an associative operation (defining semigroups).
21.45.17.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 47046	Extend class notation for the closure law.
class clLaw
Syntax	casslaw 47047	Extend class notation for the associative law.
class assLaw
Syntax	ccomlaw 47048	Extend class notation for the commutative law.
class comLaw
Definition	df-cllaw 47049*	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 47050*	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 47051*	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 47052*	The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.)
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ clLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) ∈ 𝑀))
Theorem	iscomlaw 47053*	The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.)
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ comLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) = (𝑦 ⚬ 𝑥)))
Theorem	clcllaw 47054	Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.)
⊢ (( ⚬ clLaw 𝑀 ∧ 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀) → (𝑋 ⚬ 𝑌) ∈ 𝑀)
Theorem	isasslaw 47055*	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.)
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ assLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
Theorem	asslawass 47056*	Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.)
⊢ ( ⚬ assLaw 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))
Theorem	mgmplusgiopALT 47057	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 47058	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.)
⊢ (𝐺 ∈ Smgrp → (+g‘𝐺) assLaw (Base‘𝐺))
21.45.17.2  Internal binary operations In this subsection, "internal binary operations" obeying different laws are defined.
Syntax	cintop 47059	Extend class notation with class of internal (binary) operations for a set.
class intOp
Syntax	cclintop 47060	Extend class notation with class of closed operations for a set.
class clIntOp
Syntax	cassintop 47061	Extend class notation with class of associative operations for a set.
class assIntOp
Definition	df-intop 47062*	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 47063	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 47064*	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 47065	The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 intOp 𝑁) = (𝑁 ↑m (𝑀 × 𝑀)))
Theorem	intop 47066	An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ (𝑀 intOp 𝑁) → ⚬ :(𝑀 × 𝑀)⟶𝑁)
Theorem	clintopval 47067	The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( clIntOp ‘𝑀) = (𝑀 ↑m (𝑀 × 𝑀)))
Theorem	assintopval 47068*	The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ ( clIntOp ‘𝑀) ∣ 𝑜 assLaw 𝑀})
Theorem	assintopmap 47069*	The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.)
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ (𝑀 ↑m (𝑀 × 𝑀)) ∣ 𝑜 assLaw 𝑀})
Theorem	isclintop 47070	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 47071	A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ :(𝑀 × 𝑀)⟶𝑀)
Theorem	assintop 47072	An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ⚬ assLaw 𝑀))
Theorem	isassintop 47073*	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 47074	The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ clLaw 𝑀)
Theorem	assintopcllaw 47075	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 47076	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 47077*	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.45.17.3  Alternative definitions for magmas and semigroups
Syntax	cmgm2 47078	Extend class notation with class of all magmas.
class MgmALT
Syntax	ccmgm2 47079	Extend class notation with class of all commutative magmas.
class CMgmALT
Syntax	csgrp2 47080	Extend class notation with class of all semigroups.
class SGrpALT
Syntax	ccsgrp2 47081	Extend class notation with class of all commutative semigroups.
class CSGrpALT
Definition	df-mgm2 47082	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 47083	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 47084	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 47085	A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.)
⊢ CSGrpALT = {𝑔 ∈ SGrpALT ∣ (+g‘𝑔) comLaw (Base‘𝑔)}
Theorem	ismgmALT 47086	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 47087	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 47088	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 47089	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 47090	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm)
Theorem	sgrp2sgrp 47091	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
⊢ (𝑀 ∈ SGrpALT ↔ 𝑀 ∈ Smgrp)
21.45.18  Rings (extension)
21.45.18.1  Nonzero rings (extension)
Theorem	lmod0rng 47092	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 47093	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.45.18.2  Ideals as non-unital rings
Theorem	lidldomn1 47094*	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 47095	A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel)
Theorem	lidlrng 47096	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 47097	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 47098	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 47099	A (left) ideal of a domain which is neither the zero ideal nor the unit ideal is not a unital ring. (Contributed by AV, 18-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵)) → 𝐼 ∉ Ring)
21.45.18.3  The non-unital ring of even integers
Theorem	0even 47100*	0 is an even integer. (Contributed by AV, 11-Feb-2020.)
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)}    ⇒   ⊢ 0 ∈ 𝐸