HomeTheorem List (p. 336 of 510)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 336 of 510) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-31499) |
Hilbert Space Explorer
(31500-33022) |
Users' Mathboxes
(33023-50931) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cshwrnid 33501 | Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
| ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) = ran 𝑊) | ||
| Theorem | cshf1o 33502 | 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 𝑊) | ||
| Theorem | ressplusf 33503 | 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 33504 | The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻)) | ||
| Theorem | abvpropd2 33505 | Weaker version of abvpropd 21069. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
| ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿)) & ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿)) ⇒ ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿)) | ||
| Theorem | ressprs 33506 | The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset ) | ||
| Theorem | posrasymb 33507 | A poset ordering is asymmetric. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
| Theorem | odutos 33508 | Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset) | ||
| Theorem | tlt2 33509 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋)) | ||
| Theorem | tlt3 33510 | In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋)) | ||
| Theorem | trleile 33511 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋)) | ||
| Theorem | toslublem 33512* | Lemma for toslub 33513 and xrsclat 33551. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑)))) | ||
| Theorem | toslub 33513 | 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 33514* | Lemma for tosglb 33515 and xrsclat 33551. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑)))) | ||
| Theorem | tosglb 33515 | Same theorem as toslub 33513, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < )) | ||
| Theorem | clatp0cl 33516 | 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 33517 | The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 1 = (1.‘𝑊) ⇒ ⊢ (𝑊 ∈ CLat → 1 ∈ 𝐵) | ||
| Syntax | cmnt 33518 | Extend class notation with monotone functions. |
| class Monot | ||
| Syntax | cmgc 33519 | Extend class notation with the monotone Galois connection. |
| class MGalConn | ||
| Definition | df-mnt 33520* | 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 33521* | Define monotone Galois connections. See mgcval 33527 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.) |
| ⊢ MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))}) | ||
| Theorem | mntoval 33522* | Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
| ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉Monot𝑊) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝑓‘𝑥) ≲ (𝑓‘𝑦))}) | ||
| Theorem | ismnt 33523* | Express the statement "𝐹 is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.) |
| ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 ∈ (𝑉Monot𝑊) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦))))) | ||
| Theorem | ismntd 33524 | Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
| ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ 𝐶) & ⊢ (𝜑 → 𝑊 ∈ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌)) | ||
| Theorem | mntf 33525 | A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
| ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ (𝑉Monot𝑊)) → 𝐹:𝐴⟶𝐵) | ||
| Theorem | mgcoval 33526* | Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
| ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉MGalConn𝑊) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))}) | ||
| Theorem | mgcval 33527* |
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 33528 | 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 33529 | 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 33530 | An inequality for the kernel operator 𝐺 ∘ 𝐹. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
| ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑋 ≤ (𝐺‘(𝐹‘𝑋))) | ||
| Theorem | mgccole2 33531 | 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 33532 | 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 33533 | 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 33534* | 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 33535* | Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
| ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦))) & ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥))) & ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢) ⇒ ⊢ (𝜑 → 𝐹𝐻𝐺) | ||
| Theorem | dfmgc2 33536* | Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
| ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥))))))) | ||
| Theorem | mgcmnt1d 33537 | Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹𝐻𝐺) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊)) | ||
| Theorem | mgcmnt2d 33538 | Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹𝐻𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉)) | ||
| Theorem | mgccnv 33539 | 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 33540* | 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 33541 | Property of a Galois connection, lemma for mgcf1o 33543. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ Poset) & ⊢ (𝜑 → 𝑊 ∈ Poset) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐹‘𝑋))) = (𝐹‘𝑋)) | ||
| Theorem | mgcf1olem2 33542 | Property of a Galois connection, lemma for mgcf1o 33543. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ Poset) & ⊢ (𝜑 → 𝑊 ∈ Poset) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌)) | ||
| Theorem | mgcf1o 33543 | 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 𝐹)) | ||
| Axiom | ax-xrssca 33544 | 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 33545 | 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 33546 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13357 and df-xrs 17651), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
| ⊢ 0 = (0g‘ℝ*𝑠) | ||
| Theorem | xrslt 33547 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ < = (lt‘ℝ*𝑠) | ||
| Theorem | xrsinvgval 33548 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13357 and df-xrs 17651), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
| ⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵) | ||
| Theorem | xrsmulgzz 33549 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) | ||
| Theorem | xrstos 33550 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
| ⊢ ℝ*𝑠 ∈ Toset | ||
| Theorem | xrsclat 33551 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
| ⊢ ℝ*𝑠 ∈ CLat | ||
| Theorem | xrsp0 33552 | 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 33553 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
| ⊢ +∞ = (1.‘ℝ*𝑠) | ||
| Theorem | xrge00 33554 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
| ⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge0mulgnn0 33555 | 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 33556 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
| Theorem | xrge0addgt0 33557 | The sum of nonnegative and positive numbers is positive. See addgtge0 11782. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
| ⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵)) | ||
| Theorem | xrge0adddir 33558 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
| Theorem | xrge0adddi 33559 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵))) | ||
| Theorem | xrge0npcan 33560 | Extended nonnegative real version of npcan 11544. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
| Theorem | fsumrp0cl 33561* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
| Theorem | mndcld 33562 | Closure of the operation of a monoid. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) | ||
| Theorem | mndassd 33563 | A monoid operation is associative. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
| Theorem | mndlrinv 33564 | 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 33565* | 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 33566* | If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐹 is injective. See also grplactf1o 19231. 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 33567* | An element 𝑋 of a monoid 𝐸 is left-invertible iff its left-translation 𝐹 is surjective. See also grplactf1o 19231. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑋 + 𝑦) = 0 )) | ||
| Theorem | mndractf1 33568* | If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐺 is injective. See also grplactf1o 19231. 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 33569* | 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 33570* | An element 𝑋 of a monoid 𝐸 is invertible iff its left-translation 𝐹 is bijective. See also grplactf1o 19231. 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 33571* | An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33570. 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 33572 | Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
| Theorem | cmn246135 33573 | Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33809. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑌 + (𝑈 + 𝑊)) + (𝑋 + (𝑍 + 𝑉)))) | ||
| Theorem | cmn145236 33574 | Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33809. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑋 + (𝑈 + 𝑉)) + (𝑌 + (𝑍 + 𝑊)))) | ||
| Theorem | abliso 33575 | 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 33576 | A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
| Theorem | mhmimasplusg 33577 | Value of the operation of the surjective image. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑊 = (𝐹 “s 𝑉) & ⊢ 𝐵 = (Base‘𝑉) & ⊢ 𝐶 = (Base‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐵–onto→𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑉 MndHom 𝑊)) & ⊢ + = (+g‘𝑉) & ⊢ ⨣ = (+g‘𝑊) ⇒ ⊢ (𝜑 → ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)) = (𝐹‘(𝑋 + 𝑌))) | ||
| Theorem | lmhmimasvsca 33578 | 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‘𝑉)) ⇒ ⊢ (𝜑 → (𝑋 × (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) | ||
| Theorem | grpidcld 33579 | The identity element of a group belongs to the group. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 0 ∈ 𝐵) | ||
| Theorem | grpinvinvd 33580 | Double inverse law for groups. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁‘(𝑁‘𝑋)) = 𝑋) | ||
| Theorem | grpsubcld 33581 | Closure of group subtraction. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝐵) | ||
| Theorem | subgsubcld 33582 | A subgroup is closed under group subtraction. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑆) | ||
| Theorem | subgmulgcld 33583 | Closure of the group multiple within a subgroup. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) & ⊢ (𝜑 → 𝑍 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑍 · 𝐴) ∈ 𝑆) | ||
| Theorem | ressmulgnn0d 33584 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
| ⊢ (𝜑 → (𝐺 ↾s 𝐴) = 𝐻) & ⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) & ⊢ (𝜑 → 𝐴 ⊆ (Base‘𝐺)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑁(.g‘𝐻)𝑋) = (𝑁(.g‘𝐺)𝑋)) | ||
| Theorem | ablcomd 33585 | An abelian group operation is commutative, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | gsumsubg 33586 | 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 33587 | 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 33588* | 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 33589* | Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 20163. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
| ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑦𝜑 & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) | ||
| Theorem | lmodvslmhm 33590* | 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 33591* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 20522, 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 33592* | 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 33593* | 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 33594* | 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 33595* | 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 33596* | Revert ordering in a group sum. See also gsumwrev 19557. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ 𝐵) & ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝑁)) ∧ 𝑘 = (𝑁 − 𝑙)) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑋)) = (𝑀 Σg (𝑙 ∈ (0...𝑁) ↦ 𝑌))) | ||
| Theorem | gsummptp1 33597* | 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 33598* | 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 33599* | 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 33600* | Re-index a finite group sum using a bijection. A version of gsummptf1o 20154 expressed using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ Ⅎ𝑥𝐻 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝑥 = 𝐸 → 𝐶 = 𝐻) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) finSupp 0 ) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐹) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐸 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐷 𝑥 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑦 ∈ 𝐷 ↦ 𝐻))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |