Theorem mndpfo

Description: 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 shortened by AV, 17-Aug-2026)

	Ref	Expression
Hypotheses	mndpfo.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mndpfo.p	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
Assertion	mndpfo	⊢ ( 𝐺 ∈ Mnd → ⨣ : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mndpfo.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mndpfo.p	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4		mndmgm	⊢ ( 𝐺 ∈ Mnd → 𝐺 ∈ Mgm )
5	1 3	mndid	⊢ ( 𝐺 ∈ Mnd → ∃ 𝑖 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑖 ) = 𝑥 ) )
6	1 3 4 5 2	mgmidpfod	⊢ ( 𝐺 ∈ Mnd → ⨣ : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )