Definition df-sbg 18563

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 18560	. 2 class -g
2		vg	. . 3 setvar 𝑔
3		cvv 3430	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1540	. . . . 5 class 𝑔
7		cbs 16893	. . . . 5 class Base
8	6, 7	cfv 6430	. . . 4 class (Base‘𝑔)
9	4	cv 1540	. . . . 5 class 𝑥
10	5	cv 1540	. . . . . 6 class 𝑦
11		cminusg 18559	. . . . . . 7 class invg
12	6, 11	cfv 6430	. . . . . 6 class (invg‘𝑔)
13	10, 12	cfv 6430	. . . . 5 class ((invg‘𝑔)‘𝑦)
14		cplusg 16943	. . . . . 6 class +g
15	6, 14	cfv 6430	. . . . 5 class (+g‘𝑔)
16	9, 13, 15	co 7268	. . . 4 class (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))
17	4, 5, 8, 8, 16	cmpo 7270	. . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))
18	2, 3, 17	cmpt 5161	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))
19	1, 18	wceq 1541	1 wff -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))

This definition is referenced by:  grpsubfval  18604  grpsubfvalALT  18605