Definition df-grp 13866

Description: Define class of all groups. A group is a monoid (df-mnd 13788) 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 13415) and an internal group operation (notated ( +g ` G ) per df-plusg 13502). 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 13871), associativity (so ( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see grpass 13872), 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 13874). 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 13863	. 2 class Grp
2		vm	. . . . . . . 8 setvar m
3	2	cv 1401	. . . . . . 7 class m
4		va	. . . . . . . 8 setvar a
5	4	cv 1401	. . . . . . 7 class a
6		vg	. . . . . . . . 9 setvar g
7	6	cv 1401	. . . . . . . 8 class g
8		cplusg 13489	. . . . . . . 8 class +g
9	7, 8	cfv 5380	. . . . . . 7 class ( +g ` g )
10	3, 5, 9	co 6088	. . . . . 6 class ( m ( +g ` g ) a )
11		c0g 13668	. . . . . . 7 class 0g
12	7, 11	cfv 5380	. . . . . 6 class ( 0g ` g )
13	10, 12	wceq 1402	. . . . 5 wff ( m ( +g ` g ) a ) = ( 0g ` g )
14		cbs 13409	. . . . . 6 class Base
15	7, 14	cfv 5380	. . . . 5 class ( Base ` g )
16	13, 2, 15	wrex 2529	. . . 4 wff E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g )
17	16, 4, 15	wral 2528	. . 3 wff A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g )
18		cmnd 13787	. . 3 class Mnd
19	17, 6, 18	crab 2532	. 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 1402	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 used by:  isgrp  13869