Theorem grpplusf

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

	Ref	Expression
Hypotheses	grpplusf.1	$$⊢B={\mathrm{Base}}_G$$
	grpplusf.2	$$⊢F={+}_{𝑓}\left(G\right)$$
Assertion	grpplusf	$$⊢G\in \mathrm{Grp}\to F:B\times B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		grpplusf.1	$$⊢B={\mathrm{Base}}_G$$
2		grpplusf.2	$$⊢F={+}_{𝑓}\left(G\right)$$
3		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
4	1 2	mndplusf	$$⊢G\in \mathrm{Mnd}\to F:B\times B⟶B$$
5	3 4	syl	$$⊢G\in \mathrm{Grp}\to F:B\times B⟶B$$