Theorem plusfval

Description: The group addition operation as a function. (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	plusfval	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{⨣}Y=X\underset{\dot{}}{+}Y$$

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		oveq12	$$⊢\left(x=X\wedge y=Y\right)\to x\underset{\dot{}}{+}y=X\underset{\dot{}}{+}Y$$
5	1 2 3	plusffval	$$⊢\underset{\dot{}}{⨣}=\left(x\in B,y\in B⟼x\underset{\dot{}}{+}y\right)$$
6		ovex	$$⊢X\underset{\dot{}}{+}Y\in \mathrm{V}$$
7	4 5 6	ovmpoa	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{⨣}Y=X\underset{\dot{}}{+}Y$$