HomeTheorem List (p. 337 of 511)
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. 337 of 511) | < 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-31520) |
Hilbert Space Explorer
(31521-33043) |
Users' Mathboxes
(33044-51033) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mgcmnt2d 33601 | Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹𝐻𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉)) | ||
| Theorem | mgccnv 33602 | 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 33603* | 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 33604 | Property of a Galois connection, lemma for mgcf1o 33606. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ Poset) & ⊢ (𝜑 → 𝑊 ∈ Poset) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐹‘𝑋))) = (𝐹‘𝑋)) | ||
| Theorem | mgcf1olem2 33605 | Property of a Galois connection, lemma for mgcf1o 33606. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ Poset) & ⊢ (𝜑 → 𝑊 ∈ Poset) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌)) | ||
| Theorem | mgcf1o 33606 | 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 33607 | 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 33608 | 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 33609 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13379 and df-xrs 17674), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
| ⊢ 0 = (0g‘ℝ*𝑠) | ||
| Theorem | xrslt 33610 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ < = (lt‘ℝ*𝑠) | ||
| Theorem | xrsinvgval 33611 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13379 and df-xrs 17674), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
| ⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -e𝐵) | ||
| Theorem | xrsmulgzz 33612 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) | ||
| Theorem | xrstos 33613 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
| ⊢ ℝ*𝑠 ∈ Toset | ||
| Theorem | xrsclat 33614 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
| ⊢ ℝ*𝑠 ∈ CLat | ||
| Theorem | xrsp0 33615 | 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 33616 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
| ⊢ +∞ = (1.‘ℝ*𝑠) | ||
| Theorem | xrge00 33617 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
| ⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge0mulgnn0 33618 | 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 33619 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +e 𝐵) +e 𝐶) = (𝐴 +e (𝐵 +e 𝐶))) | ||
| Theorem | xrge0addgt0 33620 | The sum of nonnegative and positive numbers is positive. See addgtge0 11804. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
| ⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +e 𝐵)) | ||
| Theorem | xrge0adddir 33621 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +e 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +e (𝐵 ·e 𝐶))) | ||
| Theorem | xrge0adddi 33622 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +e 𝐵)) = ((𝐶 ·e 𝐴) +e (𝐶 ·e 𝐵))) | ||
| Theorem | xrge0npcan 33623 | Extended nonnegative real version of npcan 11566. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +e -e𝐵) +e 𝐵) = 𝐴) | ||
| Theorem | fsumrp0cl 33624* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
| Theorem | mndcld 33625 | Closure of the operation of a monoid. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) | ||
| Theorem | mndassd 33626 | A monoid operation is associative. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
| Theorem | mndlrinv 33627 | 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 33628* | 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 33629* | If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐹 is injective. See also grplactf1o 19254. 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 33630* | An element 𝑋 of a monoid 𝐸 is left-invertible iff its left-translation 𝐹 is surjective. See also grplactf1o 19254. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑋 + 𝑦) = 0 )) | ||
| Theorem | mndractf1 33631* | If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐺 is injective. See also grplactf1o 19254. 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 33632* | 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 33633* | An element 𝑋 of a monoid 𝐸 is invertible iff its left-translation 𝐹 is bijective. See also grplactf1o 19254. 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 33634* | An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33633. 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 33635 | Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
| Theorem | cmn246135 33636 | Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33872. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑌 + (𝑈 + 𝑊)) + (𝑋 + (𝑍 + 𝑉)))) | ||
| Theorem | cmn145236 33637 | Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33872. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑋 + (𝑈 + 𝑉)) + (𝑌 + (𝑍 + 𝑊)))) | ||
| Theorem | abliso 33638 | 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 33639 | A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
| Theorem | mhmimasplusg 33640 | Value of the operation of the surjective image. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑊 = (𝐹 “s 𝑉) & ⊢ 𝐵 = (Base‘𝑉) & ⊢ 𝐶 = (Base‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐵–onto→𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑉 MndHom 𝑊)) & ⊢ + = (+g‘𝑉) & ⊢ ⨣ = (+g‘𝑊) ⇒ ⊢ (𝜑 → ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)) = (𝐹‘(𝑋 + 𝑌))) | ||
| Theorem | lmhmimasvsca 33641 | 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 33642 | The identity element of a group belongs to the group. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 0 ∈ 𝐵) | ||
| Theorem | grpinvinvd 33643 | Double inverse law for groups. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁‘(𝑁‘𝑋)) = 𝑋) | ||
| Theorem | grpsubcld 33644 | Closure of group subtraction. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝐵) | ||
| Theorem | subgsubcld 33645 | A subgroup is closed under group subtraction. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑆) | ||
| Theorem | subgmulgcld 33646 | Closure of the group multiple within a subgroup. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) & ⊢ (𝜑 → 𝑍 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑍 · 𝐴) ∈ 𝑆) | ||
| Theorem | ressmulgnn0d 33647 | 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 33648 | An abelian group operation is commutative, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | gsumsubg 33649 | 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 33650 | 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 33651* | 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 33652* | Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 20186. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
| ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑦𝜑 & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) | ||
| Theorem | lmodvslmhm 33653* | 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 33654* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 20545, 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 33655* | 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 33656* | 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 33657* | 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 33658* | 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 33659* | Revert ordering in a group sum. See also gsumwrev 19580. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ 𝐵) & ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝑁)) ∧ 𝑘 = (𝑁 − 𝑙)) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑋)) = (𝑀 Σg (𝑙 ∈ (0...𝑁) ↦ 𝑌))) | ||
| Theorem | gsummptp1 33660* | 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 33661* | 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 33662* | 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 33663* | Re-index a finite group sum using a bijection. A version of gsummptf1o 20177 expressed using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ Ⅎ𝑥𝐻 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝑥 = 𝐸 → 𝐶 = 𝐻) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) finSupp 0 ) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐹) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐸 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐷 𝑥 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑦 ∈ 𝐷 ↦ 𝐻))) | ||
| Theorem | gsumfs2d 33664* | Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d 20186 using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))))) | ||
| Theorem | gsumzresunsn 33665 | 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 33666* | 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 | gsumtp 33667* | Group sum of an unordered triple. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷) & ⊢ (𝑘 = 𝑂 → 𝐴 = 𝐸) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ 𝑊) & ⊢ (𝜑 → 𝑂 ∈ 𝑋) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) & ⊢ (𝜑 → 𝑁 ≠ 𝑂) & ⊢ (𝜑 → 𝑀 ≠ 𝑂) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁, 𝑂} ↦ 𝐴)) = ((𝐶 + 𝐷) + 𝐸)) | ||
| Theorem | gsumzrsum 33668* | Relate a group sum on ℤring to a finite sum on the complex numbers. See also gsumfsum 21740. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (ℤring Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
| Theorem | gsummulgc2 33669* | A finite group sum multiplied by a constant. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = (Σ𝑘 ∈ 𝐴 𝑋 · 𝑌)) | ||
| Theorem | gsumhashmul 33670* | 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 | gsummulsubdishift1 33671* | Distribute a subtraction over an indexed sum, shift one of the resulting sums, and regroup terms. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐷:(0...𝑁)⟶𝐵) & ⊢ (𝜑 → 𝐸 = (((𝐷‘𝑁) · 𝐴) − ((𝐷‘0) · 𝐶))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐹 = (((𝐷‘𝑘) · 𝐴) − ((𝐷‘(𝑘 + 1)) · 𝐶))) ⇒ ⊢ (𝜑 → ((𝑅 Σg 𝐷) · (𝐴 − 𝐶)) = ((𝑅 Σg (𝑘 ∈ (0..^𝑁) ↦ 𝐹)) + 𝐸)) | ||
| Theorem | gsummulsubdishift2 33672* | Distribute a subtraction over an indexed sum, shift one of the resulting sums, and regroup terms. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐷:(0...𝑁)⟶𝐵) & ⊢ (𝜑 → 𝐸 = (((𝐷‘0) · 𝐴) − ((𝐷‘𝑁) · 𝐶))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐹 = (((𝐷‘(𝑘 + 1)) · 𝐴) − ((𝐷‘𝑘) · 𝐶))) ⇒ ⊢ (𝜑 → ((𝑅 Σg 𝐷) · (𝐴 − 𝐶)) = ((𝑅 Σg (𝑘 ∈ (0..^𝑁) ↦ 𝐹)) + 𝐸)) | ||
| Theorem | gsummulsubdishift1s 33673* | Distribute a subtraction over an indexed sum, shift one of the resulting sums, and regroup terms. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑉 ∈ 𝐵) & ⊢ (𝑖 = 0 → 𝑉 = 𝐺) & ⊢ (𝑖 = 𝑁 → 𝑉 = 𝐻) & ⊢ (𝑖 = 𝑘 → 𝑉 = 𝑃) & ⊢ (𝑖 = (𝑘 + 1) → 𝑉 = 𝑄) & ⊢ (𝜑 → 𝐸 = ((𝐻 · 𝐴) − (𝐺 · 𝐶))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐹 = ((𝑃 · 𝐴) − (𝑄 · 𝐶))) ⇒ ⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑃)) · (𝐴 − 𝐶)) = ((𝑅 Σg (𝑘 ∈ (0..^𝑁) ↦ 𝐹)) + 𝐸)) | ||
| Theorem | gsummulsubdishift2s 33674* | Distribute a subtraction over an indexed sum, shift one of the resulting sums, and regroup terms. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑉 ∈ 𝐵) & ⊢ (𝑖 = 0 → 𝑉 = 𝐺) & ⊢ (𝑖 = 𝑁 → 𝑉 = 𝐻) & ⊢ (𝑖 = 𝑘 → 𝑉 = 𝑃) & ⊢ (𝑖 = (𝑘 + 1) → 𝑉 = 𝑄) & ⊢ (𝜑 → 𝐸 = ((𝐺 · 𝐴) − (𝐻 · 𝐶))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐹 = ((𝑄 · 𝐴) − (𝑃 · 𝐶))) ⇒ ⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑃)) · (𝐴 − 𝐶)) = ((𝑅 Σg (𝑘 ∈ (0..^𝑁) ↦ 𝐹)) + 𝐸)) | ||
| Theorem | suppgsumssiun 33675* | The support of a function defined as a group sum is a subset of the indexed union of the supports. (Contributed by Thierry Arnoux, 16-Mar-2026.) |
| ⊢ 𝑍 = (0g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝑀 Σg (𝑦 ∈ 𝐵 ↦ 𝐶))) supp 𝑍) ⊆ ∪ 𝑦 ∈ 𝐵 ((𝑥 ∈ 𝐴 ↦ 𝐶) supp 𝑍)) | ||
| Theorem | xrge0tsmsd 33676* | 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 33677 | 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 33678 | 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 | gsumwun 33679* | In a commutative ring, a group sum of a word 𝑊 of characters taken from two submonoids 𝐸 and 𝐹 can be written as a simple sum. (Contributed by Thierry Arnoux, 6-Oct-2025.) |
| ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝐸 ∈ (SubMnd‘𝑀)) & ⊢ (𝜑 → 𝐹 ∈ (SubMnd‘𝑀)) & ⊢ (𝜑 → 𝑊 ∈ Word (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓)) | ||
| Theorem | gsumwrd2dccatlem 33680* | Lemma for gsumwrd2dccat 33681. Expose a bijection 𝐹 between (ordered) pairs of words and words with a length of a subword. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) & ⊢ 𝐹 = (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ ⟨((1st ‘𝑎) ++ (2nd ‘𝑎)), (♯‘(1st ‘𝑎))⟩) & ⊢ 𝐺 = (𝑏 ∈ 𝑈 ↦ ⟨((1st ‘𝑏) prefix (2nd ‘𝑏)), ((1st ‘𝑏) substr ⟨(2nd ‘𝑏), (♯‘(1st ‘𝑏))⟩)⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ◡𝐹 = 𝐺)) | ||
| Theorem | gsumwrd2dccat 33681* | Rewrite a sum ranging over pairs of words as a sum of sums over concatenated subwords. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ (𝜑 → 𝐹:(Word 𝐴 × Word 𝐴)⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg (𝑤 ∈ Word 𝐴 ↦ (𝑀 Σg (𝑗 ∈ (0...(♯‘𝑤)) ↦ (𝐹‘⟨(𝑤 prefix 𝑗), (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)⟩)))))) | ||
| Theorem | cntzun 33682 | The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑍‘(𝑋 ∪ 𝑌)) = ((𝑍‘𝑋) ∩ (𝑍‘𝑌))) | ||
| Theorem | cntzsnid 33683 | 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 33684 | The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑅 ↾s (Cntr‘(mulGrp‘𝑅))) ⇒ ⊢ (𝑅 ∈ Ring → 𝑍 ∈ CRing) | ||
| Theorem | symgfcoeu 33685* | Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐺 = (Base‘(SymGrp‘𝐷)) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝)) | ||
| Theorem | symgcom 33686 | Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
| ⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸)) & ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹)) & ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅) & ⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋)) | ||
| Theorem | symgcom2 33687 | Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.) |
| ⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅) ⇒ ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋)) | ||
| Theorem | symgcntz 33688* | 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 33689 | The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (pmEven‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝑋 ∈ (𝐵 ∖ 𝐴) ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → (𝑋 ∘ 𝑌) ∈ 𝐴) | ||
| Theorem | symgsubg 33690 | The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
| ⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 ∘ ◡𝑌)) | ||
| Theorem | pmtrprfv2 33691 | In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑌) = 𝑋) | ||
| Theorem | pmtrcnel 33692 | 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 33693 | Variation on pmtrcnel 33692. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐽 = (𝐹‘𝐼) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I )) ⇒ ⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) | ||
| Theorem | pmtrcnelor 33694 | 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 | fzo0pmtrlast 33695* | Reorder a half-open integer range based at 0, so that the given index 𝐼 is at the end. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝐽 = (0..^𝑁) & ⊢ (𝜑 → 𝐼 ∈ 𝐽) ⇒ ⊢ (𝜑 → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘(𝑁 − 1)) = 𝐼)) | ||
| Theorem | wrdpmtrlast 33696* | Reorder a word, so that the symbol given at index 𝐼 is at the end. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝐽 = (0..^(♯‘𝑊)) & ⊢ (𝜑 → 𝐼 ∈ 𝐽) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ 𝑈 = ((𝑊 ∘ 𝑠) prefix ((♯‘𝑊) − 1)) ⇒ ⊢ (𝜑 → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑊 ∘ 𝑠) = (𝑈 ++ ⟨“(𝑊‘𝐼)”⟩))) | ||
| Theorem | pmtridf1o 33697 | 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 33698 | 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 33699 | 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 33700 | Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝑆 = (pmSgn‘𝐷) ⇒ ⊢ (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |