Theorem mndpfoOLD

Description: Obsolete version of mndpfo as of 17-Aug-2026. The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 11-Oct-2013) (Revised by AV, 23-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		mndpfoOLD.b	$$⊢B={\mathrm{Base}}_G$$
2		mndpfoOLD.p	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
3	1 2	mndplusf	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{⨣}:B\times B⟶B$$
4		simpr	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\right)\to x\in B$$
5		eqid	$$⊢0_G=0_G$$
6	1 5	mndidcl	$$⊢G\in \mathrm{Mnd}\to 0_G\in B$$
7	6	adantr	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\right)\to 0_G\in B$$
8		eqid	$$⊢{+}_G={+}_G$$
9	1 8 5	mndrid	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\right)\to x{+}_G{0}_G=x$$
10	9	eqcomd	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\right)\to x=x{+}_G{0}_G$$
11		rspceov	$$⊢\left(x\in B\wedge 0_G\in B\wedge x=x{+}_G{0}_G\right)\to \exists y\in B\exists z\in Bx=y{+}_{G}z$$
12	4 7 10 11	syl3anc	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\right)\to \exists y\in B\exists z\in Bx=y{+}_{G}z$$
13	1 8 2	plusfval	$$⊢\left(y\in B\wedge z\in B\right)\to y\underset{\dot{}}{⨣}z=y{+}_{G}z$$
14	13	eqeq2d	$$⊢\left(y\in B\wedge z\in B\right)\to \left(x=y\underset{\dot{}}{⨣}z\leftrightarrow x=y{+}_{G}z\right)$$
15	14	2rexbiia	$$⊢\exists y\in B\exists z\in Bx=y\underset{\dot{}}{⨣}z\leftrightarrow \exists y\in B\exists z\in Bx=y{+}_{G}z$$
16	12 15	sylibr	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\right)\to \exists y\in B\exists z\in Bx=y\underset{\dot{}}{⨣}z$$
17	16	ralrimiva	$$⊢G\in \mathrm{Mnd}\to \forall x\in B\exists y\in B\exists z\in Bx=y\underset{\dot{}}{⨣}z$$
18		foov	$$⊢\underset{\dot{}}{⨣}:B\times B\underset{onto}{⟶}B\leftrightarrow \left(\underset{\dot{}}{⨣}:B\times B⟶B\wedge \forall x\in B\exists y\in B\exists z\in Bx=y\underset{\dot{}}{⨣}z\right)$$
19	3 17 18	sylanbrc	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{⨣}:B\times B\underset{onto}{⟶}B$$