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={\mathrm{Base}}_G$$
	plusffval.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	plusffval.3	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
Assertion	plusfeq	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\to \underset{\dot{}}{⨣}=\underset{\dot{}}{+}$$

Proof

Step	Hyp	Ref	Expression
1		plusffval.1	$$⊢B={\mathrm{Base}}_G$$
2		plusffval.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		plusffval.3	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
4	1 2 3	plusffval	$$⊢\underset{\dot{}}{⨣}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$
5		fnov	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\leftrightarrow \underset{\dot{}}{+}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$
6	5	biimpi	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\to \underset{\dot{}}{+}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$
7	4 6	eqtr4id	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\to \underset{\dot{}}{⨣}=\underset{\dot{}}{+}$$