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

Definition df-plusf 17922
 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 17933), while +g only has closure (mgmcl 17926). (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 17920 . 2 class +𝑓
2 vg . . 3 setvar 𝑔
3 cvv 3409 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1537 . . . . 5 class 𝑔
7 cbs 16546 . . . . 5 class Base
86, 7cfv 6339 . . . 4 class (Base‘𝑔)
94cv 1537 . . . . 5 class 𝑥
105cv 1537 . . . . 5 class 𝑦
11 cplusg 16628 . . . . . 6 class +g
126, 11cfv 6339 . . . . 5 class (+g𝑔)
139, 10, 12co 7155 . . . 4 class (𝑥(+g𝑔)𝑦)
144, 5, 8, 8, 13cmpo 7157 . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦))
152, 3, 14cmpt 5115 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦)))
161, 15wceq 1538 1 wff +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦)))
 Colors of variables: wff setvar class This definition is referenced by:  plusffval  17929
 Copyright terms: Public domain W3C validator