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)

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

Proof

Step	Hyp	Ref	Expression
1		mndpf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mndpf.p	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
3	1 2	mndplusf	⊢ ( 𝐺 ∈ Mnd → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
4		simpr	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
5		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6	1 5	mndidcl	⊢ ( 𝐺 ∈ Mnd → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
7	6	adantr	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
8		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
9	1 8 5	mndrid	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
10	9	eqcomd	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → 𝑥 = ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
11		rspceov	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 0g ‘ 𝐺 ) ∈ 𝐵 ∧ 𝑥 = ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) → ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
12	4 7 10 11	syl3anc	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
13	1 8 2	plusfval	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ⨣ 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
14	13	eqeq2d	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 = ( 𝑦 ⨣ 𝑧 ) ↔ 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
15	14	2rexbiia	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 ⨣ 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
16	12 15	sylibr	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 ⨣ 𝑧 ) )
17	16	ralrimiva	⊢ ( 𝐺 ∈ Mnd → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 ⨣ 𝑧 ) )
18		foov	⊢ ( ⨣ : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ↔ ( ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 ⨣ 𝑧 ) ) )
19	3 17 18	sylanbrc	⊢ ( 𝐺 ∈ Mnd → ⨣ : ( 𝐵 × 𝐵 ) –onto→ 𝐵 )