Definition df-grp 17786

Description: Define class of all groups. A group is a monoid (df-mnd 17655) 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 (Base‘𝐺) per df-base 16235) and an internal group operation (notated (+_g‘𝐺) per df-plusg 16325). 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 17791), associativity (so ((𝑎+_g𝑏)+_g𝑐) = (𝑎+_g(𝑏+_g𝑐)) for any a, b, c, see grpass 17792), identity (there must be an element 𝑒 = (0_g‘𝐺) such that 𝑒+_g𝑎 = 𝑎+_g𝑒 = 𝑎 for any a), and inverse (for each element a in the base set, there must be an element 𝑏 = inv_g𝑎 in the base set such that 𝑎+_g𝑏 = 𝑏+_g𝑎 = 𝑒). It can be proven that the identity element is unique (grpideu 17794). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 18556). Subgroups can often be formed from groups, see df-subg 17949. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition), as proven in cnaddablx 18631; an Abelian group is a group as proven in ablgrp 18558. Other structures include groups, including unital rings (df-ring 18910) and fields (df-field 19113). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)

Assertion

Ref	Expression
df-grp	⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}

Distinct variable group:   𝑔,𝑎,𝑚

Detailed syntax breakdown of Definition df-grp

Step	Hyp	Ref	Expression
1		cgrp 17783	. 2 class Grp
2		vm	. . . . . . . 8 setvar 𝑚
3	2	cv 1655	. . . . . . 7 class 𝑚
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1655	. . . . . . 7 class 𝑎
6		vg	. . . . . . . . 9 setvar 𝑔
7	6	cv 1655	. . . . . . . 8 class 𝑔
8		cplusg 16312	. . . . . . . 8 class +g
9	7, 8	cfv 6127	. . . . . . 7 class (+g‘𝑔)
10	3, 5, 9	co 6910	. . . . . 6 class (𝑚(+g‘𝑔)𝑎)
11		c0g 16460	. . . . . . 7 class 0g
12	7, 11	cfv 6127	. . . . . 6 class (0g‘𝑔)
13	10, 12	wceq 1656	. . . . 5 wff (𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
14		cbs 16229	. . . . . 6 class Base
15	7, 14	cfv 6127	. . . . 5 class (Base‘𝑔)
16	13, 2, 15	wrex 3118	. . . 4 wff ∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
17	16, 4, 15	wral 3117	. . 3 wff ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
18		cmnd 17654	. . 3 class Mnd
19	17, 6, 18	crab 3121	. 2 class {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}
20	1, 19	wceq 1656	1 wff Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}

This definition is referenced by:  isgrp  17789