Metamath Proof Explorer


Theorem plusfeq

Description: If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses plusffval.1 B = Base G
plusffval.2 + ˙ = + G
plusffval.3 ˙ = + 𝑓 G
Assertion plusfeq + ˙ Fn B × B ˙ = + ˙

Proof

Step Hyp Ref Expression
1 plusffval.1 B = Base G
2 plusffval.2 + ˙ = + G
3 plusffval.3 ˙ = + 𝑓 G
4 1 2 3 plusffval ˙ = x B , y B x + ˙ y
5 fnov + ˙ Fn B × B + ˙ = x B , y B x + ˙ y
6 5 biimpi + ˙ Fn B × B + ˙ = x B , y B x + ˙ y
7 4 6 eqtr4id + ˙ Fn B × B ˙ = + ˙