Definition df-grp

Description: Define class of all groups. A group is a monoid ( df-mnd ) 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 ( BaseG ) per df-base ) and an internal group operation (notated ( +gG ) per df-plusg ). 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 ), associativity (so ( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see grpass ), identity (there must be an element e = ( 0gG ) 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 ). Groups need not be commutative; a commutative group is an Abelian group (see df-abl ). Subgroups can often be formed from groups, see df-subg . An example of an (Abelian) group is the set of complex numbers CC over the group operation + (addition), as proven in cnaddablx ; an Abelian group is a group as proven in ablgrp . Other structures include groups, including unital rings ( df-ring ) and fields ( df-field ). (Contributed by NM, 17-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Assertion	df-grp	$$⊢\mathrm{Grp}=\left\{g\in \mathrm{Mnd}|\forall a\in {\mathrm{Base}}_g\exists m\in {\mathrm{Base}}_{g}m{+}_{g}a=0_g\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgrp	$$class\mathrm{Grp}$$
1		vg	$$setvarg$$
2		cmnd	$$class\mathrm{Mnd}$$
3		va	$$setvara$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{\mathrm{Base}}_g$$
7		vm	$$setvarm$$
8	7	cv	$$setvarm$$
9		cplusg	$$class{+}_{𝑔}$$
10	5 9	cfv	$$class{+}_g$$
11	3	cv	$$setvara$$
12	8 11 10	co	$$class\left(m{+}_{g}a\right)$$
13		c0g	$$class{0}_{𝑔}$$
14	5 13	cfv	$$class{0}_g$$
15	12 14	wceq	$$wffm{+}_{g}a=0_g$$
16	15 7 6	wrex	$$wff\exists m\in {\mathrm{Base}}_{g}m{+}_{g}a=0_g$$
17	16 3 6	wral	$$wff\forall a\in {\mathrm{Base}}_g\exists m\in {\mathrm{Base}}_{g}m{+}_{g}a=0_g$$
18	17 1 2	crab	$$class\left\{g\in \mathrm{Mnd}|\forall a\in {\mathrm{Base}}_g\exists m\in {\mathrm{Base}}_{g}m{+}_{g}a=0_g\right\}$$
19	0 18	wceq	$$wff\mathrm{Grp}=\left\{g\in \mathrm{Mnd}|\forall a\in {\mathrm{Base}}_g\exists m\in {\mathrm{Base}}_{g}m{+}_{g}a=0_g\right\}$$