Definition df-sbg

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

	Ref	Expression
Assertion	df-sbg	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csg	|- -g
1		vg	|- g
2		cvv	|- _V
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- g
6	5 4	cfv	|- ( Base ` g )
7		vy	|- y
8	3	cv	|- x
9		cplusg	|- +g
10	5 9	cfv	|- ( +g ` g )
11		cminusg	|- invg
12	5 11	cfv	|- ( invg ` g )
13	7	cv	|- y
14	13 12	cfv	|- ( ( invg ` g ) ` y )
15	8 14 10	co	|- ( x ( +g ` g ) ( ( invg ` g ) ` y ) )
16	3 7 6 6 15	cmpo	|- ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) )
17	1 2 16	cmpt	|- ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
18	0 17	wceq	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )