P. 330 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32901-33000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tosglb 32901	Same theorem as toslub 32899, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < ))
21.3.9.4  Complete lattices
Theorem	clatp0cl 32902	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 32903	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.5  Order Theory
Syntax	cmnt 32904	Extend class notation with monotone functions.
class Monot
Syntax	cmgc 32905	Extend class notation with the monotone Galois connection.
class MGalConn
Definition	df-mnt 32906*	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 32907*	Define monotone Galois connections. See mgcval 32913 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.)
⊢ MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))})
Theorem	mntoval 32908*	Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉Monot𝑊) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝑓‘𝑥) ≲ (𝑓‘𝑦))})
Theorem	ismnt 32909*	Express the statement "𝐹 is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 ∈ (𝑉Monot𝑊) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))))
Theorem	ismntd 32910	Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌))
Theorem	mntf 32911	A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ (𝑉Monot𝑊)) → 𝐹:𝐴⟶𝐵)
Theorem	mgcoval 32912*	Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉MGalConn𝑊) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))})
Theorem	mgcval 32913*	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 32914	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 32915	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 32916	An inequality for the kernel operator 𝐺 ∘ 𝐹. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ≤ (𝐺‘(𝐹‘𝑋)))
Theorem	mgccole2 32917	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 32918	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 32919	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 32920*	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 32921*	Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))    &   ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)    ⇒   ⊢ (𝜑 → 𝐹𝐻𝐺)
Theorem	dfmgc2 32922*	Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
Theorem	mgcmnt1d 32923	Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))
Theorem	mgcmnt2d 32924	Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
Theorem	mgccnv 32925	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 32926*	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 32927	Property of a Galois connection, lemma for mgcf1o 32929. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐹‘𝑋))) = (𝐹‘𝑋))
Theorem	mgcf1olem2 32928	Property of a Galois connection, lemma for mgcf1o 32929. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌))
Theorem	mgcf1o 32929	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.6  Chains
Syntax	cchn 32930	Extend class notation with the class of (finite) chains.
class ( < Chain𝐴)
Definition	df-chn 32931*	Define the class of (finite) chains. A chain is defined to be a sequence of objects, where each object is less than the next one in the sequence. The term "chain" is usually used in order theory. In the context of algebra, chains are often called "towers", for example for fields, or "series", for example for subgroup or subnormal series. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
Theorem	ischn 32932*	Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
Theorem	chnwrd 32933	A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
Theorem	chnltm1 32934	Basic property of a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (dom 𝐶 ∖ {0}))    ⇒   ⊢ (𝜑 → (𝐶‘(𝑁 − 1)) < (𝐶‘𝑁))
Theorem	pfxchn 32935	A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶 prefix 𝐿) ∈ ( < Chain𝐴))
Theorem	s1chn 32936	A singleton word is always a chain. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ⟨“𝑋”⟩ ∈ ( < Chain𝐴))
Theorem	chnind 32937*	Induction over a chain. See nnind 12256 for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	chnub 32938	In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^((♯‘𝐶) − 1)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (lastS‘𝐶))
Theorem	chnlt 32939	Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝐽))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (𝐶‘𝐽))
Theorem	chnso 32940	A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → < Or ran 𝐶)
Theorem	chnccats1 32941	Extend a chain with a single element. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → (𝑇 = ∅ ∨ (lastS‘𝑇) < 𝑋))    ⇒   ⊢ (𝜑 → (𝑇 ++ ⟨“𝑋”⟩) ∈ ( < Chain𝐴))
21.3.9.7  Extended reals Structure - misc additions
Axiom	ax-xrssca 32942	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 32943	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 32944	The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13263 and df-xrs 17514), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ 0 = (0g‘ℝ*𝑠)
Theorem	xrslt 32945	The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ < = (lt‘ℝ*𝑠)
Theorem	xrsinvgval 32946	The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13263 and df-xrs 17514), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵)
Theorem	xrsmulgzz 32947	The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))
Theorem	xrstos 32948	The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ Toset
Theorem	xrsclat 32949	The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ CLat
Theorem	xrsp0 32950	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 32951	The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
⊢ +∞ = (1.‘ℝ*𝑠)
21.3.9.8  The extended nonnegative real numbers commutative monoid
Theorem	xrge0base 32952	The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge00 32953	The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0plusg 32954	The additive law of the extended nonnegative real numbers monoid is the addition in the extended real numbers. (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ +𝑒 = (+g‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0le 32955	The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.)
⊢ ≤ = (le‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0mulgnn0 32956	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 32957	Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xrge0addgt0 32958	The sum of nonnegative and positive numbers is positive. See addgtge0 11723. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵))
Theorem	xrge0adddir 32959	Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)))
Theorem	xrge0adddi 32960	Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵)))
Theorem	xrge0npcan 32961	Extended nonnegative real version of npcan 11489. (Contributed by Thierry Arnoux, 9-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
Theorem	fsumrp0cl 32962*	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 32963	Closure of the operation of a monoid. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	mndassd 32964	A monoid operation is associative. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	mndlrinv 32965	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 32966*	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 32967*	If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐹 is injective. See also grplactf1o 19025. 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 32968*	An element 𝑋 of a monoid 𝐸 is left-invertible iff its left-translation 𝐹 is surjective. See also grplactf1o 19025. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑋 + 𝑦) = 0 ))
Theorem	mndractf1 32969*	If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐺 is injective. See also grplactf1o 19025. 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 32970*	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 32971*	An element 𝑋 of a monoid 𝐸 is invertible iff its left-translation 𝐹 is bijective. See also grplactf1o 19025. 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 32972*	An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 32971. 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 32973	Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	cmn246135 32974	Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33209. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑌 + (𝑈 + 𝑊)) + (𝑋 + (𝑍 + 𝑉))))
Theorem	cmn145236 32975	Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33209. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑋 + (𝑈 + 𝑉)) + (𝑌 + (𝑍 + 𝑊))))
Theorem	submcld 32976	Submonoids are closed under the monoid operation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑆)
21.3.10.2  Monoids Homomorphisms
Theorem	abliso 32977	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 32978	A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	mhmimasplusg 32979	Value of the operation of the surjective image. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑊 = (𝐹 “s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ 𝐶 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐵–onto→𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉 MndHom 𝑊))    &   ⊢ + = (+g‘𝑉)    &   ⊢ ⨣ = (+g‘𝑊)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)) = (𝐹‘(𝑋 + 𝑌)))
Theorem	lmhmimasvsca 32980	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	grpsubcld 32981	Closure of group subtraction. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝐵)
Theorem	subgcld 32982	A subgroup is closed under group operation. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	subgsubcld 32983	A subgroup is closed under group subtraction. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑆)
Theorem	subgmulgcld 32984	Closure of the group multiple within a subgroup. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))    &   ⊢ (𝜑 → 𝑍 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑍 · 𝐴) ∈ 𝑆)
Theorem	ressmulgnn0d 32985	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  Finitely supported group sums - misc additions
Theorem	gsumsubg 32986	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 32987	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 32988*	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 32989*	Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19951. (Contributed by Thierry Arnoux, 27-Apr-2020.)
⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑊 ∈ CMnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))))
Theorem	lmodvslmhm 32990*	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 32991*	Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 20274, 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 32992*	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 32993*	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	gsummptfsf1o 32994*	Re-index a finite group sum using a bijection. A version of gsummptf1o 19942 expressed using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ Ⅎ𝑥𝐻    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝑥 = 𝐸 → 𝐶 = 𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) finSupp 0 )    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐹)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐸 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐷 𝑥 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑦 ∈ 𝐷 ↦ 𝐻)))
Theorem	gsumfs2d 32995*	Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d 19951 using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝑊 ∈ CMnd)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
Theorem	gsumzresunsn 32996	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 32997*	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 32998*	Group sum of an unordered triple. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷)    &   ⊢ (𝑘 = 𝑂 → 𝐴 = 𝐸)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑁)    &   ⊢ (𝜑 → 𝑁 ≠ 𝑂)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑂)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁, 𝑂} ↦ 𝐴)) = ((𝐶 + 𝐷) + 𝐸))
Theorem	gsumzrsum 32999*	Relate a group sum on ℤring to a finite sum on the complex numbers. See also gsumfsum 21400. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (ℤring Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	gsummulgc2 33000*	A finite group sum multiplied by a constant. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ · = (.g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = (Σ𝑘 ∈ 𝐴 𝑋 · 𝑌))