Metamath Proof Explorer


Theorem plusfval

Description: The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses plusffval.1 B=BaseG
plusffval.2 +˙=+G
plusffval.3 ˙=+𝑓G
Assertion plusfval XBYBX˙Y=X+˙Y

Proof

Step Hyp Ref Expression
1 plusffval.1 B=BaseG
2 plusffval.2 +˙=+G
3 plusffval.3 ˙=+𝑓G
4 oveq12 x=Xy=Yx+˙y=X+˙Y
5 1 2 3 plusffval ˙=xB,yBx+˙y
6 ovex X+˙YV
7 4 5 6 ovmpoa XBYBX˙Y=X+˙Y