![]() |
Metamath
Proof Explorer Theorem List (p. 308 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mcgmnt2 30701 | 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 30702* | 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 30703* | Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦))) & ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥))) & ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢) ⇒ ⊢ (𝜑 → 𝐹𝐻𝐺) | ||
Theorem | dfmgc2 30704* | Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥))))))) | ||
Theorem | mcgcnv 30705 | 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 30706* | 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𝑊)𝐻) | ||
Axiom | ax-xrssca 30707 | 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 30708 | 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 30709 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 12630 and df-xrs 16767), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ 0 = (0g‘ℝ*𝑠) | ||
Theorem | xrslt 30710 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ < = (lt‘ℝ*𝑠) | ||
Theorem | xrsinvgval 30711 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 12630 and df-xrs 16767), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵) | ||
Theorem | xrsmulgzz 30712 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) | ||
Theorem | xrstos 30713 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
⊢ ℝ*𝑠 ∈ Toset | ||
Theorem | xrsclat 30714 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
⊢ ℝ*𝑠 ∈ CLat | ||
Theorem | xrsp0 30715 | 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 30716 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
⊢ +∞ = (1.‘ℝ*𝑠) | ||
Theorem | ressmulgnn 30717 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐴 ⊆ (Base‘𝐺) & ⊢ ∗ = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴) → (𝑁(.g‘𝐻)𝑋) = (𝑁 ∗ 𝑋)) | ||
Theorem | ressmulgnn0 30718 | 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 30719 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge00 30720 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge0plusg 30721 | 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 30722 | The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.) |
⊢ ≤ = (le‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge0mulgnn0 30723 | 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 30724 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
Theorem | xrge0addgt0 30725 | The sum of nonnegative and positive numbers is positive. See addgtge0 11117. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵)) | ||
Theorem | xrge0adddir 30726 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
Theorem | xrge0adddi 30727 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵))) | ||
Theorem | xrge0npcan 30728 | Extended nonnegative real version of npcan 10884. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
Theorem | fsumrp0cl 30729* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
Theorem | abliso 30730 | 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 30731 | 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 30732 | 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 30733* | 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 30734* | Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19085. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑦𝜑 & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝑥 = 〈𝑦, 𝑧〉 → 𝐶 = 𝐷) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) | ||
Theorem | lmodvslmhm 30735* | 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 30736* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 19352, 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 30737* | 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 30738* | 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 30739 | 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 30740* | 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 30741* | 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 30742* | 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 30743 | 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 30744 | 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 30745 | The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑍‘(𝑋 ∪ 𝑌)) = ((𝑍‘𝑋) ∩ (𝑍‘𝑌))) | ||
Theorem | cntzsnid 30746 | 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 30747 | The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝑍 = (𝑅 ↾s (Cntr‘(mulGrp‘𝑅))) ⇒ ⊢ (𝑅 ∈ Ring → 𝑍 ∈ CRing) | ||
Syntax | comnd 30748 | Extend class notation with the class of all right ordered monoids. |
class oMnd | ||
Syntax | cogrp 30749 | Extend class notation with the class of all right ordered groups. |
class oGrp | ||
Definition | df-omnd 30750* | 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 30751 | 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 30752* | 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 30753 | 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 30754 | A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.) |
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) | ||
Theorem | omndmnd 30755 | A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd) | ||
Theorem | omndtos 30756 | A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) | ||
Theorem | omndadd 30757 | In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 + 𝑍) ≤ (𝑌 + 𝑍)) | ||
Theorem | omndaddr 30758 | 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 30759 | 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 30760 | 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 30761 | A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd) | ||
Theorem | xrge0omnd 30762 | The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ oMnd | ||
Theorem | omndmul2 30763 | 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 30764 | 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 30765 | 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 30766 | 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 30767 | In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ≤ = (le‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 − 𝑍) ≤ (𝑌 − 𝑍)) | ||
Theorem | ogrpaddlt 30768 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) | ||
Theorem | ogrpaddltbi 30769 | 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 30770 | 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 30771 | 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 30772 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) < (𝑌 − 𝑍)) | ||
Theorem | ogrpinv0lt 30773 | 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 30774 | 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 30775 | 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 30776* | Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
⊢ 𝐺 = (Base‘(SymGrp‘𝐷)) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝)) | ||
Theorem | symgcom 30777 | Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸)) & ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹)) & ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅) & ⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋)) | ||
Theorem | symgcom2 30778 | Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅) ⇒ ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋)) | ||
Theorem | symgcntz 30779* | 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 30780 | The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (pmEven‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝑋 ∈ (𝐵 ∖ 𝐴) ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → (𝑋 ∘ 𝑌) ∈ 𝐴) | ||
Theorem | symgsubg 30781 | The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 ∘ ◡𝑌)) | ||
Theorem | pmtrprfv2 30782 | In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑌) = 𝑋) | ||
Theorem | pmtrcnel 30783 | 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 30784 | Variation on pmtrcnel 30783. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐽 = (𝐹‘𝐼) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I )) ⇒ ⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) | ||
Theorem | pmtrcnelor 30785 | 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 30786 | 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 30787 | 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 30788 | 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 30789 | Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
⊢ 𝑆 = (pmSgn‘𝐷) ⇒ ⊢ (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1) | ||
Theorem | psgndmfi 30790 | 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 30791 | Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
⊢ 𝐷 = (1...𝑁) & ⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑇‘{𝐾, (𝐾 + 1)}) ∈ ran 𝑇) | ||
Theorem | psgnfzto1stlem 30792* | Lemma for psgnfzto1st 30797. 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 30793* | Value of our permutation 𝑃 at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) ⇒ ⊢ (𝐼 ∈ 𝐷 → (𝑃‘1) = 𝐼) | ||
Theorem | fzto1st1 30794* | Special case where the permutation defined in psgnfzto1st 30797 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) ⇒ ⊢ (𝐼 = 1 → 𝑃 = ( I ↾ 𝐷)) | ||
Theorem | fzto1st 30795* | The function moving one element to the first position (and shifting all elements before it) is a permutation. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐼 ∈ 𝐷 → 𝑃 ∈ 𝐵) | ||
Theorem | fzto1stinvn 30796* | Value of the inverse of our permutation 𝑃 at 𝐼. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐼 ∈ 𝐷 → (◡𝑃‘𝐼) = 1) | ||
Theorem | psgnfzto1st 30797* | The permutation sign for moving one element to the first position. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = (pmSgn‘𝐷) ⇒ ⊢ (𝐼 ∈ 𝐷 → (𝑆‘𝑃) = (-1↑(𝐼 + 1))) | ||
Syntax | ctocyc 30798 | Extend class notation with the permutation cycle builder. |
class toCyc | ||
Definition | df-tocyc 30799* | Define a convenience permutation cycle builder. Given a list of elements to be cycled, in the form of a word, this function produces the corresponding permutation cycle. See definition in [Lang] p. 30. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ toCyc = (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤)))) | ||
Theorem | tocycval 30800* | Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
⊢ 𝐶 = (toCyc‘𝐷) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝐶 = (𝑤 ∈ {𝑢 ∈ Word 𝐷 ∣ 𝑢:dom 𝑢–1-1→𝐷} ↦ (( I ↾ (𝐷 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |