Definition df-plusf

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 ), while +g only has closure ( mgmcl ). (Contributed by Mario Carneiro, 14-Aug-2015)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplusf	|- +f
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	7	cv	|- y
12	8 11 10	co	|- ( x ( +g ` g ) y )
13	3 7 6 6 12	cmpo	|- ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) )
14	1 2 13	cmpt	|- ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
15	0 14	wceq	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )