Definition df-grp 12770

Description: Define class of all groups. A group is a monoid (df-mnd 12710) 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 12451) and an internal group operation (notated ( +g ` G ) per df-plusg 12531). 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 12775), associativity (so ( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see grpass 12776), 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 12778). Groups need not be commutative; a commutative group is an Abelian group. Subgroups can often be formed from groups. An example of an (Abelian) group is the set of complex numbers CC over the group operation + (addition). Other structures include groups, including unital rings and fields. (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

Step	Hyp	Ref	Expression
1		cgrp 12767	. 2 class Grp
2		vm	. . . . . . . 8 setvar m
3	2	cv 1352	. . . . . . 7 class m
4		va	. . . . . . . 8 setvar a
5	4	cv 1352	. . . . . . 7 class a
6		vg	. . . . . . . . 9 setvar g
7	6	cv 1352	. . . . . . . 8 class g
8		cplusg 12518	. . . . . . . 8 class +g
9	7, 8	cfv 5212	. . . . . . 7 class ( +g ` g )
10	3, 5, 9	co 5869	. . . . . 6 class ( m ( +g ` g ) a )
11		c0g 12653	. . . . . . 7 class 0g
12	7, 11	cfv 5212	. . . . . 6 class ( 0g ` g )
13	10, 12	wceq 1353	. . . . 5 wff ( m ( +g ` g ) a ) = ( 0g ` g )
14		cbs 12445	. . . . . 6 class Base
15	7, 14	cfv 5212	. . . . 5 class ( Base ` g )
16	13, 2, 15	wrex 2456	. . . 4 wff E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g )
17	16, 4, 15	wral 2455	. . 3 wff A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g )
18		cmnd 12709	. . 3 class Mnd
19	17, 6, 18	crab 2459	. 2 class { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
20	1, 19	wceq 1353	1 wff Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }

This definition is referenced by:  isgrp  12773