Definition df-plusf 13057

Description: Define group addition function. Usually we will use +g directly instead of +f, and they have the same behavior in most cases. The main advantage of +f for any magma is that it is a guaranteed function (mgmplusf 13068), while +g only has closure (mgmcl 13061). (Contributed by Mario Carneiro, 14-Aug-2015.)

Assertion

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

Distinct variable group:   x, g, y

Detailed syntax breakdown of Definition df-plusf

Step	Hyp	Ref	Expression
1		cplusf 13055	. 2 class +f
2		vg	. . 3 setvar g
3		cvv 2763	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1363	. . . . 5 class g
7		cbs 12703	. . . . 5 class Base
8	6, 7	cfv 5259	. . . 4 class ( Base ` g )
9	4	cv 1363	. . . . 5 class x
10	5	cv 1363	. . . . 5 class y
11		cplusg 12780	. . . . . 6 class +g
12	6, 11	cfv 5259	. . . . 5 class ( +g ` g )
13	9, 10, 12	co 5925	. . . 4 class ( x ( +g ` g ) y )
14	4, 5, 8, 8, 13	cmpo 5927	. . 3 class ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) )
15	2, 3, 14	cmpt 4095	. 2 class ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
16	1, 15	wceq 1364	1 wff +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )

This definition is referenced by:  plusffvalg  13064