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, 17-Aug-2026)

	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		mndmgm	$$⊢G\in \mathrm{Mnd}\to G\in \mathrm{Mgm}$$
4	3	adantr	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to G\in \mathrm{Mgm}$$
5	1 2	mndid	$$⊢G\in \mathrm{Mnd}\to \exists u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$
6	5	adantr	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \exists u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$
7		simpr	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{+}Fn\left(B\times B\right)$$
8	1 2 4 6 7	mgmfod	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B$$