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

Definition df-grp 16673
 Description: Define class of all groups. A group is a monoid (df-mnd 16537) 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 15126) and an internal group operation (notated per df-plusg 15203). 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 16679), associativity (so for any a, b, c, see grpass 16680), 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 16682). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 17433). Subgroups can often be formed from groups, see df-subg 16814. An example of an (Abelian) group is the set of complex numbers over the group operation (addition), as proven in cnaddablx 17506; an Abelian group is a group as proven in ablgrp 17435. Other structures include groups, including unital rings (df-ring 17782) and fields (df-field 17978). (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 16669 . 2
2 vm . . . . . . . 8
32cv 1443 . . . . . . 7
4 va . . . . . . . 8
54cv 1443 . . . . . . 7
6 vg . . . . . . . . 9
76cv 1443 . . . . . . . 8
8 cplusg 15190 . . . . . . . 8
97, 8cfv 5582 . . . . . . 7
103, 5, 9co 6290 . . . . . 6
11 c0g 15338 . . . . . . 7
127, 11cfv 5582 . . . . . 6
1310, 12wceq 1444 . . . . 5
14 cbs 15121 . . . . . 6
157, 14cfv 5582 . . . . 5
1613, 2, 15wrex 2738 . . . 4
1716, 4, 15wral 2737 . . 3
18 cmnd 16535 . . 3
1917, 6, 18crab 2741 . 2
201, 19wceq 1444 1
 Colors of variables: wff setvar class This definition is referenced by:  isgrp  16677
 Copyright terms: Public domain W3C validator