Definition df-sbg 18956

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 18953	. 2 class -g
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1539	. . . . 5 class 𝑔
7		cbs 17247	. . . . 5 class Base
8	6, 7	cfv 6561	. . . 4 class (Base‘𝑔)
9	4	cv 1539	. . . . 5 class 𝑥
10	5	cv 1539	. . . . . 6 class 𝑦
11		cminusg 18952	. . . . . . 7 class invg
12	6, 11	cfv 6561	. . . . . 6 class (invg‘𝑔)
13	10, 12	cfv 6561	. . . . 5 class ((invg‘𝑔)‘𝑦)
14		cplusg 17297	. . . . . 6 class +g
15	6, 14	cfv 6561	. . . . 5 class (+g‘𝑔)
16	9, 13, 15	co 7431	. . . 4 class (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))
17	4, 5, 8, 8, 16	cmpo 7433	. . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))
18	2, 3, 17	cmpt 5225	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))
19	1, 18	wceq 1540	1 wff -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))

This definition is referenced by:  grpsubfval  19001  grpsubfvalALT  19002