P. 333 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33201-33300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pfxrn2 33201	The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14723. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ ran 𝑊)
Theorem	pfxrn3 33202	Express the range of a prefix of a word. Stronger version of pfxrn2 33201. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) = (𝑊 “ (0..^𝐿)))
Theorem	pfxf1 33203	Condition for a prefix to be injective. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝑆)    &   ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝑊)))    ⇒   ⊢ (𝜑 → (𝑊 prefix 𝐿):dom (𝑊 prefix 𝐿)–1-1→𝑆)
Theorem	s1f1 33204	Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ⟨“𝐼”⟩:dom ⟨“𝐼”⟩–1-1→𝐷)
Theorem	s2rnOLD 33205	Obsolete version of s2rn 15000 as of 1-Aug-2025. Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽”⟩ = {𝐼, 𝐽})
Theorem	s2f1 33206	Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    ⇒   ⊢ (𝜑 → ⟨“𝐼𝐽”⟩:dom ⟨“𝐼𝐽”⟩–1-1→𝐷)
Theorem	s3rnOLD 33207	Obsolete version of s2rn 15000 as of 1-Aug-2025. Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽𝐾”⟩ = {𝐼, 𝐽, 𝐾})
Theorem	s3f1 33208	Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ⟨“𝐼𝐽𝐾”⟩:dom ⟨“𝐼𝐽𝐾”⟩–1-1→𝐷)
Theorem	s3clhash 33209	Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.)
⊢ ⟨“𝐼𝐽𝐾”⟩ ∈ (◡♯ “ {3})
Theorem	ccatf1 33210	Conditions for a concatenation to be injective. (Contributed by Thierry Arnoux, 11-Dec-2023.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐴:dom 𝐴–1-1→𝑆)    &   ⊢ (𝜑 → 𝐵:dom 𝐵–1-1→𝑆)    &   ⊢ (𝜑 → (ran 𝐴 ∩ ran 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ++ 𝐵):dom (𝐴 ++ 𝐵)–1-1→𝑆)
Theorem	pfxlsw2ccat 33211	Reconstruct a word from its prefix and its last two symbols. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ 𝑁 = (♯‘𝑊)    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ ⟨“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”⟩))
Theorem	ccatws1f1o 33212	Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑁 = (♯‘𝑇)    &   ⊢ 𝐽 = (0..^(𝑁 + 1))    &   ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))    ⇒   ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩):𝐽–1-1-onto→𝐽)
Theorem	ccatws1f1olast 33213	Two ways to reorder symbols in a word 𝑊 according to permutation 𝑇, and add a last symbol 𝑋. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑁 = (♯‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))    ⇒   ⊢ (𝜑 → ((𝑊 ++ ⟨“𝑋”⟩) ∘ (𝑇 ++ ⟨“𝑁”⟩)) = ((𝑊 ∘ 𝑇) ++ ⟨“𝑋”⟩))
Theorem	wrdt2ind 33214*	Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)
Theorem	swrdrn2 33215	The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14690. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) ⊆ ran 𝑊)
Theorem	swrdrn3 33216	Express the range of a subword. Stronger version of swrdrn2 33215. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑊 “ (𝑀..^𝑁)))
Theorem	swrdf1 33217	Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝑊)))    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    ⇒   ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)–1-1→𝐷)
Theorem	swrdrndisj 33218	Condition for the range of two subwords of an injective word to be disjoint. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝑊)))    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → 𝑂 ∈ (𝑁...𝑃))    &   ⊢ (𝜑 → 𝑃 ∈ (𝑁...(♯‘𝑊)))    ⇒   ⊢ (𝜑 → (ran (𝑊 substr ⟨𝑀, 𝑁⟩) ∩ ran (𝑊 substr ⟨𝑂, 𝑃⟩)) = ∅)
21.3.8.1  Splicing words (substring replacement)
Theorem	splfv3 33219	Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.)
⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑅 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ (0..^((♯‘𝑆) − 𝑇)))    &   ⊢ (𝜑 → 𝐾 = (𝐹 + (♯‘𝑅)))    ⇒   ⊢ (𝜑 → ((𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)‘(𝑋 + 𝐾)) = (𝑆‘(𝑋 + 𝑇)))
21.3.8.2  Cyclic shift of words
Theorem	1cshid 33220	Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (♯‘𝑊) = 1) → (𝑊 cyclShift 𝑁) = 𝑊)
Theorem	cshw1s2 33221	Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ⟨“𝐵𝐴”⟩)
Theorem	cshwrnid 33222	Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) = ran 𝑊)
Theorem	cshf1o 33223	Condition for the cyclic shift to be a bijection. (Contributed by Thierry Arnoux, 4-Oct-2023.)
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁):dom 𝑊–1-1-onto→ran 𝑊)
21.3.9  Extensible Structures
21.3.9.1  Structure restriction operator
Theorem	ressplusf 33224	The group operation function +𝑓 of a structure's restriction is the operation function's restriction to the new base. (Contributed by Thierry Arnoux, 26-Mar-2017.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ ⨣ = (+g‘𝐺)    &   ⊢ ⨣ Fn (𝐵 × 𝐵)    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (+𝑓‘𝐻) = ( ⨣ ↾ (𝐴 × 𝐴))
Theorem	ressnm 33225	The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻))
Theorem	abvpropd2 33226	Weaker version of abvpropd 20916. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿))    &   ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿))    ⇒   ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿))
21.3.9.2  Posets
Theorem	ressprs 33227	The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset )
Theorem	posrasymb 33228	A poset ordering is asymmetric. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
Theorem	odutos 33229	Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset)
Theorem	tlt2 33230	In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋))
Theorem	tlt3 33231	In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋))
Theorem	trleile 33232	In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋))
Theorem	toslublem 33233*	Lemma for toslub 33234 and xrsclat 33272. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑))))
Theorem	toslub 33234	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 33235*	Lemma for tosglb 33236 and xrsclat 33272. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑))))
Theorem	tosglb 33236	Same theorem as toslub 33234, 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 33237	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 33238	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 33239	Extend class notation with monotone functions.
class Monot
Syntax	cmgc 33240	Extend class notation with the monotone Galois connection.
class MGalConn
Definition	df-mnt 33241*	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 33242*	Define monotone Galois connections. See mgcval 33248 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.)
⊢ MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))})
Theorem	mntoval 33243*	Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉Monot𝑊) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝑓‘𝑥) ≲ (𝑓‘𝑦))})
Theorem	ismnt 33244*	Express the statement "𝐹 is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 ∈ (𝑉Monot𝑊) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))))
Theorem	ismntd 33245	Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌))
Theorem	mntf 33246	A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ (𝑉Monot𝑊)) → 𝐹:𝐴⟶𝐵)
Theorem	mgcoval 33247*	Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉MGalConn𝑊) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))})
Theorem	mgcval 33248*	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 33249	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 33250	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 33251	An inequality for the kernel operator 𝐺 ∘ 𝐹. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ≤ (𝐺‘(𝐹‘𝑋)))
Theorem	mgccole2 33252	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 33253	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 33254	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 33255*	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 33256*	Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))    &   ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)    ⇒   ⊢ (𝜑 → 𝐹𝐻𝐺)
Theorem	dfmgc2 33257*	Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
Theorem	mgcmnt1d 33258	Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))
Theorem	mgcmnt2d 33259	Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
Theorem	mgccnv 33260	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 33261*	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 33262	Property of a Galois connection, lemma for mgcf1o 33264. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐹‘𝑋))) = (𝐹‘𝑋))
Theorem	mgcf1olem2 33263	Property of a Galois connection, lemma for mgcf1o 33264. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌))
Theorem	mgcf1o 33264	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 33265	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 33266	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 33267	The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13275 and df-xrs 17556), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ 0 = (0g‘ℝ*𝑠)
Theorem	xrslt 33268	The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ < = (lt‘ℝ*𝑠)
Theorem	xrsinvgval 33269	The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13275 and df-xrs 17556), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵)
Theorem	xrsmulgzz 33270	The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))
Theorem	xrstos 33271	The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ Toset
Theorem	xrsclat 33272	The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ CLat
Theorem	xrsp0 33273	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 33274	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 33275	The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0mulgnn0 33276	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 33277	Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xrge0addgt0 33278	The sum of nonnegative and positive numbers is positive. See addgtge0 11702. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵))
Theorem	xrge0adddir 33279	Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)))
Theorem	xrge0adddi 33280	Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵)))
Theorem	xrge0npcan 33281	Extended nonnegative real version of npcan 11466. (Contributed by Thierry Arnoux, 9-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
Theorem	fsumrp0cl 33282*	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 33283	Closure of the operation of a monoid. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	mndassd 33284	A monoid operation is associative. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	mndlrinv 33285	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 33286*	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 33287*	If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐹 is injective. See also grplactf1o 19110. 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 33288*	An element 𝑋 of a monoid 𝐸 is left-invertible iff its left-translation 𝐹 is surjective. See also grplactf1o 19110. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑋 + 𝑦) = 0 ))
Theorem	mndractf1 33289*	If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐺 is injective. See also grplactf1o 19110. 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 33290*	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 33291*	An element 𝑋 of a monoid 𝐸 is invertible iff its left-translation 𝐹 is bijective. See also grplactf1o 19110. 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 33292*	An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33291. 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 33293	Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	cmn246135 33294	Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33530. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑌 + (𝑈 + 𝑊)) + (𝑋 + (𝑍 + 𝑉))))
Theorem	cmn145236 33295	Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33530. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑋 + (𝑈 + 𝑉)) + (𝑌 + (𝑍 + 𝑊))))
21.3.10.2  Monoids Homomorphisms
Theorem	abliso 33296	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 33297	A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	mhmimasplusg 33298	Value of the operation of the surjective image. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑊 = (𝐹 “s 𝑉)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ 𝐶 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐵–onto→𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉 MndHom 𝑊))    &   ⊢ + = (+g‘𝑉)    &   ⊢ ⨣ = (+g‘𝑊)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)) = (𝐹‘(𝑋 + 𝑌)))
Theorem	lmhmimasvsca 33299	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 33300	The identity element of a group belongs to the group. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 0 ∈ 𝐵)