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 𝐵 = ( Base ‘ 𝐺 )
plusffval.2 + = ( +g𝐺 )
plusffval.3 = ( +𝑓𝐺 )
Assertion plusfeq ( + Fn ( 𝐵 × 𝐵 ) → = + )

Proof

Step Hyp Ref Expression
1 plusffval.1 𝐵 = ( Base ‘ 𝐺 )
2 plusffval.2 + = ( +g𝐺 )
3 plusffval.3 = ( +𝑓𝐺 )
4 1 2 3 plusffval = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + 𝑦 ) )
5 fnov ( + Fn ( 𝐵 × 𝐵 ) ↔ + = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + 𝑦 ) ) )
6 5 biimpi ( + Fn ( 𝐵 × 𝐵 ) → + = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + 𝑦 ) ) )
7 4 6 eqtr4id ( + Fn ( 𝐵 × 𝐵 ) → = + )