Definition df-grp 18495

Description: Define class of all groups. A group is a monoid (df-mnd 18301) 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 16841) and an internal group operation (notated (+_g‘𝐺) per df-plusg 16901). 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 18500), associativity (so ((𝑎+_g𝑏)+_g𝑐) = (𝑎+_g(𝑏+_g𝑐)) for any a, b, c, see grpass 18501), 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 18503). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 19304). Subgroups can often be formed from groups, see df-subg 18667. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition), as proven in cnaddablx 19384; an Abelian group is a group as proven in ablgrp 19306. Other structures include groups, including unital rings (df-ring 19700) and fields (df-field 19909). (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 18492	. 2 class Grp
2		vm	. . . . . . . 8 setvar 𝑚
3	2	cv 1538	. . . . . . 7 class 𝑚
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1538	. . . . . . 7 class 𝑎
6		vg	. . . . . . . . 9 setvar 𝑔
7	6	cv 1538	. . . . . . . 8 class 𝑔
8		cplusg 16888	. . . . . . . 8 class +g
9	7, 8	cfv 6418	. . . . . . 7 class (+g‘𝑔)
10	3, 5, 9	co 7255	. . . . . 6 class (𝑚(+g‘𝑔)𝑎)
11		c0g 17067	. . . . . . 7 class 0g
12	7, 11	cfv 6418	. . . . . 6 class (0g‘𝑔)
13	10, 12	wceq 1539	. . . . 5 wff (𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
14		cbs 16840	. . . . . 6 class Base
15	7, 14	cfv 6418	. . . . 5 class (Base‘𝑔)
16	13, 2, 15	wrex 3064	. . . 4 wff ∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
17	16, 4, 15	wral 3063	. . 3 wff ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)
18		cmnd 18300	. . 3 class Mnd
19	17, 6, 18	crab 3067	. 2 class {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}
20	1, 19	wceq 1539	1 wff Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}

This definition is referenced by:  isgrp  18498  bj-grpssmnd  35372