P. 135 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13401-13500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pwsplusgval 13401	Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ✚ 𝐺) = (𝐹 ∘𝑓 + 𝐺))
Theorem	pwsmulrval 13402	Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝐹 ∘𝑓 · 𝐺))
Theorem	pwsdiagel 13403	Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑌)    ⇒   ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝐴 ∈ 𝐵) → (𝐼 × {𝐴}) ∈ 𝐶)
Theorem	pwssnf1o 13404*	Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s {𝐼})    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ({𝐼} × {𝑥}))    &   ⊢ 𝐶 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵–1-1-onto→𝐶)
6.1.4  Definition of the structure quotient
Syntax	cimas 13405	Image structure function.
class “s
Syntax	cqus 13406	Quotient structure function.
class /s
Syntax	cxps 13407	Binary product structure function.
class ×s
Definition	df-iimas 13408*	Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly 𝑓 must either be injective or satisfy the well-definedness condition 𝑓(𝑎) = 𝑓(𝑐) ∧ 𝑓(𝑏) = 𝑓(𝑑) → 𝑓(𝑎 + 𝑏) = 𝑓(𝑐 + 𝑑) for each relevant operation. Note that although we call this an "image" by association to df-ima 4740, in order to keep the definition simple we consider only the case when the domain of 𝐹 is equal to the base set of 𝑅. Other cases can be achieved by restricting 𝐹 (with df-res 4739) and/or 𝑅 ( with df-iress 13113) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.)
⊢ “s = (𝑓 ∈ V, 𝑟 ∈ V ↦ ⦋(Base‘𝑟) / 𝑣⦌{⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩})
Definition	df-qus 13409*	Define a quotient ring (or quotient group), which is a special case of an image structure df-iimas 13408 where the image function is 𝑥 ↦ [𝑥]𝑒. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟))
Definition	df-xps 13410*	Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
⊢ ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
Theorem	imasex 13411	Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝐹 “s 𝑅) ∈ V)
Theorem	imasival 13412*	Value of an image structure. The is a lemma for the theorems imasbas 13413, imasplusg 13414, and imasmulr 13415 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ + = (+g‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑈 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})
Theorem	imasbas 13413	The base set of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑈))
Theorem	imasplusg 13414*	The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
Theorem	imasmulr 13415*	The ring multiplication in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
Theorem	f1ocpbllem 13416	Lemma for f1ocpbl 13417. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	f1ocpbl 13417	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷))))
Theorem	f1ovscpbl 13418	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐹‘𝐵) = (𝐹‘𝐶) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐴 + 𝐶))))
Theorem	f1olecpbl 13419	An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷)))
Theorem	imasaddfnlemg 13420*	The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))
Theorem	imasaddvallemg 13421*	The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasaddflemg 13422*	The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵)
Theorem	imasaddfn 13423*	The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))
Theorem	imasaddval 13424*	The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasaddf 13425*	The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵)
Theorem	imasmulfn 13426*	The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))
Theorem	imasmulval 13427*	The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasmulf 13428*	The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵)
Theorem	qusval 13429*	Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
Theorem	quslem 13430*	The function in qusval 13429 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐹:𝑉–onto→(𝑉 / ∼ ))
Theorem	qusex 13431	Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.)
⊢ ((𝑅 ∈ 𝑉 ∧ ∼ ∈ 𝑊) → (𝑅 /s ∼ ) ∈ V)
Theorem	qusin 13432	Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ( ∼ “ 𝑉) ⊆ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 = (𝑅 /s ( ∼ ∩ (𝑉 × 𝑉))))
Theorem	qusbas 13433	Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (𝑉 / ∼ ) = (Base‘𝑈))
Theorem	divsfval 13434*	Value of the function in qusval 13429. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = [𝐴] ∼ )
Theorem	divsfvalg 13435*	Value of the function in qusval 13429. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = [𝐴] ∼ )
Theorem	ercpbllemg 13436*	Lemma for ercpbl 13437. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ 𝐴 ∼ 𝐵))
Theorem	ercpbl 13437*	Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 + 𝑏) ∈ 𝑉)    &   ⊢ (𝜑 → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷))))
Theorem	erlecpbl 13438*	Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷)))
Theorem	qusaddvallemg 13439*	Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    &   ⊢ (𝜑 → · ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusaddflemg 13440*	The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    &   ⊢ (𝜑 → · ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	qusaddval 13441*	The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusaddf 13442*	The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	qusmulval 13443*	The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusmulf 13444*	The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	fnpr2o 13445	Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o)
Theorem	fnpr2ob 13446	Biconditional version of fnpr2o 13445. (Contributed by Jim Kingdon, 27-Sep-2023.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o)
Theorem	fvpr0o 13447	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ (𝐴 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴)
Theorem	fvpr1o 13448	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ (𝐵 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) = 𝐵)
Theorem	fvprif 13449	The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵))
Theorem	xpsfrnel 13450*	Elementhood in the target space of the function 𝐹 appearing in xpsval 13458. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐺 ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
Theorem	xpsfeq 13451	A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝐺 Fn 2o → {⟨∅, (𝐺‘∅)⟩, ⟨1o, (𝐺‘1o)⟩} = 𝐺)
Theorem	xpsfrnel2 13452*	Elementhood in the target space of the function 𝐹 appearing in xpsval 13458. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))
Theorem	xpscf 13453	Equivalent condition for the pair function to be a proper function on 𝐴. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩}:2o⟶𝐴 ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴))
Theorem	xpsfval 13454*	The value of the function appearing in xpsval 13458. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐹𝑌) = {⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩})
Theorem	xpsff1o 13455*	The function appearing in xpsval 13458 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {∅, 1o}. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)
Theorem	xpsfrn 13456*	A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ ran 𝐹 = X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)
Theorem	xpsff1o2 13457*	The function appearing in xpsval 13458 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {∅, 1o}. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→ran 𝐹
Theorem	xpsval 13458*	Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝑈 = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})    ⇒   ⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈))
PART 7  BASIC ALGEBRAIC STRUCTURES
7.1  Monoids
7.1.1  Magmas According to Wikipedia ("Magma (algebra)", 08-Jan-2020, https://en.wikipedia.org/wiki/magma_(algebra)) "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.". Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following: With df-mpo 6028, binary operations are defined by a rule, and with df-ov 6026, 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 6026 (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, binary operations mapping the elements of the Cartesian product 𝑆 × 𝑆 are more precisely called internal binary operations. If, in addition, the result is also contained in the set 𝑆, the operation should be called closed internal binary operation. Therefore, a "binary operation on a set 𝑆" according to Wikipedia is a "closed internal binary operation" in a more precise 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 6026). The definition of magmas (Mgm, see df-mgm 13462) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible.
Syntax	cplusf 13459	Extend class notation with group addition as a function.
class +𝑓
Syntax	cmgm 13460	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 13461*	Define group addition function. Usually we will use +g directly instead of +𝑓, and they have the same behavior in most cases. The main advantage of +𝑓 for any magma is that it is a guaranteed function (mgmplusf 13472), while +g only has closure (mgmcl 13465). (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦)))
Definition	df-mgm 13462*	A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [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 FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ Mgm = {𝑔 ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
Theorem	ismgm 13463*	The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
Theorem	ismgmn0 13464*	The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
Theorem	mgmcl 13465	Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵)
Theorem	isnmgm 13466	A condition for a structure not to be a magma. (Contributed by AV, 30-Jan-2020.) (Proof shortened by NM, 5-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 ⚬ 𝑌) ∉ 𝐵) → 𝑀 ∉ Mgm)
Theorem	mgmsscl 13467	If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    ⇒   ⊢ (((𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(+g‘𝐺)𝑌) ∈ 𝑆)
Theorem	plusffvalg 13468*	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ⨣ = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)))
Theorem	plusfvalg 13469	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⨣ 𝑌) = (𝑋 + 𝑌))
Theorem	plusfeqg 13470	If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ + Fn (𝐵 × 𝐵)) → ⨣ = + )
Theorem	plusffng 13471	The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ⨣ Fn (𝐵 × 𝐵))
Theorem	mgmplusf 13472	The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revisd by AV, 28-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⨣ = (+𝑓‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → ⨣ :(𝐵 × 𝐵)⟶𝐵)
Theorem	intopsn 13473	The internal operation for a set is the trivial operation iff the set is a singleton. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 23-Jan-2020.)
⊢ (( ⚬ :(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ⚬ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}))
Theorem	mgmb1mgm1 13474	The only magma with a base set consisting of one element is the trivial magma (at least if its operation is an internal binary operation). (Contributed by AV, 23-Jan-2020.) (Revised by AV, 7-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn (𝐵 × 𝐵)) → (𝐵 = {𝑍} ↔ + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}))
Theorem	mgm0 13475	Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.)
⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ Mgm)
Theorem	mgm1 13476	The structure with one element and the only closed internal operation for a singleton is a magma. (Contributed by AV, 10-Feb-2020.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mgm)
Theorem	opifismgmdc 13477*	A structure with a group addition operation expressed by a conditional operator is a magma if both values of the conditional operator are contained in the base set. (Contributed by AV, 9-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝜓, 𝐶, 𝐷))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → DECID 𝜓)    &   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑀 ∈ Mgm)
7.1.2  Identity elements According to Wikipedia ("Identity element", 7-Feb-2020, https://en.wikipedia.org/wiki/Identity_element): "In mathematics, an identity element, or neutral element, is a special type of element of a set with respect to a binary operation on that set, which leaves any element of the set unchanged when combined with it.". Or in more detail "... an element e of S is called a left identity if e * a = a for all a in S, and a right identity if a * e = a for all a in S. If e is both a left identity and a right identity, then it is called a two-sided identity, or simply an identity." We concentrate on two-sided identities in the following. The existence of an identity (an identity is unique if it exists, see mgmidmo 13478) is an important property of monoids, and therefore also for groups, but also for magmas not required to be associative. Magmas with an identity element are called "unital magmas" (see Definition 2 in [BourbakiAlg1] p. 12) or, if the magmas are cancellative, "loops" (see definition in [Bruck] p. 15). In the context of extensible structures, the identity element (of any magma 𝑀) is defined as "group identity element" (0g‘𝑀), see df-0g 13364. Related theorems which are already valid for magmas are provided in the following.
Theorem	mgmidmo 13478*	A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.)
⊢ ∃*𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥)
Theorem	grpidvalg 13479*	The value of the identity element of a group. (Contributed by NM, 20-Aug-2011.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 0 = (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))))
Theorem	grpidpropdg 13480*	If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (0g‘𝐾) = (0g‘𝐿))
Theorem	fn0g 13481	The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 0g Fn V
Theorem	0g0 13482	The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.)
⊢ ∅ = (0g‘∅)
Theorem	ismgmid 13483*	The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → ∃𝑒 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))    ⇒   ⊢ (𝜑 → ((𝑈 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑈 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑈) = 𝑥)) ↔ 0 = 𝑈))
Theorem	mgmidcl 13484*	The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → ∃𝑒 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))    ⇒   ⊢ (𝜑 → 0 ∈ 𝐵)
Theorem	mgmlrid 13485*	The identity element of a magma, if it exists, is a left and right identity. (Contributed by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → ∃𝑒 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
Theorem	ismgmid2 13486*	Show that a given element is the identity element of a magma. (Contributed by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 𝑈) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑈 = 0 )
Theorem	lidrideqd 13487*	If there is a left and right identity element for any binary operation (group operation) +, both identity elements are equal. Generalization of statement in [Lang] p. 3: it is sufficient that "e" is a left identity element and "e`" is a right identity element instead of both being (two-sided) identity elements. (Contributed by AV, 26-Dec-2023.)
⊢ (𝜑 → 𝐿 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐿 + 𝑥) = 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑥 + 𝑅) = 𝑥)    ⇒   ⊢ (𝜑 → 𝐿 = 𝑅)
Theorem	lidrididd 13488*	If there is a left and right identity element for any binary operation (group operation) +, the left identity element (and therefore also the right identity element according to lidrideqd 13487) is equal to the two-sided identity element. (Contributed by AV, 26-Dec-2023.)
⊢ (𝜑 → 𝐿 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐿 + 𝑥) = 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑥 + 𝑅) = 𝑥)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → 𝐿 = 0 )
Theorem	grpidd 13489*	Deduce the identity element of a magma from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)    ⇒   ⊢ (𝜑 → 0 = (0g‘𝐺))
Theorem	mgmidsssn0 13490*	Property of the set of identities of 𝐺. Either 𝐺 has no identities, and 𝑂 = ∅, or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑂 ⊆ { 0 })
Theorem	grpinvalem 13491*	Lemma for grpinva 13492. (Contributed by NM, 9-Aug-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝑂 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑋) = 𝑋)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 = 𝑂)
Theorem	grpinva 13492*	Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝑂 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑁 + 𝑋) = 𝑂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑁) = 𝑂)
Theorem	grprida 13493*	Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝑂 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 𝑂) = 𝑥)
7.1.3  Iterated sums in a magma The symbol Σg is mostly used in the context of abelian groups. Therefore, it is usually called "group sum". It can be defined, however, in arbitrary magmas (then it should be called "iterated sum"). If the magma is not required to be commutative or associative, then the order of the summands and the order in which summations are done become important. If the magma is not unital, then one cannot define a meaningful empty sum. See the comment for df-igsum 13365.
Theorem	fngsum 13494	Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.)
⊢ Σg Fn (V × V)
Theorem	igsumvalx 13495*	Expand out the substitutions in df-igsum 13365. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → dom 𝐹 = 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (℩𝑥((𝐴 = ∅ ∧ 𝑥 = 0 ) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))))
Theorem	igsumval 13496*	Expand out the substitutions in df-igsum 13365. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (℩𝑥((𝐴 = ∅ ∧ 𝑥 = 0 ) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))))
Theorem	gsumfzval 13497	An expression for Σg when summing over a finite set of sequential integers. (Contributed by Jim Kingdon, 14-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)))
Theorem	gsumpropd 13498	The group sum depends only on the base set and additive operation. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Proof shortened by Mario Carneiro, 18-Sep-2015.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))    &   ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Theorem	gsumpropd2 13499*	A stronger version of gsumpropd 13498, working for magma, where only the closure of the addition operation on a common base is required, see gsummgmpropd 13500. (Contributed by Thierry Arnoux, 28-Jun-2017.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))    &   ⊢ ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g‘𝐺)𝑡) ∈ (Base‘𝐺))    &   ⊢ ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g‘𝐺)𝑡) = (𝑠(+g‘𝐻)𝑡))    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Theorem	gsummgmpropd 13500*	A stronger version of gsumpropd 13498 if at least one of the involved structures is a magma, see gsumpropd2 13499. (Contributed by AV, 31-Jan-2020.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ Mgm)    &   ⊢ ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g‘𝐺)𝑡) = (𝑠(+g‘𝐻)𝑡))    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))