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	⊢ +𝑓 = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplusf	⊢ +𝑓
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Base ‘ 𝑔 )
7		vy	⊢ 𝑦
8	3	cv	⊢ 𝑥
9		cplusg	⊢ +g
10	5 9	cfv	⊢ ( +g ‘ 𝑔 )
11	7	cv	⊢ 𝑦
12	8 11 10	co	⊢ ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 )
13	3 7 6 6 12	cmpo	⊢ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) )
14	1 2 13	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) )
15	0 14	wceq	⊢ +𝑓 = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) )