Definition df-sbg 12713

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

Assertion

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

Distinct variable group:   x, g, y

Detailed syntax breakdown of Definition df-sbg

Step	Hyp	Ref	Expression
1		csg 12710	. 2 class -g
2		vg	. . 3 setvar g
3		cvv 2730	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1347	. . . . 5 class g
7		cbs 12416	. . . . 5 class Base
8	6, 7	cfv 5198	. . . 4 class ( Base ` g )
9	4	cv 1347	. . . . 5 class x
10	5	cv 1347	. . . . . 6 class y
11		cminusg 12709	. . . . . . 7 class invg
12	6, 11	cfv 5198	. . . . . 6 class ( invg ` g )
13	10, 12	cfv 5198	. . . . 5 class ( ( invg ` g ) ` y )
14		cplusg 12480	. . . . . 6 class +g
15	6, 14	cfv 5198	. . . . 5 class ( +g ` g )
16	9, 13, 15	co 5853	. . . 4 class ( x ( +g ` g ) ( ( invg ` g ) ` y ) )
17	4, 5, 8, 8, 16	cmpo 5855	. . 3 class ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) )
18	2, 3, 17	cmpt 4050	. 2 class ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
19	1, 18	wceq 1348	1 wff -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )

This definition is referenced by:  grpsubfvalg  12748