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

Definition df-grp 14489
Description: Define class of all groups. A group is a monoid (df-mnd 14367) 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 13153) and an internal group operation (notated  ( +g  `  G
) per df-plusg 13221). 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 14495), associativity (so  ( (
a +g  b ) +g  c )  =  ( a +g  ( b +g  c ) ) for any a, b, c, see grpass 14496), identity (there must be an element  e  =  ( 0g `  G
) such that  e +g  a  =  e +g  a  =  a for any a), and inverse (for each element a in the base set, there must be an element  b  =  inv g 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 14498). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 15092). Subgroups can often be formed from groups, see df-subg 14618. An example of an (Abelian) group is the set of complex numbers  CC over the group operation  + (addition), as proven in cnaddablx 15158; an Abelian group is a group as proven in ablgrp 15094. Other structures include groups, including unital rings (df-rng 15340) and fields (df-field 15515). (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 14362 . 2  class  Grp
2 vm . . . . . . . 8  set  m
32cv 1622 . . . . . . 7  class  m
4 va . . . . . . . 8  set  a
54cv 1622 . . . . . . 7  class  a
6 vg . . . . . . . . 9  set  g
76cv 1622 . . . . . . . 8  class  g
8 cplusg 13208 . . . . . . . 8  class  +g
97, 8cfv 5255 . . . . . . 7  class  ( +g  `  g )
103, 5, 9co 5858 . . . . . 6  class  ( m ( +g  `  g
) a )
11 c0g 13400 . . . . . . 7  class  0g
127, 11cfv 5255 . . . . . 6  class  ( 0g
`  g )
1310, 12wceq 1623 . . . . 5  wff  ( m ( +g  `  g
) a )  =  ( 0g `  g
)
14 cbs 13148 . . . . . 6  class  Base
157, 14cfv 5255 . . . . 5  class  ( Base `  g )
1613, 2, 15wrex 2544 . . . 4  wff  E. m  e.  ( Base `  g
) ( m ( +g  `  g ) a )  =  ( 0g `  g )
1716, 4, 15wral 2543 . . 3  wff  A. a  e.  ( Base `  g
) E. m  e.  ( Base `  g
) ( m ( +g  `  g ) a )  =  ( 0g `  g )
18 cmnd 14361 . . 3  class  Mnd
1917, 6, 18crab 2547 . 2  class  { g  e.  Mnd  |  A. a  e.  ( Base `  g ) E. m  e.  ( Base `  g
) ( m ( +g  `  g ) a )  =  ( 0g `  g ) }
201, 19wceq 1623 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 set class
This definition is referenced by:  isgrp  14493
  Copyright terms: Public domain W3C validator