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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mndfo.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	mndfo	⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mndfo.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mndfo.p	⊢ + = ( +g ‘ 𝐺 )
3		eqid	⊢ ( +𝑓 ‘ 𝐺 ) = ( +𝑓 ‘ 𝐺 )
4	1 3	mndpfo	⊢ ( 𝐺 ∈ Mnd → ( +𝑓 ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )
5	4	adantr	⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → ( +𝑓 ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )
6	1 2 3	plusfeq	⊢ ( + Fn ( 𝐵 × 𝐵 ) → ( +𝑓 ‘ 𝐺 ) = + )
7	6	eqcomd	⊢ ( + Fn ( 𝐵 × 𝐵 ) → + = ( +𝑓 ‘ 𝐺 ) )
8	7	adantl	⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → + = ( +𝑓 ‘ 𝐺 ) )
9		foeq1	⊢ ( + = ( +𝑓 ‘ 𝐺 ) → ( + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ↔ ( +𝑓 ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ) )
10	8 9	syl	⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → ( + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ↔ ( +𝑓 ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ) )
11	5 10	mpbird	⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )