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
|- +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 ) ) )