Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-plusf Structured version   Visualization version   GIF version

Definition df-plusf 17064
 Description: Define group addition function. Usually we will use +g directly instead of +𝑓, and they have the same behavior in most cases. The main advantage of +𝑓 for any magma is that it is a guaranteed function (mgmplusf 17074), while +g only has closure (mgmcl 17068). (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df-plusf +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦)))
Distinct variable group:   𝑥,𝑔,𝑦

Detailed syntax breakdown of Definition df-plusf
StepHypRef Expression
1 cplusf 17062 . 2 class +𝑓
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1474 . . . . 5 class 𝑔
7 cbs 15695 . . . . 5 class Base
86, 7cfv 5804 . . . 4 class (Base‘𝑔)
94cv 1474 . . . . 5 class 𝑥
105cv 1474 . . . . 5 class 𝑦
11 cplusg 15768 . . . . . 6 class +g
126, 11cfv 5804 . . . . 5 class (+g𝑔)
139, 10, 12co 6549 . . . 4 class (𝑥(+g𝑔)𝑦)
144, 5, 8, 8, 13cmpt2 6551 . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦))
152, 3, 14cmpt 4643 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦)))
161, 15wceq 1475 1 wff +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦)))
 Colors of variables: wff setvar class This definition is referenced by:  plusffval  17070
 Copyright terms: Public domain W3C validator