Definition df-sbg 12713

Description: Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.)

Assertion

Ref	Expression
df-sbg	⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))

Distinct variable group:   𝑥,𝑔,𝑦

Detailed syntax breakdown of Definition df-sbg

Step	Hyp	Ref	Expression
1		csg 12710	. 2 class -g
2		vg	. . 3 setvar 𝑔
3		cvv 2730	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1347	. . . . 5 class 𝑔
7		cbs 12416	. . . . 5 class Base
8	6, 7	cfv 5198	. . . 4 class (Base‘𝑔)
9	4	cv 1347	. . . . 5 class 𝑥
10	5	cv 1347	. . . . . 6 class 𝑦
11		cminusg 12709	. . . . . . 7 class invg
12	6, 11	cfv 5198	. . . . . 6 class (invg‘𝑔)
13	10, 12	cfv 5198	. . . . 5 class ((invg‘𝑔)‘𝑦)
14		cplusg 12480	. . . . . 6 class +g
15	6, 14	cfv 5198	. . . . 5 class (+g‘𝑔)
16	9, 13, 15	co 5853	. . . 4 class (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))
17	4, 5, 8, 8, 16	cmpo 5855	. . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))
18	2, 3, 17	cmpt 4050	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))
19	1, 18	wceq 1348	1 wff -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))

This definition is referenced by:  grpsubfvalg  12748