Theorem mndfo

Description: The addition operation of a monoid is an onto function (assuming it is a function). (Contributed by Mario Carneiro, 11-Oct-2013) (Proof shortened by AV, 23-Jan-2020)

	Ref	Expression
Hypotheses	mndfo.b	$$⊢B={\mathrm{Base}}_G$$
	mndfo.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	mndfo	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		mndfo.b	$$⊢B={\mathrm{Base}}_G$$
2		mndfo.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		eqid	$$⊢{+}_{𝑓}\left(G\right)={+}_{𝑓}\left(G\right)$$
4	1 3	mndpfo	$$⊢G\in \mathrm{Mnd}\to {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B$$
5	4	adantr	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B$$
6	1 2 3	plusfeq	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\to {+}_{𝑓}\left(G\right)=\underset{\dot{}}{+}$$
7	6	eqcomd	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\to \underset{\dot{}}{+}={+}_{𝑓}\left(G\right)$$
8	7	adantl	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{+}={+}_{𝑓}\left(G\right)$$
9		foeq1	$$⊢\underset{\dot{}}{+}={+}_{𝑓}\left(G\right)\to \left(\underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B\leftrightarrow {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B\right)$$
10	8 9	syl	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \left(\underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B\leftrightarrow {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B\right)$$
11	5 10	mpbird	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B$$