P. 334 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	odutos 33301	Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset)
Theorem	tlt2 33302	In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋))
Theorem	tlt3 33303	In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋))
Theorem	trleile 33304	In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋))
Theorem	toslublem 33305*	Lemma for toslub 33306 and xrsclat 33344. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑))))
Theorem	toslub 33306	In a toset, the lowest upper bound lub, defined for partial orders is the supremum, sup(𝐴, 𝐵, < ), defined for total orders. (these are the set.mm definitions: lowest upper bound and supremum are normally synonymous). Note that those two values are also equal if such a supremum does not exist: in that case, both are equal to the empty set. (Contributed by Thierry Arnoux, 15-Feb-2018.) (Revised by Thierry Arnoux, 24-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ((lub‘𝐾)‘𝐴) = sup(𝐴, 𝐵, < ))
Theorem	tosglblem 33307*	Lemma for tosglb 33308 and xrsclat 33344. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑))))
Theorem	tosglb 33308	Same theorem as toslub 33306, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < ))
21.3.9.3  Complete lattices
Theorem	clatp0cl 33309	The poset zero of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0.‘𝑊)    ⇒   ⊢ (𝑊 ∈ CLat → 0 ∈ 𝐵)
Theorem	clatp1cl 33310	The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 1 = (1.‘𝑊)    ⇒   ⊢ (𝑊 ∈ CLat → 1 ∈ 𝐵)
21.3.9.4  Order Theory
Syntax	cmnt 33311	Extend class notation with monotone functions.
class Monot
Syntax	cmgc 33312	Extend class notation with the monotone Galois connection.
class MGalConn
Definition	df-mnt 33313*	Define a monotone function between two ordered sets. (Contributed by Thierry Arnoux, 20-Apr-2024.)
⊢ Monot = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))})
Definition	df-mgc 33314*	Define monotone Galois connections. See mgcval 33320 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.)
⊢ MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))})
Theorem	mntoval 33315*	Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉Monot𝑊) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝑓‘𝑥) ≲ (𝑓‘𝑦))})
Theorem	ismnt 33316*	Express the statement "𝐹 is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 ∈ (𝑉Monot𝑊) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))))
Theorem	ismntd 33317	Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌))
Theorem	mntf 33318	A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ (𝑉Monot𝑊)) → 𝐹:𝐴⟶𝐵)
Theorem	mgcoval 33319*	Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉MGalConn𝑊) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))})
Theorem	mgcval 33320*	Monotone Galois connection between two functions 𝐹 and 𝐺. If this relation is satisfied, 𝐹 is called the lower adjoint of 𝐺, and 𝐺 is called the upper adjoint of 𝐹. Technically, this is implemented as an operation taking a pair of structures 𝑉 and 𝑊, expected to be posets, which gives a relation between pairs of functions 𝐹 and 𝐺. If such a relation exists, it can be proven to be unique. Galois connections generalize the fundamental theorem of Galois theory about the correspondence between subgroups and subfields. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)))))
Theorem	mgcf1 33321	The lower adjoint 𝐹 of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
Theorem	mgcf2 33322	The upper adjoint 𝐺 of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
Theorem	mgccole1 33323	An inequality for the kernel operator 𝐺 ∘ 𝐹. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ≤ (𝐺‘(𝐹‘𝑋)))
Theorem	mgccole2 33324	Inequality for the closure operator (𝐹 ∘ 𝐺) of the Galois connection 𝐻. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐺‘𝑌)) ≲ 𝑌)
Theorem	mgcmnt1 33325	The lower adjoint 𝐹 of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌))
Theorem	mgcmnt2 33326	The upper adjoint 𝐺 of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≲ 𝑌)    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) ≤ (𝐺‘𝑌))
Theorem	mgcmntco 33327*	A Galois connection like statement, for two functions with same range. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ 𝐶 = (Base‘𝑋)    &   ⊢ < = (le‘𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ Proset )    &   ⊢ (𝜑 → 𝐾 ∈ (𝑉Monot𝑋))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑊Monot𝑋))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥)) ↔ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)))
Theorem	dfmgc2lem 33328*	Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))    &   ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)    ⇒   ⊢ (𝜑 → 𝐹𝐻𝐺)
Theorem	dfmgc2 33329*	Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
Theorem	mgcmnt1d 33330	Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))
Theorem	mgcmnt2d 33331	Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
Theorem	mgccnv 33332	The inverse Galois connection is the Galois connection of the dual orders. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝑀 = ((ODual‘𝑊)MGalConn(ODual‘𝑉))    ⇒   ⊢ ((𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → (𝐹𝐻𝐺 ↔ 𝐺𝑀𝐹))
Theorem	pwrssmgc 33333*	Given a function 𝐹, exhibit a Galois connection between subsets of its domain and subsets of its range. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐺 = (𝑛 ∈ 𝒫 𝑌 ↦ (◡𝐹 “ 𝑛))    &   ⊢ 𝐻 = (𝑚 ∈ 𝒫 𝑋 ↦ {𝑦 ∈ 𝑌 ∣ (◡𝐹 “ {𝑦}) ⊆ 𝑚})    &   ⊢ 𝑉 = (toInc‘𝒫 𝑌)    &   ⊢ 𝑊 = (toInc‘𝒫 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    ⇒   ⊢ (𝜑 → 𝐺(𝑉MGalConn𝑊)𝐻)
Theorem	mgcf1olem1 33334	Property of a Galois connection, lemma for mgcf1o 33336. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐹‘𝑋))) = (𝐹‘𝑋))
Theorem	mgcf1olem2 33335	Property of a Galois connection, lemma for mgcf1o 33336. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌))
Theorem	mgcf1o 33336	Given a Galois connection, exhibit an order isomorphism. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹))
21.3.9.5  Extended reals Structure - misc additions
Axiom	ax-xrssca 33337	Assume the scalar component of the extended real structure is the field of the real numbers (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ℝfld = (Scalar‘ℝ*𝑠)
Axiom	ax-xrsvsca 33338	Assume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ·e = ( ·𝑠 ‘ℝ*𝑠)
Theorem	xrs0 33339	The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13285 and df-xrs 17566), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ 0 = (0g‘ℝ*𝑠)
Theorem	xrslt 33340	The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ < = (lt‘ℝ*𝑠)
Theorem	xrsinvgval 33341	The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13285 and df-xrs 17566), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵)
Theorem	xrsmulgzz 33342	The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))
Theorem	xrstos 33343	The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ Toset
Theorem	xrsclat 33344	The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ CLat
Theorem	xrsp0 33345	The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Proof shortened by AV, 28-Sep-2020.)
⊢ -∞ = (0.‘ℝ*𝑠)
Theorem	xrsp1 33346	The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
⊢ +∞ = (1.‘ℝ*𝑠)
21.3.9.6  The extended nonnegative real numbers commutative monoid
Theorem	xrge00 33347	The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0mulgnn0 33348	The group multiple function in the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 14-Jun-2017.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴(.g‘(ℝ*𝑠 ↾s (0[,]+∞)))𝐵) = (𝐴 ·e 𝐵))
Theorem	xrge0addass 33349	Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xrge0addgt0 33350	The sum of nonnegative and positive numbers is positive. See addgtge0 11712. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵))
Theorem	xrge0adddir 33351	Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)))
Theorem	xrge0adddi 33352	Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵)))
Theorem	xrge0npcan 33353	Extended nonnegative real version of npcan 11476. (Contributed by Thierry Arnoux, 9-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
Theorem	fsumrp0cl 33354*	Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞))
21.3.10  Algebra
21.3.10.1  Monoids
Theorem	mndcld 33355	Closure of the operation of a monoid. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	mndassd 33356	A monoid operation is associative. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	mndlrinv 33357	In a monoid, if an element 𝑋 has both a left inverse 𝑀 and a right inverse 𝑁, they are equal. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 + 𝑋) = 0 )    &   ⊢ (𝜑 → (𝑋 + 𝑁) = 0 )    ⇒   ⊢ (𝜑 → 𝑀 = 𝑁)
Theorem	mndlrinvb 33358*	In a monoid, if an element has both a left-inverse and a right-inverse, they are equal. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 ∧ ∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ) ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
Theorem	mndlactf1 33359*	If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐹 is injective. See also grplactf1o 19120. Remark in chapter I. of [BourbakiAlg1] p. 17 . (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 + 𝑋) = 0 )    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐵)
Theorem	mndlactfo 33360*	An element 𝑋 of a monoid 𝐸 is left-invertible iff its left-translation 𝐹 is surjective. See also grplactf1o 19120. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑋 + 𝑦) = 0 ))
Theorem	mndractf1 33361*	If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐺 is injective. See also grplactf1o 19120. Remark in chapter I. of [BourbakiAlg1] p. 17 . (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 + 𝑌) = 0 )    ⇒   ⊢ (𝜑 → 𝐺:𝐵–1-1→𝐵)
Theorem	mndractfo 33362*	An element 𝑋 of a monoid 𝐸 is right-invertible iff its right-translation 𝐺 is surjective. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 ))
Theorem	mndlactf1o 33363*	An element 𝑋 of a monoid 𝐸 is invertible iff its left-translation 𝐹 is bijective. See also grplactf1o 19120. Remark in chapter I. of [BourbakiAlg1] p. 17. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
Theorem	mndractf1o 33364*	An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33363. Remark in chapter I. of [BourbakiAlg1] p. 17 . (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
Theorem	cmn4d 33365	Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	cmn246135 33366	Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33602. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑌 + (𝑈 + 𝑊)) + (𝑋 + (𝑍 + 𝑉))))
Theorem	cmn145236 33367	Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33602. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑋 + (𝑈 + 𝑉)) + (𝑌 + (𝑍 + 𝑊))))
21.3.10.2  Monoids Homomorphisms
Theorem	abliso 33368	The image of an Abelian group by a group isomorphism is also Abelian. (Contributed by Thierry Arnoux, 8-Mar-2018.)
⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → 𝑁 ∈ Abel)
Theorem	lmhmghmd 33369	A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	mhmimasplusg 33370	Value of the operation of the surjective image. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑊 = (𝐹 “s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ 𝐶 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐵–onto→𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉 MndHom 𝑊))    &   ⊢ + = (+g‘𝑉)    &   ⊢ ⨣ = (+g‘𝑊)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)) = (𝐹‘(𝑋 + 𝑌)))
Theorem	lmhmimasvsca 33371	Value of the scalar product of the surjective image of a module. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑊 = (𝐹 “s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ 𝐶 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐵–onto→𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉 LMHom 𝑊))    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ × = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘(Scalar‘𝑉))    ⇒   ⊢ (𝜑 → (𝑋 × (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
21.3.10.3  Groups - misc additions
Theorem	grpidcld 33372	The identity element of a group belongs to the group. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 0 ∈ 𝐵)
Theorem	grpinvinvd 33373	Double inverse law for groups. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑁‘𝑋)) = 𝑋)
Theorem	grpsubcld 33374	Closure of group subtraction. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝐵)
Theorem	subgsubcld 33375	A subgroup is closed under group subtraction. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑆)
Theorem	subgmulgcld 33376	Closure of the group multiple within a subgroup. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))    &   ⊢ (𝜑 → 𝑍 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑍 · 𝐴) ∈ 𝑆)
Theorem	ressmulgnn0d 33377	Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 14-Jun-2017.)
⊢ (𝜑 → (𝐺 ↾s 𝐴) = 𝐻)    &   ⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻))    &   ⊢ (𝜑 → 𝐴 ⊆ (Base‘𝐺))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑁(.g‘𝐻)𝑋) = (𝑁(.g‘𝐺)𝑋))
21.3.10.4  Abelian Groups - misc additions
Theorem	ablcomd 33378	An abelian group operation is commutative, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))
21.3.10.5  Finitely supported group sums - misc additions
Theorem	gsumsubg 33379	The group sum in a subgroup is the same as the group sum. (Contributed by Thierry Arnoux, 28-May-2023.)
⊢ 𝐻 = (𝐺 ↾s 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Theorem	gsumsra 33380	The group sum in a subring algebra is the same as the ring's group sum. (Contributed by Thierry Arnoux, 28-May-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 Σg 𝐹) = (𝐴 Σg 𝐹))
Theorem	gsummpt2co 33381*	Split a finite sum into a sum of a collection of sums over disjoint subsets. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐸)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐷)    ⇒   ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)))))
Theorem	gsummpt2d 33382*	Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 20052. (Contributed by Thierry Arnoux, 27-Apr-2020.)
⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑊 ∈ CMnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))))
Theorem	lmodvslmhm 33383*	Scalar multiplication in a left module by a fixed element is a group homomorphism. (Contributed by Thierry Arnoux, 12-Jun-2023.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐾 ↦ (𝑥 · 𝑌)) ∈ (𝐹 GrpHom 𝑊))
Theorem	gsumvsmul1 33384*	Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 20408, since every ring is a left module over itself. (Contributed by Thierry Arnoux, 12-Jun-2023.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑆 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ LMod)    &   ⊢ (𝜑 → 𝑆 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑆 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌))
Theorem	gsummptres 33385*	Extend a finite group sum by padding outside with zeroes. Proof generated using OpenAI's proof assistant. (Contributed by Thierry Arnoux, 11-Jul-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐷)) → 𝐶 = 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑥 ∈ (𝐴 ∩ 𝐷) ↦ 𝐶)))
Theorem	gsummptres2 33386*	Extend a finite group sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 22-Jun-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝑆)) → 𝑌 = 0 )    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝑌)) = (𝐺 Σg (𝑥 ∈ 𝑆 ↦ 𝑌)))
Theorem	gsummptfsres 33387*	Extend a finitely supported group sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝑆)) → 𝑌 = 0 )    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑌) finSupp 0 )    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝑌)) = (𝐺 Σg (𝑥 ∈ 𝑆 ↦ 𝑌)))
Theorem	gsummptf1od 33388*	Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018.)
⊢ Ⅎ𝑥𝐻    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 = 𝐸) → 𝐶 = 𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐹)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐸 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐷 𝑥 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑦 ∈ 𝐷 ↦ 𝐻)))
Theorem	gsummptrev 33389*	Revert ordering in a group sum. See also gsumwrev 19446. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ 𝐵)    &   ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝑁)) ∧ 𝑘 = (𝑁 − 𝑙)) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑋)) = (𝑀 Σg (𝑙 ∈ (0...𝑁) ↦ 𝑌)))
Theorem	gsummptp1 33390*	Reindex a zero-based sum as a one-base sum. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑙 ∈ (1...𝑁)) → 𝑌 ∈ 𝐵)    &   ⊢ (((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) ∧ 𝑙 = (𝑘 + 1)) → 𝑌 = 𝑋)    ⇒   ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0..^𝑁) ↦ 𝑋)) = (𝑅 Σg (𝑙 ∈ (1...𝑁) ↦ 𝑌)))
Theorem	gsummptfzsplitra 33391*	Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the right. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑁) → 𝑌 = 𝑋)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝑌)) = ((𝐺 Σg (𝑘 ∈ (𝑀..^𝑁) ↦ 𝑌)) + 𝑋))
Theorem	gsummptfzsplitla 33392*	Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the left. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑌 = 𝑋)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝑌)) = (𝑋 + (𝐺 Σg (𝑘 ∈ ((𝑀 + 1)...𝑁) ↦ 𝑌))))
Theorem	gsummptfsf1o 33393*	Re-index a finite group sum using a bijection. A version of gsummptf1o 20043 expressed using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ Ⅎ𝑥𝐻    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝑥 = 𝐸 → 𝐶 = 𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) finSupp 0 )    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐹)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐸 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐷 𝑥 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑦 ∈ 𝐷 ↦ 𝐻)))
Theorem	gsumfs2d 33394*	Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d 20052 using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝑊 ∈ CMnd)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
Theorem	gsumzresunsn 33395	Append an element to a finite group sum expressed as a function restriction. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (𝐹‘𝑋)    &   ⊢ (𝜑 → 𝐹:𝐶⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹 “ (𝐴 ∪ {𝑋})) ⊆ (𝑍‘(𝐹 “ (𝐴 ∪ {𝑋}))))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ∪ {𝑋}))) = ((𝐺 Σg (𝐹 ↾ 𝐴)) + 𝑌))
Theorem	gsumpart 33396*	Express a group sum as a double sum, grouping along a (possibly infinite) partition. (Contributed by Thierry Arnoux, 22-Jun-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶)))))
Theorem	gsumtp 33397*	Group sum of an unordered triple. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷)    &   ⊢ (𝑘 = 𝑂 → 𝐴 = 𝐸)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑁)    &   ⊢ (𝜑 → 𝑁 ≠ 𝑂)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑂)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁, 𝑂} ↦ 𝐴)) = ((𝐶 + 𝐷) + 𝐸))
Theorem	gsumzrsum 33398*	Relate a group sum on ℤring to a finite sum on the complex numbers. See also gsumfsum 21599. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (ℤring Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	gsummulgc2 33399*	A finite group sum multiplied by a constant. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ · = (.g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = (Σ𝑘 ∈ 𝐴 𝑋 · 𝑌))
Theorem	gsumhashmul 33400*	Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((♯‘(◡𝐹 “ {𝑥})) · 𝑥))))