![]() |
Metamath
Proof Explorer Theorem List (p. 191 of 485) | < 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-30805) |
![]() (30806-32328) |
![]() (32329-48426) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grpnpcan 19001 | Cancellation law for subtraction (npcan 11506 analog). (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) + 𝑌) = 𝑋) | ||
Theorem | grpsubsub4 19002 | Double group subtraction (subsub4 11530 analog). (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑍 + 𝑌))) | ||
Theorem | grppnpcan2 19003 | Cancellation law for mixed addition and subtraction. (pnpcan2 11537 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) − (𝑌 + 𝑍)) = (𝑋 − 𝑌)) | ||
Theorem | grpnpncan 19004 | Cancellation law for group subtraction. (npncan 11518 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑍)) = (𝑋 − 𝑍)) | ||
Theorem | grpnpncan0 19005 | Cancellation law for group subtraction (npncan2 11524 analog). (Contributed by AV, 24-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑋)) = 0 ) | ||
Theorem | grpnnncan2 19006 | Cancellation law for group subtraction. (nnncan2 11534 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) − (𝑌 − 𝑍)) = (𝑋 − 𝑌)) | ||
Theorem | dfgrp3lem 19007* | Lemma for dfgrp3 19008. (Contributed by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ∃𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑢 + 𝑎) = 𝑎 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑎) = 𝑢)) | ||
Theorem | dfgrp3 19008* | Alternate definition of a group as semigroup (with at least one element) which is also a quasigroup, i.e. a magma in which solutions 𝑥 and 𝑦 of the equations (𝑎 + 𝑥) = 𝑏 and (𝑥 + 𝑎) = 𝑏 exist. Theorem 3.2 of [Bruck] p. 28. (Contributed by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))) | ||
Theorem | dfgrp3e 19009* | Alternate definition of a group as a set with a closed, associative operation, for which solutions 𝑥 and 𝑦 of the equations (𝑎 + 𝑥) = 𝑏 and (𝑥 + 𝑎) = 𝑏 exist. Exercise 1 of [Herstein] p. 57. (Contributed by NM, 5-Dec-2006.) (Revised by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp ↔ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)))) | ||
Theorem | grplactfval 19010* | The left group action of element 𝐴 of group 𝐺. (Contributed by Paul Chapman, 18-Mar-2008.) |
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝐹‘𝐴) = (𝑎 ∈ 𝑋 ↦ (𝐴 + 𝑎))) | ||
Theorem | grplactval 19011* | The value of the left group action of element 𝐴 of group 𝐺 at 𝐵. (Contributed by Paul Chapman, 18-Mar-2008.) |
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐹‘𝐴)‘𝐵) = (𝐴 + 𝐵)) | ||
Theorem | grplactcnv 19012* | The left group action of element 𝐴 of group 𝐺 maps the underlying set 𝑋 of 𝐺 one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡(𝐹‘𝐴) = (𝐹‘(𝐼‘𝐴)))) | ||
Theorem | grplactf1o 19013* | The left group action of element 𝐴 of group 𝐺 maps the underlying set 𝑋 of 𝐺 one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴):𝑋–1-1-onto→𝑋) | ||
Theorem | grpsubpropd 19014 | Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.) |
⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻)) ⇒ ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻)) | ||
Theorem | grpsubpropd2 19015* | Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) ⇒ ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻)) | ||
Theorem | grp1 19016 | The (smallest) structure representing a trivial group. According to Wikipedia ("Trivial group", 28-Apr-2019, https://en.wikipedia.org/wiki/Trivial_group) "In mathematics, a trivial group is a group consisting of a single element. All such groups are isomorphic, so one often speaks of the trivial group. The single element of the trivial group is the identity element". (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Grp) | ||
Theorem | grp1inv 19017 | The inverse function of the trivial group. (Contributed by FL, 21-Jun-2010.) (Revised by AV, 26-Aug-2021.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → (invg‘𝑀) = ( I ↾ {𝐼})) | ||
Theorem | prdsinvlem 19018* | Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶Grp) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 0 = (0g ∘ 𝑅) & ⊢ 𝑁 = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ (𝑁 + 𝐹) = 0 )) | ||
Theorem | prdsgrpd 19019 | The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Grp) ⇒ ⊢ (𝜑 → 𝑌 ∈ Grp) | ||
Theorem | prdsinvgd 19020* | Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Grp) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑁 = (invg‘𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁‘𝑋) = (𝑥 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑥))‘(𝑋‘𝑥)))) | ||
Theorem | pwsgrp 19021 | A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Grp) | ||
Theorem | pwsinvg 19022 | Negation in a group power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑀 = (invg‘𝑅) & ⊢ 𝑁 = (invg‘𝑌) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = (𝑀 ∘ 𝑋)) | ||
Theorem | pwssub 19023 | Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑀 = (-g‘𝑅) & ⊢ − = (-g‘𝑌) ⇒ ⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹 − 𝐺) = (𝐹 ∘f 𝑀𝐺)) | ||
Theorem | imasgrp2 19024* | The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧)))) & ⊢ (𝜑 → 0 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 )) ⇒ ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0g‘𝑈))) | ||
Theorem | imasgrp 19025* | The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0g‘𝑈))) | ||
Theorem | imasgrpf1 19026 | The image of a group under an injection is a group. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑈 = (𝐹 “s 𝑅) & ⊢ 𝑉 = (Base‘𝑅) ⇒ ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Grp) → 𝑈 ∈ Grp) | ||
Theorem | qusgrp2 19027* | Prove that a quotient structure is a group. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) ∼ (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) ∼ 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) ∼ 0 ) ⇒ ⊢ (𝜑 → (𝑈 ∈ Grp ∧ [ 0 ] ∼ = (0g‘𝑈))) | ||
Theorem | xpsgrp 19028 | The binary product of groups is a group. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → 𝑇 ∈ Grp) | ||
Theorem | xpsinv 19029 | Value of the negation operation in a binary structure product. (Contributed by AV, 18-Mar-2025.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ 𝑀 = (invg‘𝑅) & ⊢ 𝑁 = (invg‘𝑆) & ⊢ 𝐼 = (invg‘𝑇) ⇒ ⊢ (𝜑 → (𝐼‘〈𝐴, 𝐵〉) = 〈(𝑀‘𝐴), (𝑁‘𝐵)〉) | ||
Theorem | xpsgrpsub 19030 | Value of the subtraction operation in a binary structure product of groups. (Contributed by AV, 24-Mar-2025.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ · = (-g‘𝑅) & ⊢ × = (-g‘𝑆) & ⊢ − = (-g‘𝑇) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 − 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) | ||
Theorem | mhmlem 19031* | Lemma for mhmmnd 19033 and ghmgrp 19035. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵))) | ||
Theorem | mhmid 19032* | A surjective monoid morphism preserves identity element. (Contributed by Thierry Arnoux, 25-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → (𝐹‘ 0 ) = (0g‘𝐻)) | ||
Theorem | mhmmnd 19033* | The image of a monoid 𝐺 under a monoid homomorphism 𝐹 is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝐻 ∈ Mnd) | ||
Theorem | mhmfmhm 19034* | The function fulfilling the conditions of mhmmnd 19033 is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐺 MndHom 𝐻)) | ||
Theorem | ghmgrp 19035* | The image of a group 𝐺 under a group homomorphism 𝐹 is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator 𝑂 in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐻 ∈ Grp) | ||
The "group multiple" operation (if the group is multiplicative, also called "group power" or "group exponentiation" operation), can be defined for arbitrary magmas, if the multiplier/exponent is a nonnegative integer. See also the definition in [Lang] p. 6, where an element 𝑥(of a monoid) to the power of a nonnegative integer 𝑛 is defined and denoted by 𝑥↑𝑛. Definition df-mulg 19037, however, defines the group multiple for arbitrary (i.e. also negative) integers. This is meaningful for groups only, and requires Definition df-minusg 18907 of the inverse operation invg. | ||
Syntax | cmg 19036 | Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group. |
class .g | ||
Definition | df-mulg 19037* | Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))) | ||
Theorem | mulgfval 19038* | Group multiple (exponentiation) operation. For a shorter proof using ax-rep 5286, see mulgfvalALT 19039. (Contributed by Mario Carneiro, 11-Dec-2014.) Remove dependency on ax-rep 5286. (Revised by Rohan Ridenour, 17-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) | ||
Theorem | mulgfvalALT 19039* | Shorter proof of mulgfval 19038 using ax-rep 5286. (Contributed by Mario Carneiro, 11-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) | ||
Theorem | mulgval 19040 | Value of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑆 = seq1( + , (ℕ × {𝑋})) ⇒ ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = if(𝑁 = 0, 0 , if(0 < 𝑁, (𝑆‘𝑁), (𝐼‘(𝑆‘-𝑁))))) | ||
Theorem | mulgfn 19041 | Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · Fn (ℤ × 𝐵) | ||
Theorem | mulgfvi 19042 | The group multiple operation is compatible with identity-function protection. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ · = (.g‘𝐺) ⇒ ⊢ · = (.g‘( I ‘𝐺)) | ||
Theorem | mulg0 19043 | Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 ) | ||
Theorem | mulgnn 19044 | Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑆 = seq1( + , (ℕ × {𝑋})) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝑆‘𝑁)) | ||
Theorem | ressmulgnn 19045 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐴 ⊆ (Base‘𝐺) & ⊢ ∗ = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴) → (𝑁(.g‘𝐻)𝑋) = (𝑁 ∗ 𝑋)) | ||
Theorem | ressmulgnn0 19046 | 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 | mulgnngsum 19047* | Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ (1...𝑁) ↦ 𝑋) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝐺 Σg 𝐹)) | ||
Theorem | mulgnn0gsum 19048* | Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in [Lang] p. 6, second formula. (Contributed by AV, 28-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ (1...𝑁) ↦ 𝑋) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝐺 Σg 𝐹)) | ||
Theorem | mulg1 19049 | Group multiple (exponentiation) operation at one. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐵 → (1 · 𝑋) = 𝑋) | ||
Theorem | mulgnnp1 19050 | Group multiple (exponentiation) operation at a successor. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋)) | ||
Theorem | mulg2 19051 | Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐵 → (2 · 𝑋) = (𝑋 + 𝑋)) | ||
Theorem | mulgnegnn 19052 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝐼‘(𝑁 · 𝑋))) | ||
Theorem | mulgnn0p1 19053 | Group multiple (exponentiation) operation at a successor, extended to ℕ0. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋)) | ||
Theorem | mulgnnsubcl 19054* | Closure of the group multiple (exponentiation) operation in a submagma. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆) | ||
Theorem | mulgnn0subcl 19055* | Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 0 ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆) | ||
Theorem | mulgsubcl 19056* | Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 0 ∈ 𝑆) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆) | ||
Theorem | mulgnncl 19057 | Closure of the group multiple (exponentiation) operation for a positive multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) | ||
Theorem | mulgnn0cl 19058 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) | ||
Theorem | mulgcl 19059 | Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) | ||
Theorem | mulgneg 19060 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝐼‘(𝑁 · 𝑋))) | ||
Theorem | mulgnegneg 19061 | The inverse of a negative group multiple is the positive group multiple. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐼‘(-𝑁 · 𝑋)) = (𝑁 · 𝑋)) | ||
Theorem | mulgm1 19062 | Group multiple (exponentiation) operation at negative one. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 20-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (-1 · 𝑋) = (𝐼‘𝑋)) | ||
Theorem | mulgnn0cld 19063 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 19058. (Contributed by SN, 1-Feb-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁 · 𝑋) ∈ 𝐵) | ||
Theorem | mulgcld 19064 | Deduction associated with mulgcl 19059. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁 · 𝑋) ∈ 𝐵) | ||
Theorem | mulgaddcomlem 19065 | Lemma for mulgaddcom 19066. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ ((𝑦 · 𝑋) + 𝑋) = (𝑋 + (𝑦 · 𝑋))) → ((-𝑦 · 𝑋) + 𝑋) = (𝑋 + (-𝑦 · 𝑋))) | ||
Theorem | mulgaddcom 19066 | The group multiple operator commutes with the group operation. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑁 · 𝑋) + 𝑋) = (𝑋 + (𝑁 · 𝑋))) | ||
Theorem | mulginvcom 19067 | The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · (𝐼‘𝑋)) = (𝐼‘(𝑁 · 𝑋))) | ||
Theorem | mulginvinv 19068 | The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐼‘(𝑁 · (𝐼‘𝑋))) = (𝑁 · 𝑋)) | ||
Theorem | mulgnn0z 19069 | A group multiple of the identity, for nonnegative multiple. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0) → (𝑁 · 0 ) = 0 ) | ||
Theorem | mulgz 19070 | A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝑁 · 0 ) = 0 ) | ||
Theorem | mulgnndir 19071 | Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) | ||
Theorem | mulgnn0dir 19072 | Sum of group multiples, generalized to ℕ0. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) | ||
Theorem | mulgdirlem 19073 | Lemma for mulgdir 19074. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) | ||
Theorem | mulgdir 19074 | Sum of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) | ||
Theorem | mulgp1 19075 | Group multiple (exponentiation) operation at a successor, extended to ℤ. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋)) | ||
Theorem | mulgneg2 19076 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝑁 · (𝐼‘𝑋))) | ||
Theorem | mulgnnass 19077 | Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014.) (Revised by AV, 29-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
Theorem | mulgnn0ass 19078 | Product of group multiples, generalized to ℕ0. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
Theorem | mulgass 19079 | Product of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
Theorem | mulgassr 19080 | Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑁 · 𝑀) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
Theorem | mulgmodid 19081 | Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 mod 𝑀) · 𝑋) = (𝑁 · 𝑋)) | ||
Theorem | mulgsubdir 19082 | Distribution of group multiples over subtraction for group elements, subdir 11685 analog. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 − 𝑁) · 𝑋) = ((𝑀 · 𝑋) − (𝑁 · 𝑋))) | ||
Theorem | mhmmulg 19083 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ × = (.g‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))) | ||
Theorem | mulgpropd 19084* | Two structures with the same group-nature have the same group multiple function. 𝐾 is expected to either be V (when strong equality is available) or 𝐵 (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ · = (.g‘𝐺) & ⊢ × = (.g‘𝐻) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐵 ⊆ 𝐾) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐾) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) ⇒ ⊢ (𝜑 → · = × ) | ||
Theorem | submmulgcl 19085 | Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ ∙ = (.g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) ∈ 𝑆) | ||
Theorem | submmulg 19086 | A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ∙ = (.g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ · = (.g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) = (𝑁 · 𝑋)) | ||
Theorem | pwsmulg 19087 | Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ ∙ = (.g‘𝑌) & ⊢ · = (.g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼)) → ((𝑁 ∙ 𝑋)‘𝐴) = (𝑁 · (𝑋‘𝐴))) | ||
Syntax | csubg 19088 | Extend class notation with all subgroups of a group. |
class SubGrp | ||
Syntax | cnsg 19089 | Extend class notation with all normal subgroups of a group. |
class NrmSGrp | ||
Syntax | cqg 19090 | Quotient group equivalence class. |
class ~QG | ||
Definition | df-subg 19091* | Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 19109), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 19104), contains the neutral element of the group (see subg0 19100) and contains the inverses for all of its elements (see subginvcl 19103). (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp}) | ||
Definition | df-nsg 19092* | Define the equivalence relation in a quotient ring or quotient group (where 𝑖 is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ NrmSGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)}) | ||
Definition | df-eqg 19093* | Define the equivalence relation in a group generated by a subgroup. More precisely, if 𝐺 is a group and 𝐻 is a subgroup, then 𝐺 ~QG 𝐻 is the equivalence relation on 𝐺 associated with the left cosets of 𝐻. A typical application of this definition is the construction of the quotient group (resp. ring) of a group (resp. ring) by a normal subgroup (resp. two-sided ideal). (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ~QG = (𝑟 ∈ V, 𝑖 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)}) | ||
Theorem | issubg 19094 | The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) | ||
Theorem | subgss 19095 | A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) | ||
Theorem | subgid 19096 | A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (SubGrp‘𝐺)) | ||
Theorem | subggrp 19097 | A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) | ||
Theorem | subgbas 19098 | The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻)) | ||
Theorem | subgrcl 19099 | Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) | ||
Theorem | subg0 19100 | A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘𝐻)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |