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	$$⊢{+}_{𝑓}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_{g}y\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplusf	$$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	7	cv	$$setvary$$
12	8 11 10	co	$$class\left(x{+}_{g}y\right)$$
13	3 7 6 6 12	cmpo	$$class\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_{g}y\right)$$
14	1 2 13	cmpt	$$class\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_{g}y\right)\right)$$
15	0 14	wceq	$$wff{+}_{𝑓}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{+}_{g}y\right)\right)$$