MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-grp Structured version   Visualization version   GIF version

Definition df-grp 18046
Description: Define class of all groups. A group is a monoid (df-mnd 17902) whose internal operation is such that every element admits a left inverse (which can be proven to be a two-sided inverse). Thus, a group 𝐺 is an algebraic structure formed from a base set of elements (notated (Base‘𝐺) per df-base 16479) and an internal group operation (notated (+g𝐺) per df-plusg 16568). The operation combines any two elements of the group base set and must satisfy the 4 group axioms: closure (the result of the group operation must always be a member of the base set, see grpcl 18051), associativity (so ((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see grpass 18052), identity (there must be an element 𝑒 = (0g𝐺) such that 𝑒+g𝑎 = 𝑎+g𝑒 = 𝑎 for any a), and inverse (for each element a in the base set, there must be an element 𝑏 = invg𝑎 in the base set such that 𝑎+g𝑏 = 𝑏+g𝑎 = 𝑒). It can be proven that the identity element is unique (grpideu 18054). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 18840). Subgroups can often be formed from groups, see df-subg 18216. An example of an (Abelian) group is the set of complex numbers over the group operation + (addition), as proven in cnaddablx 18919; an Abelian group is a group as proven in ablgrp 18842. Other structures include groups, including unital rings (df-ring 19230) and fields (df-field 19436). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
df-grp Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g𝑔)𝑎) = (0g𝑔)}
Distinct variable group:   𝑔,𝑎,𝑚

Detailed syntax breakdown of Definition df-grp
StepHypRef Expression
1 cgrp 18043 . 2 class Grp
2 vm . . . . . . . 8 setvar 𝑚
32cv 1527 . . . . . . 7 class 𝑚
4 va . . . . . . . 8 setvar 𝑎
54cv 1527 . . . . . . 7 class 𝑎
6 vg . . . . . . . . 9 setvar 𝑔
76cv 1527 . . . . . . . 8 class 𝑔
8 cplusg 16555 . . . . . . . 8 class +g
97, 8cfv 6349 . . . . . . 7 class (+g𝑔)
103, 5, 9co 7145 . . . . . 6 class (𝑚(+g𝑔)𝑎)
11 c0g 16703 . . . . . . 7 class 0g
127, 11cfv 6349 . . . . . 6 class (0g𝑔)
1310, 12wceq 1528 . . . . 5 wff (𝑚(+g𝑔)𝑎) = (0g𝑔)
14 cbs 16473 . . . . . 6 class Base
157, 14cfv 6349 . . . . 5 class (Base‘𝑔)
1613, 2, 15wrex 3139 . . . 4 wff 𝑚 ∈ (Base‘𝑔)(𝑚(+g𝑔)𝑎) = (0g𝑔)
1716, 4, 15wral 3138 . . 3 wff 𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g𝑔)𝑎) = (0g𝑔)
18 cmnd 17901 . . 3 class Mnd
1917, 6, 18crab 3142 . 2 class {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g𝑔)𝑎) = (0g𝑔)}
201, 19wceq 1528 1 wff Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g𝑔)𝑎) = (0g𝑔)}
Colors of variables: wff setvar class
This definition is referenced by:  isgrp  18049  bj-grpssmnd  34445
  Copyright terms: Public domain W3C validator