Theorem grpplusfo

Description: The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	grpplusf.1	$$⊢B={\mathrm{Base}}_G$$
	grpplusf.2	$$⊢F={+}_{𝑓}\left(G\right)$$
Assertion	grpplusfo	$$⊢G\in \mathrm{Grp}\to F:B\times B\underset{onto}{⟶}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	mndpfo	$$⊢G\in \mathrm{Mnd}\to F:B\times B\underset{onto}{⟶}B$$
5	3 4	syl	$$⊢G\in \mathrm{Grp}\to F:B\times B\underset{onto}{⟶}B$$