![]() |
Metamath
Proof Explorer Theorem List (p. 190 of 481) | < 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-30604) |
![]() (30605-32127) |
![]() (32128-48014) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grprcan 18901 | Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) = (𝑌 + 𝑍) ↔ 𝑋 = 𝑌)) | ||
Theorem | grpinveu 18902* | The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 24-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ∃!𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 ) | ||
Theorem | grpid 18903 | Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑋 + 𝑋) = 𝑋 ↔ 0 = 𝑋)) | ||
Theorem | isgrpid2 18904 | Properties showing that an element 𝑍 is the identity element of a group. (Contributed by NM, 7-Aug-2013.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ((𝑍 ∈ 𝐵 ∧ (𝑍 + 𝑍) = 𝑍) ↔ 0 = 𝑍)) | ||
Theorem | grpidd2 18905* | Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 18886. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 0 = (0g‘𝐺)) | ||
Theorem | grpinvfval 18906* | The inverse function of a group. For a shorter proof using ax-rep 5285, see grpinvfvalALT 18907. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) Remove dependency on ax-rep 5285. (Revised by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) | ||
Theorem | grpinvfvalALT 18907* | Shorter proof of grpinvfval 18906 using ax-rep 5285. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) | ||
Theorem | grpinvval 18908* | The inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝑁‘𝑋) = (℩𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 )) | ||
Theorem | grpinvfn 18909 | Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ 𝑁 Fn 𝐵 | ||
Theorem | grpinvfvi 18910 | The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ 𝑁 = (invg‘( I ‘𝐺)) | ||
Theorem | grpsubfval 18911* | Group subtraction (division) operation. For a shorter proof using ax-rep 5285, see grpsubfvalALT 18912. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) Remove dependency on ax-rep 5285. (Revised by Rohan Ridenour, 17-Aug-2023.) (Proof shortened by AV, 19-Feb-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) | ||
Theorem | grpsubfvalALT 18912* | Shorter proof of grpsubfval 18911 using ax-rep 5285. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) | ||
Theorem | grpsubval 18913 | Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌))) | ||
Theorem | grpinvf 18914 | The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵) | ||
Theorem | grpinvcl 18915 | A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵) | ||
Theorem | grpinvcld 18916 | A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁‘𝑋) ∈ 𝐵) | ||
Theorem | grplinv 18917 | The left inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑁‘𝑋) + 𝑋) = 0 ) | ||
Theorem | grprinv 18918 | The right inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + (𝑁‘𝑋)) = 0 ) | ||
Theorem | grpinvid1 18919 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) = 𝑌 ↔ (𝑋 + 𝑌) = 0 )) | ||
Theorem | grpinvid2 18920 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) = 𝑌 ↔ (𝑌 + 𝑋) = 0 )) | ||
Theorem | isgrpinv 18921* | Properties showing that a function 𝑀 is the inverse function of a group. (Contributed by NM, 7-Aug-2013.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ((𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 ) ↔ 𝑁 = 𝑀)) | ||
Theorem | grplinvd 18922 | The left inverse of a group element. Deduction associated with grplinv 18917. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) + 𝑋) = 0 ) | ||
Theorem | grprinvd 18923 | The right inverse of a group element. Deduction associated with grprinv 18918. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + (𝑁‘𝑋)) = 0 ) | ||
Theorem | grplrinv 18924* | In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑦 + 𝑥) = 0 ∧ (𝑥 + 𝑦) = 0 )) | ||
Theorem | grpidinv2 18925* | A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by AV, 1-Sep-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵) → ((( 0 + 𝐴) = 𝐴 ∧ (𝐴 + 0 ) = 𝐴) ∧ ∃𝑦 ∈ 𝐵 ((𝑦 + 𝐴) = 0 ∧ (𝐴 + 𝑦) = 0 ))) | ||
Theorem | grpidinv 18926* | A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (Revised by AV, 1-Sep-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 (((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥) ∧ ∃𝑦 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑢 ∧ (𝑥 + 𝑦) = 𝑢))) | ||
Theorem | grpinvid 18927 | The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 ) | ||
Theorem | grplcan 18928 | Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | grpasscan1 18929 | An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + ((𝑁‘𝑋) + 𝑌)) = 𝑌) | ||
Theorem | grpasscan2 18930 | An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋) | ||
Theorem | grpidrcan 18931 | If right adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑍) = 𝑋 ↔ 𝑍 = 0 )) | ||
Theorem | grpidlcan 18932 | If left adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑍 + 𝑋) = 𝑋 ↔ 𝑍 = 0 )) | ||
Theorem | grpinvinv 18933 | Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝑁‘𝑋)) = 𝑋) | ||
Theorem | grpinvcnv 18934 | The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ◡𝑁 = 𝑁) | ||
Theorem | grpinv11 18935 | The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) = (𝑁‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | grpinvf1o 18936 | The group inverse is a one-to-one onto function. (Contributed by NM, 22-Oct-2014.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑁:𝐵–1-1-onto→𝐵) | ||
Theorem | grpinvnz 18937 | The inverse of a nonzero group element is not zero. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑁‘𝑋) ≠ 0 ) | ||
Theorem | grpinvnzcl 18938 | The inverse of a nonzero group element is a nonzero group element. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ∖ { 0 })) → (𝑁‘𝑋) ∈ (𝐵 ∖ { 0 })) | ||
Theorem | grpsubinv 18939 | Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑁‘𝑌)) = (𝑋 + 𝑌)) | ||
Theorem | grplmulf1o 18940* | Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑋 + 𝑥)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → 𝐹:𝐵–1-1-onto→𝐵) | ||
Theorem | grpinvpropd 18941* | If two structures have the same group components (properties), they have the same group inversion function. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Stefan O'Rear, 21-Mar-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (invg‘𝐾) = (invg‘𝐿)) | ||
Theorem | grpidssd 18942* | If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then both groups have the same identity element. (Contributed by AV, 15-Mar-2019.) |
⊢ (𝜑 → 𝑀 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ Grp) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑀)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (0g‘𝑀) = (0g‘𝑆)) | ||
Theorem | grpinvssd 18943* | If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the elements of the first group have the same inverses in both groups. (Contributed by AV, 15-Mar-2019.) |
⊢ (𝜑 → 𝑀 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ Grp) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑀)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 → ((invg‘𝑆)‘𝑋) = ((invg‘𝑀)‘𝑋))) | ||
Theorem | grpinvadd 18944 | The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁‘𝑌) + (𝑁‘𝑋))) | ||
Theorem | grpsubf 18945 | Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | grpsubcl 18946 | Closure of group subtraction. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵) | ||
Theorem | grpsubrcan 18947 | Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) = (𝑌 − 𝑍) ↔ 𝑋 = 𝑌)) | ||
Theorem | grpinvsub 18948 | Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 − 𝑌)) = (𝑌 − 𝑋)) | ||
Theorem | grpinvval2 18949 | A df-neg 11454-like equation for inverse in terms of group subtraction. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = ( 0 − 𝑋)) | ||
Theorem | grpsubid 18950 | Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 𝑋) = 0 ) | ||
Theorem | grpsubid1 18951 | Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 0 ) = 𝑋) | ||
Theorem | grpsubeq0 18952 | If the difference between two group elements is zero, they are equal. (subeq0 11493 analog.) (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) = 0 ↔ 𝑋 = 𝑌)) | ||
Theorem | grpsubadd0sub 18953 | Subtraction expressed as addition of the difference of the identity element and the subtrahend. (Contributed by AV, 9-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + ( 0 − 𝑌))) | ||
Theorem | grpsubadd 18954 | Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑍 + 𝑌) = 𝑋)) | ||
Theorem | grpsubsub 18955 | Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 − (𝑌 − 𝑍)) = (𝑋 + (𝑍 − 𝑌))) | ||
Theorem | grpaddsubass 18956 | Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = (𝑋 + (𝑌 − 𝑍))) | ||
Theorem | grppncan 18957 | Cancellation law for subtraction (pncan 11473 analog). (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑌) = 𝑋) | ||
Theorem | grpnpcan 18958 | Cancellation law for subtraction (npcan 11476 analog). (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) + 𝑌) = 𝑋) | ||
Theorem | grpsubsub4 18959 | Double group subtraction (subsub4 11500 analog). (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑍 + 𝑌))) | ||
Theorem | grppnpcan2 18960 | Cancellation law for mixed addition and subtraction. (pnpcan2 11507 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) − (𝑌 + 𝑍)) = (𝑋 − 𝑌)) | ||
Theorem | grpnpncan 18961 | Cancellation law for group subtraction. (npncan 11488 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑍)) = (𝑋 − 𝑍)) | ||
Theorem | grpnpncan0 18962 | Cancellation law for group subtraction (npncan2 11494 analog). (Contributed by AV, 24-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑋)) = 0 ) | ||
Theorem | grpnnncan2 18963 | Cancellation law for group subtraction. (nnncan2 11504 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) − (𝑌 − 𝑍)) = (𝑋 − 𝑌)) | ||
Theorem | dfgrp3lem 18964* | Lemma for dfgrp3 18965. (Contributed by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ∃𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑢 + 𝑎) = 𝑎 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑎) = 𝑢)) | ||
Theorem | dfgrp3 18965* | 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 18966* | 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 18967* | The left group action of element 𝐴 of group 𝐺. (Contributed by Paul Chapman, 18-Mar-2008.) |
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝐹‘𝐴) = (𝑎 ∈ 𝑋 ↦ (𝐴 + 𝑎))) | ||
Theorem | grplactval 18968* | The value of the left group action of element 𝐴 of group 𝐺 at 𝐵. (Contributed by Paul Chapman, 18-Mar-2008.) |
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐹‘𝐴)‘𝐵) = (𝐴 + 𝐵)) | ||
Theorem | grplactcnv 18969* | 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 18970* | 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 18971 | Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.) |
⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻)) ⇒ ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻)) | ||
Theorem | grpsubpropd2 18972* | Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) ⇒ ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻)) | ||
Theorem | grp1 18973 | 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 18974 | 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 18975* | Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶Grp) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 0 = (0g ∘ 𝑅) & ⊢ 𝑁 = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ (𝑁 + 𝐹) = 0 )) | ||
Theorem | prdsgrpd 18976 | The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Grp) ⇒ ⊢ (𝜑 → 𝑌 ∈ Grp) | ||
Theorem | prdsinvgd 18977* | Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Grp) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑁 = (invg‘𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁‘𝑋) = (𝑥 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑥))‘(𝑋‘𝑥)))) | ||
Theorem | pwsgrp 18978 | A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Grp) | ||
Theorem | pwsinvg 18979 | Negation in a group power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑀 = (invg‘𝑅) & ⊢ 𝑁 = (invg‘𝑌) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = (𝑀 ∘ 𝑋)) | ||
Theorem | pwssub 18980 | Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑀 = (-g‘𝑅) & ⊢ − = (-g‘𝑌) ⇒ ⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹 − 𝐺) = (𝐹 ∘f 𝑀𝐺)) | ||
Theorem | imasgrp2 18981* | 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 18982* | 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 18983 | 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 18984* | 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 18985 | The binary product of groups is a group. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → 𝑇 ∈ Grp) | ||
Theorem | xpsinv 18986 | 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 18987 | 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 18988* | Lemma for mhmmnd 18990 and ghmgrp 18992. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵))) | ||
Theorem | mhmid 18989* | 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 18990* | 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 18991* | The function fulfilling the conditions of mhmmnd 18990 is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐺 MndHom 𝐻)) | ||
Theorem | ghmgrp 18992* | 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 18994, however, defines the group multiple for arbitrary (i.e. also negative) integers. This is meaningful for groups only, and requires Definition df-minusg 18865 of the inverse operation invg. | ||
Syntax | cmg 18993 | Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group. |
class .g | ||
Definition | df-mulg 18994* | 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 18995* | Group multiple (exponentiation) operation. For a shorter proof using ax-rep 5285, see mulgfvalALT 18996. (Contributed by Mario Carneiro, 11-Dec-2014.) Remove dependency on ax-rep 5285. (Revised by Rohan Ridenour, 17-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) | ||
Theorem | mulgfvalALT 18996* | Shorter proof of mulgfval 18995 using ax-rep 5285. (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 18997 | 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 18998 | 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 18999 | The group multiple operation is compatible with identity-function protection. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ · = (.g‘𝐺) ⇒ ⊢ · = (.g‘( I ‘𝐺)) | ||
Theorem | mulg0 19000 | Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |