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