P. 331 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33001-33100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wrdpmcl 33001	Closure of a word with permuted symbols. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝐽 = (0..^(♯‘𝑊))    &   ⊢ (𝜑 → 𝐸:𝐽–1-1-onto→𝐽)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → (𝑊 ∘ 𝐸) ∈ Word 𝑆)
Theorem	pfx1s2 33002	The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ prefix 1) = ⟨“𝐴”⟩)
Theorem	pfxrn2 33003	The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14613. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ ran 𝑊)
Theorem	pfxrn3 33004	Express the range of a prefix of a word. Stronger version of pfxrn2 33003. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) = (𝑊 “ (0..^𝐿)))
Theorem	pfxf1 33005	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 33006	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 33007	Obsolete version of s2rn 14890 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 33008	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 33009	Obsolete version of s2rn 14890 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 33010	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 33011	Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.)
⊢ ⟨“𝐼𝐽𝐾”⟩ ∈ (◡♯ “ {3})
Theorem	ccatf1 33012	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 33013	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 33014	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 33015	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 33016*	Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)
Theorem	swrdrn2 33017	The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14580. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) ⊆ ran 𝑊)
Theorem	swrdrn3 33018	Express the range of a subword. Stronger version of swrdrn2 33017. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑊 “ (𝑀..^𝑁)))
Theorem	swrdf1 33019	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 33020	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 33021	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 33022	Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (♯‘𝑊) = 1) → (𝑊 cyclShift 𝑁) = 𝑊)
Theorem	cshw1s2 33023	Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ⟨“𝐵𝐴”⟩)
Theorem	cshwrnid 33024	Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) = ran 𝑊)
Theorem	cshf1o 33025	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 33026	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 33027	The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻))
Theorem	abvpropd2 33028	Weaker version of abvpropd 20772. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿))    &   ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿))    ⇒   ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿))
21.3.9.2  Posets
Theorem	ressprs 33029	The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset )
Theorem	posrasymb 33030	A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
Theorem	odutos 33031	Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset)
Theorem	tlt2 33032	In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋))
Theorem	tlt3 33033	In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋))
Theorem	trleile 33034	In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋))
Theorem	toslublem 33035*	Lemma for toslub 33036 and xrsclat 33074. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑))))
Theorem	toslub 33036	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 33037*	Lemma for tosglb 33038 and xrsclat 33074. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑))))
Theorem	tosglb 33038	Same theorem as toslub 33036, 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 33039	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 33040	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 33041	Extend class notation with monotone functions.
class Monot
Syntax	cmgc 33042	Extend class notation with the monotone Galois connection.
class MGalConn
Definition	df-mnt 33043*	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 33044*	Define monotone Galois connections. See mgcval 33050 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.)
⊢ MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))})
Theorem	mntoval 33045*	Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉Monot𝑊) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝑓‘𝑥) ≲ (𝑓‘𝑦))})
Theorem	ismnt 33046*	Express the statement "𝐹 is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 ∈ (𝑉Monot𝑊) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))))
Theorem	ismntd 33047	Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌))
Theorem	mntf 33048	A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ (𝑉Monot𝑊)) → 𝐹:𝐴⟶𝐵)
Theorem	mgcoval 33049*	Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉MGalConn𝑊) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))})
Theorem	mgcval 33050*	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 33051	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 33052	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 33053	An inequality for the kernel operator 𝐺 ∘ 𝐹. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ≤ (𝐺‘(𝐹‘𝑋)))
Theorem	mgccole2 33054	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 33055	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 33056	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 33057*	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 33058*	Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))    &   ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)    ⇒   ⊢ (𝜑 → 𝐹𝐻𝐺)
Theorem	dfmgc2 33059*	Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
Theorem	mgcmnt1d 33060	Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))
Theorem	mgcmnt2d 33061	Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
Theorem	mgccnv 33062	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 33063*	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 33064	Property of a Galois connection, lemma for mgcf1o 33066. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐹‘𝑋))) = (𝐹‘𝑋))
Theorem	mgcf1olem2 33065	Property of a Galois connection, lemma for mgcf1o 33066. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌))
Theorem	mgcf1o 33066	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 33067	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 33068	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 33069	The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13168 and df-xrs 17427), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ 0 = (0g‘ℝ*𝑠)
Theorem	xrslt 33070	The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ < = (lt‘ℝ*𝑠)
Theorem	xrsinvgval 33071	The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13168 and df-xrs 17427), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵)
Theorem	xrsmulgzz 33072	The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))
Theorem	xrstos 33073	The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ Toset
Theorem	xrsclat 33074	The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ CLat
Theorem	xrsp0 33075	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 33076	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 33077	The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0mulgnn0 33078	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 33079	Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xrge0addgt0 33080	The sum of nonnegative and positive numbers is positive. See addgtge0 11629. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵))
Theorem	xrge0adddir 33081	Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)))
Theorem	xrge0adddi 33082	Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵)))
Theorem	xrge0npcan 33083	Extended nonnegative real version of npcan 11393. (Contributed by Thierry Arnoux, 9-Jun-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
Theorem	fsumrp0cl 33084*	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 33085	Closure of the operation of a monoid. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	mndassd 33086	A monoid operation is associative. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	mndlrinv 33087	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 33088*	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 33089*	If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐹 is injective. See also grplactf1o 18978. 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 33090*	An element 𝑋 of a monoid 𝐸 is left-invertible iff its left-translation 𝐹 is surjective. See also grplactf1o 18978. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑋 + 𝑦) = 0 ))
Theorem	mndractf1 33091*	If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐺 is injective. See also grplactf1o 18978. 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 33092*	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 33093*	An element 𝑋 of a monoid 𝐸 is invertible iff its left-translation 𝐹 is bijective. See also grplactf1o 18978. 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 33094*	An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33093. 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 33095	Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	cmn246135 33096	Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33331. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑌 + (𝑈 + 𝑊)) + (𝑋 + (𝑍 + 𝑉))))
Theorem	cmn145236 33097	Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33331. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑋 + (𝑈 + 𝑉)) + (𝑌 + (𝑍 + 𝑊))))
Theorem	submcld 33098	Submonoids are closed under the monoid operation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑆)
21.3.10.2  Monoids Homomorphisms
Theorem	abliso 33099	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 33100	A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))