Definition df-sbg 18968

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 18965	. 2 class -g
2		vg	. . 3 setvar 𝑔
3		cvv 3477	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1535	. . . . 5 class 𝑔
7		cbs 17244	. . . . 5 class Base
8	6, 7	cfv 6562	. . . 4 class (Base‘𝑔)
9	4	cv 1535	. . . . 5 class 𝑥
10	5	cv 1535	. . . . . 6 class 𝑦
11		cminusg 18964	. . . . . . 7 class invg
12	6, 11	cfv 6562	. . . . . 6 class (invg‘𝑔)
13	10, 12	cfv 6562	. . . . 5 class ((invg‘𝑔)‘𝑦)
14		cplusg 17297	. . . . . 6 class +g
15	6, 14	cfv 6562	. . . . 5 class (+g‘𝑔)
16	9, 13, 15	co 7430	. . . 4 class (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))
17	4, 5, 8, 8, 16	cmpo 7432	. . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))
18	2, 3, 17	cmpt 5230	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))
19	1, 18	wceq 1536	1 wff -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))

This definition is referenced by:  grpsubfval  19013  grpsubfvalALT  19014