Theorem mndplusf

Description: The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015) (Proof shortened by AV, 3-Feb-2020)

	Ref	Expression
Hypotheses	mndplusf.1	$$⊢B={\mathrm{Base}}_G$$
	mndplusf.2	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
Assertion	mndplusf	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{⨣}:B\times B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mndplusf.1	$$⊢B={\mathrm{Base}}_G$$
2		mndplusf.2	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
3		mndmgm	$$⊢G\in \mathrm{Mnd}\to G\in \mathrm{Mgm}$$
4	1 2	mgmplusf	$$⊢G\in \mathrm{Mgm}\to \underset{\dot{}}{⨣}:B\times B⟶B$$
5	3 4	syl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{⨣}:B\times B⟶B$$