Definition df-sbg

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

	Ref	Expression
Assertion	df-sbg	$$⊢{-}_{𝑔}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_g{inv}_g\left(g\right)\left(y\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csg	$$class{-}_{𝑔}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{\mathrm{Base}}_g$$
7		vy	$$setvary$$
8	3	cv	$$setvarx$$
9		cplusg	$$class{+}_{𝑔}$$
10	5 9	cfv	$$class{+}_g$$
11		cminusg	$$class{inv}_g$$
12	5 11	cfv	$$class{inv}_g\left(g\right)$$
13	7	cv	$$setvary$$
14	13 12	cfv	$$class{inv}_g\left(g\right)\left(y\right)$$
15	8 14 10	co	$$class\left(x{+}_g{inv}_g\left(g\right)\left(y\right)\right)$$
16	3 7 6 6 15	cmpo	$$class\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_g{inv}_g\left(g\right)\left(y\right)\right)$$
17	1 2 16	cmpt	$$class\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_g{inv}_g\left(g\right)\left(y\right)\right)\right)$$
18	0 17	wceq	$$wff{-}_{𝑔}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_g{inv}_g\left(g\right)\left(y\right)\right)\right)$$