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

Definition df-plusf 17010
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 17020), while +g only has closure (mgmcl 17014). (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 17008 . 2 class +𝑓
2 vg . . 3 setvar 𝑔
3 cvv 3172 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1473 . . . . 5 class 𝑔
7 cbs 15641 . . . . 5 class Base
86, 7cfv 5790 . . . 4 class (Base‘𝑔)
94cv 1473 . . . . 5 class 𝑥
105cv 1473 . . . . 5 class 𝑦
11 cplusg 15714 . . . . . 6 class +g
126, 11cfv 5790 . . . . 5 class (+g𝑔)
139, 10, 12co 6527 . . . 4 class (𝑥(+g𝑔)𝑦)
144, 5, 8, 8, 13cmpt2 6529 . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦))
152, 3, 14cmpt 4637 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦)))
161, 15wceq 1474 1 wff +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  plusffval  17016
  Copyright terms: Public domain W3C validator