This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑔 ) 𝑦 ) ) )