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

Definition df-grp 14843
 Description: Define class of all groups. A group is a monoid (df-mnd 14721) 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 per df-base 13505) and an internal group operation (notated per df-plusg 13573). 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 14849), associativity (so for any a, b, c, see grpass 14850), identity (there must be an element such that for any a), and inverse (for each element a in the base set, there must be an element in the base set such that ). It can be proven that the identity element is unique (grpideu 14852). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 15446). Subgroups can often be formed from groups, see df-subg 14972. An example of an (Abelian) group is the set of complex numbers over the group operation (addition), as proven in cnaddablx 15512; an Abelian group is a group as proven in ablgrp 15448. Other structures include groups, including unital rings (df-rng 15694) and fields (df-field 15869). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
df-grp
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-grp
StepHypRef Expression
1 cgrp 14716 . 2
2 vm . . . . . . . 8
32cv 1652 . . . . . . 7
4 va . . . . . . . 8
54cv 1652 . . . . . . 7
6 vg . . . . . . . . 9
76cv 1652 . . . . . . . 8
8 cplusg 13560 . . . . . . . 8
97, 8cfv 5483 . . . . . . 7
103, 5, 9co 6110 . . . . . 6
11 c0g 13754 . . . . . . 7
127, 11cfv 5483 . . . . . 6
1310, 12wceq 1653 . . . . 5
14 cbs 13500 . . . . . 6
157, 14cfv 5483 . . . . 5
1613, 2, 15wrex 2712 . . . 4
1716, 4, 15wral 2711 . . 3
18 cmnd 14715 . . 3
1917, 6, 18crab 2715 . 2
201, 19wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  isgrp  14847
 Copyright terms: Public domain W3C validator