Home | Metamath
Proof Explorer Theorem List (p. 317 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wrdt2ind 31601* | Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ ++ β¨βππββ©) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ ((π¦ β Word π΅ β§ π β π΅ β§ π β π΅) β (π β π)) β β’ ((π΄ β Word π΅ β§ 2 β₯ (β―βπ΄)) β π) | ||
Theorem | swrdrn2 31602 | The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14471. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
β’ ((π β Word π β§ π β (0...π) β§ π β (0...(β―βπ))) β ran (π substr β¨π, πβ©) β ran π) | ||
Theorem | swrdrn3 31603 | Express the range of a subword. Stronger version of swrdrn2 31602. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
β’ ((π β Word π β§ π β (0...π) β§ π β (0...(β―βπ))) β ran (π substr β¨π, πβ©) = (π β (π..^π))) | ||
Theorem | swrdf1 31604 | 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 31605 | 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 β¨π, πβ©)) = β ) | ||
Theorem | splfv3 31606 | Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
β’ (π β π β Word π΄) & β’ (π β πΉ β (0...π)) & β’ (π β π β (0...(β―βπ))) & β’ (π β π β Word π΄) & β’ (π β π β (0..^((β―βπ) β π))) & β’ (π β πΎ = (πΉ + (β―βπ ))) β β’ (π β ((π splice β¨πΉ, π, π β©)β(π + πΎ)) = (πβ(π + π))) | ||
Theorem | 1cshid 31607 | Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
β’ ((π β Word π β§ π β β€ β§ (β―βπ) = 1) β (π cyclShift π) = π) | ||
Theorem | cshw1s2 31608 | Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (β¨βπ΄π΅ββ© cyclShift 1) = β¨βπ΅π΄ββ©) | ||
Theorem | cshwrnid 31609 | Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ ((π β Word π β§ π β β€) β ran (π cyclShift π) = ran π) | ||
Theorem | cshf1o 31610 | 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 31611 | 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 31612 | The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
β’ π» = (πΊ βΎs π΄) & β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (normβπΊ) β β’ ((πΊ β Mnd β§ 0 β π΄ β§ π΄ β π΅) β (π βΎ π΄) = (normβπ»)) | ||
Theorem | abvpropd2 31613 | Weaker version of abvpropd 20224. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (+gβπΎ) = (+gβπΏ)) & β’ (π β (.rβπΎ) = (.rβπΏ)) β β’ (π β (AbsValβπΎ) = (AbsValβπΏ)) | ||
Theorem | oppgle 31614 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π = (oppgβπ ) & β’ β€ = (leβπ ) β β’ β€ = (leβπ) | ||
Theorem | oppgleOLD 31615 | Obsolete version of oppgle 31614 as of 27-Oct-2024. less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (oppgβπ ) & β’ β€ = (leβπ ) β β’ β€ = (leβπ) | ||
Theorem | oppglt 31616 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π = (oppgβπ ) & β’ < = (ltβπ ) β β’ (π β π β < = (ltβπ)) | ||
Theorem | ressprs 31617 | The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
β’ π΅ = (BaseβπΎ) β β’ ((πΎ β Proset β§ π΄ β π΅) β (πΎ βΎs π΄) β Proset ) | ||
Theorem | oduprs 31618 | Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
β’ π· = (ODualβπΎ) β β’ (πΎ β Proset β π· β Proset ) | ||
Theorem | posrasymb 31619 | A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β ((π β€ π β§ π β€ π) β π = π)) | ||
Theorem | resspos 31620 | The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ ((πΉ β Poset β§ π΄ β π) β (πΉ βΎs π΄) β Poset) | ||
Theorem | resstos 31621 | The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ ((πΉ β Toset β§ π΄ β π) β (πΉ βΎs π΄) β Toset) | ||
Theorem | odutos 31622 | Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
β’ π· = (ODualβπΎ) β β’ (πΎ β Toset β π· β Toset) | ||
Theorem | tlt2 31623 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π β€ π β¨ π < π)) | ||
Theorem | tlt3 31624 | In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π = π β¨ π < π β¨ π < π)) | ||
Theorem | trleile 31625 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π β€ π β¨ π β€ π)) | ||
Theorem | toslublem 31626* | Lemma for toslub 31627 and xrsclat 31665. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ (π β πΎ β Toset) & β’ (π β π΄ β π΅) & β’ β€ = (leβπΎ) β β’ ((π β§ π β π΅) β ((βπ β π΄ π β€ π β§ βπ β π΅ (βπ β π΄ π β€ π β π β€ π)) β (βπ β π΄ Β¬ π < π β§ βπ β π΅ (π < π β βπ β π΄ π < π)))) | ||
Theorem | toslub 31627 | 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 31628* | Lemma for tosglb 31629 and xrsclat 31665. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ (π β πΎ β Toset) & β’ (π β π΄ β π΅) & β’ β€ = (leβπΎ) β β’ ((π β§ π β π΅) β ((βπ β π΄ π β€ π β§ βπ β π΅ (βπ β π΄ π β€ π β π β€ π)) β (βπ β π΄ Β¬ πβ‘ < π β§ βπ β π΅ (πβ‘ < π β βπ β π΄ πβ‘ < π)))) | ||
Theorem | tosglb 31629 | Same theorem as toslub 31627, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ (π β πΎ β Toset) & β’ (π β π΄ β π΅) β β’ (π β ((glbβπΎ)βπ΄) = inf(π΄, π΅, < )) | ||
Theorem | clatp0cl 31630 | 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 31631 | 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 31632 | Extend class notation with monotone functions. |
class Monot | ||
Syntax | cmgc 31633 | Extend class notation with the monotone Galois connection. |
class MGalConn | ||
Definition | df-mnt 31634* | 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 31635* | Define monotone Galois connections. See mgcval 31641 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.) |
β’ MGalConn = (π£ β V, π€ β V β¦ β¦(Baseβπ£) / πβ¦β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))}) | ||
Theorem | mntoval 31636* | Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) β β’ ((π β π β§ π β π) β (πMonotπ) = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))}) | ||
Theorem | ismnt 31637* | Express the statement "πΉ is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) β β’ ((π β π β§ π β π) β (πΉ β (πMonotπ) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))))) | ||
Theorem | ismntd 31638 | Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β πΆ) & β’ (π β π β π·) & β’ (π β πΉ β (πMonotπ)) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β€ π) β β’ (π β (πΉβπ) β² (πΉβπ)) | ||
Theorem | mntf 31639 | A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) β β’ ((π β π β§ π β π β§ πΉ β (πMonotπ)) β πΉ:π΄βΆπ΅) | ||
Theorem | mgcoval 31640* | Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) β β’ ((π β π β§ π β π) β (πMGalConnπ) = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) | ||
Theorem | mgcval 31641* |
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 31642 | 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 31643 | 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 31644 | An inequality for the kernel operator πΊ β πΉ. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΄) β β’ (π β π β€ (πΊβ(πΉβπ))) | ||
Theorem | mgccole2 31645 | 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 31646 | 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 31647 | 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 31648* | 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 31649* | Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΊ:π΅βΆπ΄) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) & β’ (π β βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) & β’ ((π β§ π₯ β π΄) β π₯ β€ (πΊβ(πΉβπ₯))) & β’ ((π β§ π’ β π΅) β (πΉβ(πΊβπ’)) β² π’) β β’ (π β πΉπ»πΊ) | ||
Theorem | dfmgc2 31650* | Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) β β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))))))) | ||
Theorem | mgcmnt1d 31651 | Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) β β’ (π β πΉ β (πMonotπ)) | ||
Theorem | mgcmnt2d 31652 | Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) β β’ (π β πΊ β (πMonotπ)) | ||
Theorem | mgccnv 31653 | 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 31654* | 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 31655 | Property of a Galois connection, lemma for mgcf1o 31657. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β Poset) & β’ (π β π β Poset) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΄) β β’ (π β (πΉβ(πΊβ(πΉβπ))) = (πΉβπ)) | ||
Theorem | mgcf1olem2 31656 | Property of a Galois connection, lemma for mgcf1o 31657. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β Poset) & β’ (π β π β Poset) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΅) β β’ (π β (πΊβ(πΉβ(πΊβπ))) = (πΊβπ)) | ||
Theorem | mgcf1o 31657 | 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 31658 | 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 31659 | 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 31660 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13096 and df-xrs 17318), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
β’ 0 = (0gββ*π ) | ||
Theorem | xrslt 31661 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ < = (ltββ*π ) | ||
Theorem | xrsinvgval 31662 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13096 and df-xrs 17318), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
β’ (π΅ β β* β ((invgββ*π )βπ΅) = -ππ΅) | ||
Theorem | xrsmulgzz 31663 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
β’ ((π΄ β β€ β§ π΅ β β*) β (π΄(.gββ*π )π΅) = (π΄ Β·e π΅)) | ||
Theorem | xrstos 31664 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
β’ β*π β Toset | ||
Theorem | xrsclat 31665 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
β’ β*π β CLat | ||
Theorem | xrsp0 31666 | 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 31667 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
β’ +β = (1.ββ*π ) | ||
Theorem | ressmulgnn 31668 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017.) |
β’ π» = (πΊ βΎs π΄) & β’ π΄ β (BaseβπΊ) & β’ β = (.gβπΊ) & β’ πΌ = (invgβπΊ) β β’ ((π β β β§ π β π΄) β (π(.gβπ»)π) = (π β π)) | ||
Theorem | ressmulgnn0 31669 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
β’ π» = (πΊ βΎs π΄) & β’ π΄ β (BaseβπΊ) & β’ β = (.gβπΊ) & β’ πΌ = (invgβπΊ) & β’ (0gβπΊ) = (0gβπ») β β’ ((π β β0 β§ π β π΄) β (π(.gβπ»)π) = (π β π)) | ||
Theorem | xrge0base 31670 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ (0[,]+β) = (Baseβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge00 31671 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ 0 = (0gβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge0plusg 31672 | 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 31673 | The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.) |
β’ β€ = (leβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge0mulgnn0 31674 | 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 31675 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β ((π΄ +π π΅) +π πΆ) = (π΄ +π (π΅ +π πΆ))) | ||
Theorem | xrge0addgt0 31676 | The sum of nonnegative and positive numbers is positive. See addgtge0 11576. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
β’ (((π΄ β (0[,]+β) β§ π΅ β (0[,]+β)) β§ 0 < π΄) β 0 < (π΄ +π π΅)) | ||
Theorem | xrge0adddir 31677 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β ((π΄ +π π΅) Β·e πΆ) = ((π΄ Β·e πΆ) +π (π΅ Β·e πΆ))) | ||
Theorem | xrge0adddi 31678 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β (πΆ Β·e (π΄ +π π΅)) = ((πΆ Β·e π΄) +π (πΆ Β·e π΅))) | ||
Theorem | xrge0npcan 31679 | Extended nonnegative real version of npcan 11343. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ π΅ β€ π΄) β ((π΄ +π -ππ΅) +π π΅) = π΄) | ||
Theorem | fsumrp0cl 31680* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β Ξ£π β π΄ π΅ β (0[,)+β)) | ||
Theorem | abliso 31681 | The image of an Abelian group by a group isomorphism is also Abelian. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
β’ ((π β Abel β§ πΉ β (π GrpIso π)) β π β Abel) | ||
Theorem | gsumsubg 31682 | 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 31683 | 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 31684* | 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 31685* | Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19678. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
β’ β²π§πΆ & β’ β²π¦π & β’ π΅ = (Baseβπ) & β’ (π₯ = β¨π¦, π§β© β πΆ = π·) & β’ (π β Rel π΄) & β’ (π β π΄ β Fin) & β’ (π β π β CMnd) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) β β’ (π β (π Ξ£g (π₯ β π΄ β¦ πΆ)) = (π Ξ£g (π¦ β dom π΄ β¦ (π Ξ£g (π§ β (π΄ β {π¦}) β¦ π·))))) | ||
Theorem | lmodvslmhm 31686* | 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 31687* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 19953, 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 31688* | 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 31689* | 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 | gsumzresunsn 31690 | 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 31691* | 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 | gsumhashmul 31692* | Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ Β· = (.gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (π₯ β (ran πΉ β { 0 }) β¦ ((β―β(β‘πΉ β {π₯})) Β· π₯)))) | ||
Theorem | xrge0tsmsd 31693* | Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015.) (Revised by Thierry Arnoux, 30-Jan-2017.) |
β’ πΊ = (β*π βΎs (0[,]+β)) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) & β’ (π β π = sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, < )) β β’ (π β (πΊ tsums πΉ) = {π}) | ||
Theorem | xrge0tsmsbi 31694 | Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 23-Jun-2017.) |
β’ πΊ = (β*π βΎs (0[,]+β)) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) β β’ (π β (πΆ β (πΊ tsums πΉ) β πΆ = βͺ (πΊ tsums πΉ))) | ||
Theorem | xrge0tsmseq 31695 | Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
β’ πΊ = (β*π βΎs (0[,]+β)) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) & β’ (π β πΆ β (πΊ tsums πΉ)) β β’ (π β πΆ = βͺ (πΊ tsums πΉ)) | ||
Theorem | cntzun 31696 | The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ π΅ = (Baseβπ) & β’ π = (Cntzβπ) β β’ ((π β π΅ β§ π β π΅) β (πβ(π βͺ π)) = ((πβπ) β© (πβπ))) | ||
Theorem | cntzsnid 31697 | The centralizer of the identity element is the whole base set. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ π΅ = (Baseβπ) & β’ π = (Cntzβπ) & β’ 0 = (0gβπ) β β’ (π β Mnd β (πβ{ 0 }) = π΅) | ||
Theorem | cntrcrng 31698 | The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs (Cntrβ(mulGrpβπ ))) β β’ (π β Ring β π β CRing) | ||
Syntax | comnd 31699 | Extend class notation with the class of all right ordered monoids. |
class oMnd | ||
Syntax | cogrp 31700 | Extend class notation with the class of all right ordered groups. |
class oGrp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |