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

Definition df-grp 16381
Description: Define class of all groups. A group is a monoid (df-mnd 16245) 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  G is an algebraic structure formed from a base set of elements (notated  ( Base `  G
) per df-base 14846) and an internal group operation (notated  ( +g  `  G
) per df-plusg 14922). 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 16387), associativity (so  ( (
a +g  b ) +g  c )  =  ( a +g  ( b +g  c ) ) for any a, b, c, see grpass 16388), identity (there must be an element  e  =  ( 0g `  G
) such that  e +g  a  =  a +g  e  =  a for any a), and inverse (for each element a in the base set, there must be an element  b  =  invg a in the base set such that  a +g  b  =  b +g  a  =  e). It can be proven that the identity element is unique (grpideu 16390). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 17125). Subgroups can often be formed from groups, see df-subg 16522. An example of an (Abelian) group is the set of complex numbers  CC over the group operation  + (addition), as proven in cnaddablx 17198; an Abelian group is a group as proven in ablgrp 17127. Other structures include groups, including unital rings (df-ring 17520) and fields (df-field 17719). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
df-grp  |-  Grp  =  { g  e.  Mnd  | 
A. a  e.  (
Base `  g ) E. m  e.  ( Base `  g ) ( m ( +g  `  g
) a )  =  ( 0g `  g
) }
Distinct variable group:    g, a, m

Detailed syntax breakdown of Definition df-grp
StepHypRef Expression
1 cgrp 16377 . 2  class  Grp
2 vm . . . . . . . 8  setvar  m
32cv 1404 . . . . . . 7  class  m
4 va . . . . . . . 8  setvar  a
54cv 1404 . . . . . . 7  class  a
6 vg . . . . . . . . 9  setvar  g
76cv 1404 . . . . . . . 8  class  g
8 cplusg 14909 . . . . . . . 8  class  +g
97, 8cfv 5569 . . . . . . 7  class  ( +g  `  g )
103, 5, 9co 6278 . . . . . 6  class  ( m ( +g  `  g
) a )
11 c0g 15054 . . . . . . 7  class  0g
127, 11cfv 5569 . . . . . 6  class  ( 0g
`  g )
1310, 12wceq 1405 . . . . 5  wff  ( m ( +g  `  g
) a )  =  ( 0g `  g
)
14 cbs 14841 . . . . . 6  class  Base
157, 14cfv 5569 . . . . 5  class  ( Base `  g )
1613, 2, 15wrex 2755 . . . 4  wff  E. m  e.  ( Base `  g
) ( m ( +g  `  g ) a )  =  ( 0g `  g )
1716, 4, 15wral 2754 . . 3  wff  A. a  e.  ( Base `  g
) E. m  e.  ( Base `  g
) ( m ( +g  `  g ) a )  =  ( 0g `  g )
18 cmnd 16243 . . 3  class  Mnd
1917, 6, 18crab 2758 . 2  class  { g  e.  Mnd  |  A. a  e.  ( Base `  g ) E. m  e.  ( Base `  g
) ( m ( +g  `  g ) a )  =  ( 0g `  g ) }
201, 19wceq 1405 1  wff  Grp  =  { g  e.  Mnd  | 
A. a  e.  (
Base `  g ) E. m  e.  ( Base `  g ) ( m ( +g  `  g
) a )  =  ( 0g `  g
) }
Colors of variables: wff setvar class
This definition is referenced by:  isgrp  16385
  Copyright terms: Public domain W3C validator