Definition df-grp 12711

Description: Define class of all groups. A group is a monoid (df-mnd 12653) 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 12422) and an internal group operation (notated (+_g‘𝐺) per df-plusg 12493). 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 12716), associativity (so ((𝑎+_g𝑏)+_g𝑐) = (𝑎+_g(𝑏+_g𝑐)) for any a, b, c, see grpass 12717), 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 12719). 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 ℂ 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 = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}

Distinct variable group:   𝑔,𝑎,𝑚

Detailed syntax breakdown of Definition df-grp

Step	Hyp	Ref	Expression
1		cgrp 12708	. 2 class Grp
2		vm	. . . . . . . 8 setvar 𝑚
3	2	cv 1347	. . . . . . 7 class 𝑚
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1347	. . . . . . 7 class 𝑎
6		vg	. . . . . . . . 9 setvar 𝑔
7	6	cv 1347	. . . . . . . 8 class 𝑔
8		cplusg 12480	. . . . . . . 8 class +g
9	7, 8	cfv 5198	. . . . . . 7 class (+g‘𝑔)
10	3, 5, 9	co 5853	. . . . . 6 class (𝑚(+g‘𝑔)𝑎)
11		c0g 12596	. . . . . . 7 class 0g
12	7, 11	cfv 5198	. . . . . 6 class (0g‘𝑔)
13	10, 12	wceq 1348	. . . . 5 wff (𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
14		cbs 12416	. . . . . 6 class Base
15	7, 14	cfv 5198	. . . . 5 class (Base‘𝑔)
16	13, 2, 15	wrex 2449	. . . 4 wff ∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
17	16, 4, 15	wral 2448	. . 3 wff ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
18		cmnd 12652	. . 3 class Mnd
19	17, 6, 18	crab 2452	. 2 class {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}
20	1, 19	wceq 1348	1 wff Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}

This definition is referenced by:  isgrp  12714