This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐵 )