![]() |
Metamath
Proof Explorer Theorem List (p. 328 of 482) | < 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: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mgcmnt1 32701 | 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 32702 | 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 32703* | 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 32704* | Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΊ:π΅βΆπ΄) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) & β’ (π β βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) & β’ ((π β§ π₯ β π΄) β π₯ β€ (πΊβ(πΉβπ₯))) & β’ ((π β§ π’ β π΅) β (πΉβ(πΊβπ’)) β² π’) β β’ (π β πΉπ»πΊ) | ||
Theorem | dfmgc2 32705* | Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) β β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))))))) | ||
Theorem | mgcmnt1d 32706 | Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) β β’ (π β πΉ β (πMonotπ)) | ||
Theorem | mgcmnt2d 32707 | Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) β β’ (π β πΊ β (πMonotπ)) | ||
Theorem | mgccnv 32708 | 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 32709* | 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 32710 | Property of a Galois connection, lemma for mgcf1o 32712. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β Poset) & β’ (π β π β Poset) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΄) β β’ (π β (πΉβ(πΊβ(πΉβπ))) = (πΉβπ)) | ||
Theorem | mgcf1olem2 32711 | Property of a Galois connection, lemma for mgcf1o 32712. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β Poset) & β’ (π β π β Poset) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΅) β β’ (π β (πΊβ(πΉβ(πΊβπ))) = (πΊβπ)) | ||
Theorem | mgcf1o 32712 | 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 32713 | 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 32714 | 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 32715 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13252 and df-xrs 17475), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
β’ 0 = (0gββ*π ) | ||
Theorem | xrslt 32716 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ < = (ltββ*π ) | ||
Theorem | xrsinvgval 32717 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13252 and df-xrs 17475), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
β’ (π΅ β β* β ((invgββ*π )βπ΅) = -ππ΅) | ||
Theorem | xrsmulgzz 32718 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
β’ ((π΄ β β€ β§ π΅ β β*) β (π΄(.gββ*π )π΅) = (π΄ Β·e π΅)) | ||
Theorem | xrstos 32719 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
β’ β*π β Toset | ||
Theorem | xrsclat 32720 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
β’ β*π β CLat | ||
Theorem | xrsp0 32721 | 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 32722 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
β’ +β = (1.ββ*π ) | ||
Theorem | xrge0base 32723 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ (0[,]+β) = (Baseβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge00 32724 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ 0 = (0gβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge0plusg 32725 | 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 32726 | The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.) |
β’ β€ = (leβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge0mulgnn0 32727 | 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 32728 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β ((π΄ +π π΅) +π πΆ) = (π΄ +π (π΅ +π πΆ))) | ||
Theorem | xrge0addgt0 32729 | The sum of nonnegative and positive numbers is positive. See addgtge0 11724. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
β’ (((π΄ β (0[,]+β) β§ π΅ β (0[,]+β)) β§ 0 < π΄) β 0 < (π΄ +π π΅)) | ||
Theorem | xrge0adddir 32730 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β ((π΄ +π π΅) Β·e πΆ) = ((π΄ Β·e πΆ) +π (π΅ Β·e πΆ))) | ||
Theorem | xrge0adddi 32731 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β (πΆ Β·e (π΄ +π π΅)) = ((πΆ Β·e π΄) +π (πΆ Β·e π΅))) | ||
Theorem | xrge0npcan 32732 | Extended nonnegative real version of npcan 11491. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ π΅ β€ π΄) β ((π΄ +π -ππ΅) +π π΅) = π΄) | ||
Theorem | fsumrp0cl 32733* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β Ξ£π β π΄ π΅ β (0[,)+β)) | ||
Theorem | abliso 32734 | 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 32735 | A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ (π β πΉ β (π LMHom π)) β β’ (π β πΉ β (π GrpHom π)) | ||
Theorem | mhmimasplusg 32736 | Value of the operation of the surjective image. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (πΉ βs π) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ:π΅βontoβπΆ) & β’ (π β πΉ β (π MndHom π)) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ (π β ((πΉβπ) ⨣ (πΉβπ)) = (πΉβ(π + π))) | ||
Theorem | lmhmimasvsca 32737 | 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 | gsumsubg 32738 | 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 32739 | 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 32740* | 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 32741* | Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19918. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
β’ β²π§πΆ & β’ β²π¦π & β’ π΅ = (Baseβπ) & β’ (π₯ = β¨π¦, π§β© β πΆ = π·) & β’ (π β Rel π΄) & β’ (π β π΄ β Fin) & β’ (π β π β CMnd) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) β β’ (π β (π Ξ£g (π₯ β π΄ β¦ πΆ)) = (π Ξ£g (π¦ β dom π΄ β¦ (π Ξ£g (π§ β (π΄ β {π¦}) β¦ π·))))) | ||
Theorem | lmodvslmhm 32742* | 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 32743* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 20241, 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 32744* | 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 32745* | 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 32746 | 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 32747* | 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 32748* | 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 32749* | 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 32750 | 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 32751 | 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 32752 | The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ π΅ = (Baseβπ) & β’ π = (Cntzβπ) β β’ ((π β π΅ β§ π β π΅) β (πβ(π βͺ π)) = ((πβπ) β© (πβπ))) | ||
Theorem | cntzsnid 32753 | 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 32754 | The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs (Cntrβ(mulGrpβπ ))) β β’ (π β Ring β π β CRing) | ||
Syntax | comnd 32755 | Extend class notation with the class of all right ordered monoids. |
class oMnd | ||
Syntax | cogrp 32756 | Extend class notation with the class of all right ordered groups. |
class oGrp | ||
Definition | df-omnd 32757* | Define class of all right ordered monoids. An ordered monoid is a monoid with a total ordering compatible with its operation. It is possible to use this definition also for left ordered monoids, by applying it to (oppgβπ). (Contributed by Thierry Arnoux, 13-Mar-2018.) |
β’ oMnd = {π β Mnd β£ [(Baseβπ) / π£][(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ)))} | ||
Definition | df-ogrp 32758 | Define class of all ordered groups. An ordered group is a group with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
β’ oGrp = (Grp β© oMnd) | ||
Theorem | isomnd 32759* | A (left) ordered monoid is a monoid with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ β€ = (leβπ) β β’ (π β oMnd β (π β Mnd β§ π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π)))) | ||
Theorem | isogrp 32760 | A (left-)ordered group is a group with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ (πΊ β oGrp β (πΊ β Grp β§ πΊ β oMnd)) | ||
Theorem | ogrpgrp 32761 | A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.) |
β’ (πΊ β oGrp β πΊ β Grp) | ||
Theorem | omndmnd 32762 | A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
β’ (π β oMnd β π β Mnd) | ||
Theorem | omndtos 32763 | A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
β’ (π β oMnd β π β Toset) | ||
Theorem | omndadd 32764 | In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ + = (+gβπ) β β’ ((π β oMnd β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π + π) β€ (π + π)) | ||
Theorem | omndaddr 32765 | In a right ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ + = (+gβπ) β β’ (((oppgβπ) β oMnd β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π + π) β€ (π + π)) | ||
Theorem | omndadd2d 32766 | In a commutative left ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ + = (+gβπ) & β’ (π β π β oMnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β π β CMnd) β β’ (π β (π + π) β€ (π + π)) | ||
Theorem | omndadd2rd 32767 | In a left- and right- ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 2-May-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ + = (+gβπ) & β’ (π β π β oMnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β (oppgβπ) β oMnd) β β’ (π β (π + π) β€ (π + π)) | ||
Theorem | submomnd 32768 | A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ ((π β oMnd β§ (π βΎs π΄) β Mnd) β (π βΎs π΄) β oMnd) | ||
Theorem | xrge0omnd 32769 | The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.) |
β’ (β*π βΎs (0[,]+β)) β oMnd | ||
Theorem | omndmul2 32770 | In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ 0 = (0gβπ) β β’ ((π β oMnd β§ (π β π΅ β§ π β β0) β§ 0 β€ π) β 0 β€ (π Β· π)) | ||
Theorem | omndmul3 32771 | In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ 0 = (0gβπ) & β’ (π β π β oMnd) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β€ π) & β’ (π β π β π΅) & β’ (π β 0 β€ π) β β’ (π β (π Β· π) β€ (π Β· π)) | ||
Theorem | omndmul 32772 | In a commutative ordered monoid, the ordering is compatible with group power. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ (π β π β oMnd) & β’ (π β π β CMnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β β0) & β’ (π β π β€ π) β β’ (π β (π Β· π) β€ (π Β· π)) | ||
Theorem | ogrpinv0le 32773 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ β€ = (leβπΊ) & β’ πΌ = (invgβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β oGrp β§ π β π΅) β ( 0 β€ π β (πΌβπ) β€ 0 )) | ||
Theorem | ogrpsub 32774 | In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (BaseβπΊ) & β’ β€ = (leβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π β π) β€ (π β π)) | ||
Theorem | ogrpaddlt 32775 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π + π) < (π + π)) | ||
Theorem | ogrpaddltbi 32776 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π < π β (π + π) < (π + π))) | ||
Theorem | ogrpaddltrd 32777 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β (oppgβπΊ) β oGrp) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π < π) β β’ (π β (π + π) < (π + π)) | ||
Theorem | ogrpaddltrbid 32778 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β (oppgβπΊ) β oGrp) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π < π β (π + π) < (π + π))) | ||
Theorem | ogrpsublt 32779 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π β π) < (π β π)) | ||
Theorem | ogrpinv0lt 32780 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ πΌ = (invgβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β oGrp β§ π β π΅) β ( 0 < π β (πΌβπ) < 0 )) | ||
Theorem | ogrpinvlt 32781 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ πΌ = (invgβπΊ) β β’ (((πΊ β oGrp β§ (oppgβπΊ) β oGrp) β§ π β π΅ β§ π β π΅) β (π < π β (πΌβπ) < (πΌβπ))) | ||
Theorem | gsumle 32782 | A finite sum in an ordered monoid is monotonic. This proof would be much easier in an ordered group, where an inverse element would be available. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ (π β π β oMnd) & β’ (π β π β CMnd) & β’ (π β π΄ β Fin) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΊ:π΄βΆπ΅) & β’ (π β πΉ βr β€ πΊ) β β’ (π β (π Ξ£g πΉ) β€ (π Ξ£g πΊ)) | ||
Theorem | symgfcoeu 32783* | Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ πΊ = (Baseβ(SymGrpβπ·)) β β’ ((π· β π β§ π β πΊ β§ π β πΊ) β β!π β πΊ π = (π β π)) | ||
Theorem | symgcom 32784 | Two permutations π and π commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π βΎ πΈ) = ( I βΎ πΈ)) & β’ (π β (π βΎ πΉ) = ( I βΎ πΉ)) & β’ (π β (πΈ β© πΉ) = β ) & β’ (π β (πΈ βͺ πΉ) = π΄) β β’ (π β (π β π) = (π β π)) | ||
Theorem | symgcom2 32785 | Two permutations π and π commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (dom (π β I ) β© dom (π β I )) = β ) β β’ (π β (π β π) = (π β π)) | ||
Theorem | symgcntz 32786* | All elements of a (finite) set of permutations commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π΅ = (Baseβπ) & β’ π = (Cntzβπ) & β’ (π β π΄ β π΅) & β’ (π β Disj π₯ β π΄ dom (π₯ β I )) β β’ (π β π΄ β (πβπ΄)) | ||
Theorem | odpmco 32787 | The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ π = (SymGrpβπ·) & β’ π΅ = (Baseβπ) & β’ π΄ = (pmEvenβπ·) β β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (π β π) β π΄) | ||
Theorem | symgsubg 32788 | The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π β β‘π)) | ||
Theorem | pmtrprfv2 32789 | In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π)) β ((πβ{π, π})βπ) = π) | ||
Theorem | pmtrcnel 32790 | Composing a permutation πΉ with a transposition which results in moving at least one less point. Here the set of points moved by a permutation πΉ is expressed as dom (πΉ β I ). (Contributed by Thierry Arnoux, 16-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (pmTrspβπ·) & β’ π΅ = (Baseβπ) & β’ π½ = (πΉβπΌ) & β’ (π β π· β π) & β’ (π β πΉ β π΅) & β’ (π β πΌ β dom (πΉ β I )) β β’ (π β dom (((πβ{πΌ, π½}) β πΉ) β I ) β (dom (πΉ β I ) β {πΌ})) | ||
Theorem | pmtrcnel2 32791 | Variation on pmtrcnel 32790. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (pmTrspβπ·) & β’ π΅ = (Baseβπ) & β’ π½ = (πΉβπΌ) & β’ (π β π· β π) & β’ (π β πΉ β π΅) & β’ (π β πΌ β dom (πΉ β I )) β β’ (π β (dom (πΉ β I ) β {πΌ, π½}) β dom (((πβ{πΌ, π½}) β πΉ) β I )) | ||
Theorem | pmtrcnelor 32792 | Composing a permutation πΉ with a transposition which results in moving one or two less points. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (pmTrspβπ·) & β’ π΅ = (Baseβπ) & β’ π½ = (πΉβπΌ) & β’ (π β π· β π) & β’ (π β πΉ β π΅) & β’ (π β πΌ β dom (πΉ β I )) & β’ πΈ = dom (πΉ β I ) & β’ π΄ = dom (((πβ{πΌ, π½}) β πΉ) β I ) β β’ (π β (π΄ = (πΈ β {πΌ, π½}) β¨ π΄ = (πΈ β {πΌ}))) | ||
Theorem | pmtridf1o 32793 | Transpositions of π and π (understood to be the identity when π = π), are bijections. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
β’ (π β π΄ β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ π = if(π = π, ( I βΎ π΄), ((pmTrspβπ΄)β{π, π})) β β’ (π β π:π΄β1-1-ontoβπ΄) | ||
Theorem | pmtridfv1 32794 | Value at X of the transposition of π and π (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.) |
β’ (π β π΄ β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ π = if(π = π, ( I βΎ π΄), ((pmTrspβπ΄)β{π, π})) β β’ (π β (πβπ) = π) | ||
Theorem | pmtridfv2 32795 | Value at Y of the transposition of π and π (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.) |
β’ (π β π΄ β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ π = if(π = π, ( I βΎ π΄), ((pmTrspβπ΄)β{π, π})) β β’ (π β (πβπ) = π) | ||
Theorem | psgnid 32796 | Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π = (pmSgnβπ·) β β’ (π· β Fin β (πβ( I βΎ π·)) = 1) | ||
Theorem | psgndmfi 32797 | For a finite base set, the permutation sign is defined for all permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π = (pmSgnβπ·) & β’ πΊ = (Baseβ(SymGrpβπ·)) β β’ (π· β Fin β π Fn πΊ) | ||
Theorem | pmtrto1cl 32798 | Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π· = (1...π) & β’ π = (pmTrspβπ·) β β’ ((πΎ β β β§ (πΎ + 1) β π·) β (πβ{πΎ, (πΎ + 1)}) β ran π) | ||
Theorem | psgnfzto1stlem 32799* | Lemma for psgnfzto1st 32804. Our permutation of rank (π + 1) can be written as a permutation of rank π composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π· = (1...π) β β’ ((πΎ β β β§ (πΎ + 1) β π·) β (π β π· β¦ if(π = 1, (πΎ + 1), if(π β€ (πΎ + 1), (π β 1), π))) = (((pmTrspβπ·)β{πΎ, (πΎ + 1)}) β (π β π· β¦ if(π = 1, πΎ, if(π β€ πΎ, (π β 1), π))))) | ||
Theorem | fzto1stfv1 32800* | Value of our permutation π at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
β’ π· = (1...π) & β’ π = (π β π· β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) β β’ (πΌ β π· β (πβ1) = πΌ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |