![]() |
Metamath
Proof Explorer Theorem List (p. 199 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vrgpinv 19801 | The inverse of a generating element is represented by 〈𝐴, 1〉 instead of 〈𝐴, 0〉. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑁‘(𝑈‘𝐴)) = [〈“〈𝐴, 1o〉”〉] ∼ ) | ||
Theorem | frgpuptf 19802* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) ⇒ ⊢ (𝜑 → 𝑇:(𝐼 × 2o)⟶𝐵) | ||
Theorem | frgpuptinv 19803* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2o)) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))) | ||
Theorem | frgpuplem 19804* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))) | ||
Theorem | frgpupf 19805* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) ⇒ ⊢ (𝜑 → 𝐸:𝑋⟶𝐵) | ||
Theorem | frgpupval 19806* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑊) → (𝐸‘[𝐴] ∼ ) = (𝐻 Σg (𝑇 ∘ 𝐴))) | ||
Theorem | frgpup1 19807* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻)) | ||
Theorem | frgpup2 19808* | The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐸‘(𝑈‘𝐴)) = (𝐹‘𝐴)) | ||
Theorem | frgpup3lem 19809* | The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ (𝜑 → 𝐾 ∈ (𝐺 GrpHom 𝐻)) & ⊢ (𝜑 → (𝐾 ∘ 𝑈) = 𝐹) ⇒ ⊢ (𝜑 → 𝐾 = 𝐸) | ||
Theorem | frgpup3 19810* | Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑈 = (varFGrp‘𝐼) ⇒ ⊢ ((𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝐵) → ∃!𝑚 ∈ (𝐺 GrpHom 𝐻)(𝑚 ∘ 𝑈) = 𝐹) | ||
Theorem | 0frgp 19811 | The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐺 = (freeGrp‘∅) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 ≈ 1o | ||
Syntax | ccmn 19812 | Extend class notation with class of all commutative monoids. |
class CMnd | ||
Syntax | cabl 19813 | Extend class notation with class of all Abelian groups. |
class Abel | ||
Definition | df-cmn 19814* | Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)} | ||
Definition | df-abl 19815 | Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ Abel = (Grp ∩ CMnd) | ||
Theorem | isabl 19816 | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) |
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | ||
Theorem | ablgrp 19817 | An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | ||
Theorem | ablgrpd 19818 | An Abelian group is a group, deduction form of ablgrp 19817. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | ablcmn 19819 | An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) | ||
Theorem | ablcmnd 19820 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐺 ∈ CMnd) | ||
Theorem | iscmn 19821* | The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))) | ||
Theorem | isabl2 19822* | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))) | ||
Theorem | cmnpropd 19823* | If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ CMnd ↔ 𝐿 ∈ CMnd)) | ||
Theorem | ablpropd 19824* | If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel)) | ||
Theorem | ablprop 19825 | If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.) |
⊢ (Base‘𝐾) = (Base‘𝐿) & ⊢ (+g‘𝐾) = (+g‘𝐿) ⇒ ⊢ (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel) | ||
Theorem | iscmnd 19826* | Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ CMnd) | ||
Theorem | isabld 19827* | Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ Abel) | ||
Theorem | isabli 19828* | Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.) |
⊢ 𝐺 ∈ Grp & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ 𝐺 ∈ Abel | ||
Theorem | cmnmnd 19829 | A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | ||
Theorem | cmncom 19830 | A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | ablcom 19831 | An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | cmn32 19832 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
Theorem | cmn4 19833 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
Theorem | cmn12 19834 | Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍))) | ||
Theorem | abl32 19835 | Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
Theorem | cmnmndd 19836 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
⊢ (𝜑 → 𝐺 ∈ CMnd) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
Theorem | cmnbascntr 19837 | The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntr‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd → 𝐵 = 𝑍) | ||
Theorem | rinvmod 19838* | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo 7669. (Contributed by AV, 31-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃*𝑤 ∈ 𝐵 (𝐴 + 𝑤) = 0 ) | ||
Theorem | ablinvadd 19839 | The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁‘𝑋) + (𝑁‘𝑌))) | ||
Theorem | ablsub2inv 19840 | Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) − (𝑁‘𝑌)) = (𝑌 − 𝑋)) | ||
Theorem | ablsubadd 19841 | Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑌 + 𝑍) = 𝑋)) | ||
Theorem | ablsub4 19842 | Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) − (𝑍 + 𝑊)) = ((𝑋 − 𝑍) + (𝑌 − 𝑊))) | ||
Theorem | abladdsub4 19843 | Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) = (𝑍 + 𝑊) ↔ (𝑋 − 𝑍) = (𝑊 − 𝑌))) | ||
Theorem | abladdsub 19844 | Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = ((𝑋 − 𝑍) + 𝑌)) | ||
Theorem | ablsubadd23 19845 | Commutative/associative law for addition and subtraction in abelian groups. (subadd23d 11639 analog.) (Contributed by AV, 2-Mar-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + 𝑍) = (𝑋 + (𝑍 − 𝑌))) | ||
Theorem | ablsubaddsub 19846 | Double subtraction and addition in abelian groups. (cnambpcma 47243 analog.) (Contributed by AV, 3-Mar-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 − 𝑌) + 𝑍) − 𝑋) = (𝑍 − 𝑌)) | ||
Theorem | ablpncan2 19847 | Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑋) = 𝑌) | ||
Theorem | ablpncan3 19848 | A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 + (𝑌 − 𝑋)) = 𝑌) | ||
Theorem | ablsubsub 19849 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑌 − 𝑍)) = ((𝑋 − 𝑌) + 𝑍)) | ||
Theorem | ablsubsub4 19850 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍))) | ||
Theorem | ablpnpcan 19851 | Cancellation law for mixed addition and subtraction. (pnpcan 11545 analog.) (Contributed by NM, 29-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) − (𝑋 + 𝑍)) = (𝑌 − 𝑍)) | ||
Theorem | ablnncan 19852 | Cancellation law for group subtraction. (nncan 11535 analog.) (Contributed by NM, 7-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑋 − 𝑌)) = 𝑌) | ||
Theorem | ablsub32 19853 | Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑍) − 𝑌)) | ||
Theorem | ablnnncan 19854 | Cancellation law for group subtraction. (nnncan 11541 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − (𝑌 − 𝑍)) − 𝑍) = (𝑋 − 𝑌)) | ||
Theorem | ablnnncan1 19855 | Cancellation law for group subtraction. (nnncan1 11542 analog.) (Contributed by NM, 7-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − (𝑋 − 𝑍)) = (𝑍 − 𝑌)) | ||
Theorem | ablsubsub23 19856 | Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
Theorem | mulgnn0di 19857 | Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) | ||
Theorem | mulgdi 19858 | Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) | ||
Theorem | mulgmhm 19859* | The map from 𝑥 to 𝑛𝑥 for a fixed positive integer 𝑛 is a monoid homomorphism if the monoid is commutative. (Contributed by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0) → (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 MndHom 𝐺)) | ||
Theorem | mulgghm 19860* | The map from 𝑥 to 𝑛𝑥 for a fixed integer 𝑛 is a group homomorphism if the group is commutative. (Contributed by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 GrpHom 𝐺)) | ||
Theorem | mulgsubdi 19861 | Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 − 𝑌)) = ((𝑀 · 𝑋) − (𝑀 · 𝑌))) | ||
Theorem | ghmfghm 19862* | The function fulfilling the conditions of ghmgrp 19096 is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
Theorem | ghmcmn 19863* | The image of a commutative monoid 𝐺 under a group homomorphism 𝐹 is a commutative monoid. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ CMnd) ⇒ ⊢ (𝜑 → 𝐻 ∈ CMnd) | ||
Theorem | ghmabl 19864* | The image of an abelian group 𝐺 under a group homomorphism 𝐹 is an abelian group. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐻 ∈ Abel) | ||
Theorem | invghm 19865 | The inversion map is a group automorphism if and only if the group is abelian. (In general it is only a group homomorphism into the opposite group, but in an abelian group the opposite group coincides with the group itself.) (Contributed by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝐼 ∈ (𝐺 GrpHom 𝐺)) | ||
Theorem | eqgabl 19866 | Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐵 − 𝐴) ∈ 𝑆))) | ||
Theorem | qusecsub 19867 | Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑆) ⇒ ⊢ (((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ([𝑋] ∼ = [𝑌] ∼ ↔ (𝑌 − 𝑋) ∈ 𝑆)) | ||
Theorem | subgabl 19868 | A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel) | ||
Theorem | subcmn 19869 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝐻 ∈ Mnd) → 𝐻 ∈ CMnd) | ||
Theorem | submcmn 19870 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ CMnd) | ||
Theorem | submcmn2 19871 | A submonoid is commutative iff it is a subset of its own centralizer. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐻 ∈ CMnd ↔ 𝑆 ⊆ (𝑍‘𝑆))) | ||
Theorem | cntzcmn 19872 | The centralizer of any subset in a commutative monoid is the whole monoid. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = 𝐵) | ||
Theorem | cntzcmnss 19873 | Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ (𝑍‘𝑆)) | ||
Theorem | cntrcmnd 19874 | The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝑍 = (𝑀 ↾s (Cntr‘𝑀)) ⇒ ⊢ (𝑀 ∈ Mnd → 𝑍 ∈ CMnd) | ||
Theorem | cntrabl 19875 | The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝑍 = (𝑀 ↾s (Cntr‘𝑀)) ⇒ ⊢ (𝑀 ∈ Grp → 𝑍 ∈ Abel) | ||
Theorem | cntzspan 19876 | If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubMnd‘𝐺)) & ⊢ 𝐻 = (𝐺 ↾s (𝐾‘𝑆)) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ (𝑍‘𝑆)) → 𝐻 ∈ CMnd) | ||
Theorem | cntzcmnf 19877 | Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) | ||
Theorem | ghmplusg 19878 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ + = (+g‘𝑁) ⇒ ⊢ ((𝑁 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpHom 𝑁) ∧ 𝐺 ∈ (𝑀 GrpHom 𝑁)) → (𝐹 ∘f + 𝐺) ∈ (𝑀 GrpHom 𝑁)) | ||
Theorem | ablnsg 19879 | Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝐺 ∈ Abel → (NrmSGrp‘𝐺) = (SubGrp‘𝐺)) | ||
Theorem | odadd1 19880 | The order of a product in an abelian group divides the LCM of the orders of the factors. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ ((𝑂‘𝐴) · (𝑂‘𝐵))) | ||
Theorem | odadd2 19881 | The order of a product in an abelian group is divisible by the LCM of the orders of the factors divided by the GCD. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑂‘𝐴) · (𝑂‘𝐵)) ∥ ((𝑂‘(𝐴 + 𝐵)) · (((𝑂‘𝐴) gcd (𝑂‘𝐵))↑2))) | ||
Theorem | odadd 19882 | The order of a product is the product of the orders, if the factors have coprime order. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 1) → (𝑂‘(𝐴 + 𝐵)) = ((𝑂‘𝐴) · (𝑂‘𝐵))) | ||
Theorem | gex2abl 19883 | A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∥ 2) → 𝐺 ∈ Abel) | ||
Theorem | gexexlem 19884* | Lemma for gexex 19885. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑂‘𝑦) ≤ (𝑂‘𝐴)) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) | ||
Theorem | gexex 19885* | In an abelian group with finite exponent, there is an element in the group with order equal to the exponent. In other words, all orders of elements divide the largest order of an element of the group. This fails if 𝐸 = 0, for example in an infinite p-group, where there are elements of arbitrarily large orders (so 𝐸 is zero) but no elements of infinite order. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ) → ∃𝑥 ∈ 𝑋 (𝑂‘𝑥) = 𝐸) | ||
Theorem | torsubg 19886 | The set of all elements of finite order forms a subgroup of any abelian group, called the torsion subgroup. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel → (◡𝑂 “ ℕ) ∈ (SubGrp‘𝐺)) | ||
Theorem | oddvdssubg 19887* | The set of all elements whose order divides a fixed integer is a subgroup of any abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺)) | ||
Theorem | lsmcomx 19888 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
Theorem | ablcntzd 19889 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) | ||
Theorem | lsmcom 19890 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
Theorem | lsmsubg2 19891 | The sum of two subgroups is a subgroup. (Contributed by NM, 4-Feb-2014.) (Proof shortened by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝐺)) | ||
Theorem | lsm4 19892 | Commutative/associative law for subgroup sum. (Contributed by NM, 26-Sep-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑄 ∈ (SubGrp‘𝐺) ∧ 𝑅 ∈ (SubGrp‘𝐺)) ∧ (𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺))) → ((𝑄 ⊕ 𝑅) ⊕ (𝑇 ⊕ 𝑈)) = ((𝑄 ⊕ 𝑇) ⊕ (𝑅 ⊕ 𝑈))) | ||
Theorem | prdscmnd 19893 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶CMnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ CMnd) | ||
Theorem | prdsabld 19894 | The product of a family of Abelian groups is an Abelian group. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Abel) ⇒ ⊢ (𝜑 → 𝑌 ∈ Abel) | ||
Theorem | pwscmn 19895 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ CMnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CMnd) | ||
Theorem | pwsabl 19896 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Abel ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Abel) | ||
Theorem | qusabl 19897 | If 𝑌 is a subgroup of the abelian group 𝐺, then 𝐻 = 𝐺 / 𝑌 is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel) | ||
Theorem | abl1 19898 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Abel) | ||
Theorem | abln0 19899 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
⊢ Abel ≠ ∅ | ||
Theorem | cnaddablx 19900 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19901 shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl 19901 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
⊢ 𝐺 = {〈1, ℂ〉, 〈2, + 〉} ⇒ ⊢ 𝐺 ∈ Abel |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |