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 ⊢ B = Base G
mndpf.p ⊢ ⨣ ˙ = + 𝑓 ⁡ G
Assertion mndpfo ⊢ G ∈ Mnd → ⨣ ˙ : B × B ⟶ onto B

Proof

Step Hyp Ref Expression
1 mndpf.b ⊢ B = Base G
2 mndpf.p ⊢ ⨣ ˙ = + 𝑓 ⁡ G
3 1 2 mndplusf ⊢ G ∈ Mnd → ⨣ ˙ : B × B ⟶ B
4 simpr ⊢ G ∈ Mnd ∧ x ∈ B → x ∈ B
5 eqid ⊢ 0 G = 0 G
6 1 5 mndidcl ⊢ G ∈ Mnd → 0 G ∈ B
7 6 adantr ⊢ G ∈ Mnd ∧ x ∈ B → 0 G ∈ B
8 eqid ⊢ + G = + G
9 1 8 5 mndrid ⊢ G ∈ Mnd ∧ x ∈ B → x + G 0 G = x
10 9 eqcomd ⊢ G ∈ Mnd ∧ x ∈ B → x = x + G 0 G
11 rspceov ⊢ x ∈ B ∧ 0 G ∈ B ∧ x = x + G 0 G → ∃ y ∈ B ∃ z ∈ B x = y + G z
12 4 7 10 11 syl3anc ⊢ G ∈ Mnd ∧ x ∈ B → ∃ y ∈ B ∃ z ∈ B x = y + G z
13 1 8 2 plusfval ⊢ y ∈ B ∧ z ∈ B → y ⨣ ˙ z = y + G z
14 13 eqeq2d ⊢ y ∈ B ∧ z ∈ B → x = y ⨣ ˙ z ↔ x = y + G z
15 14 2rexbiia ⊢ ∃ y ∈ B ∃ z ∈ B x = y ⨣ ˙ z ↔ ∃ y ∈ B ∃ z ∈ B x = y + G z
16 12 15 sylibr ⊢ G ∈ Mnd ∧ x ∈ B → ∃ y ∈ B ∃ z ∈ B x = y ⨣ ˙ z
17 16 ralrimiva ⊢ G ∈ Mnd → ∀ x ∈ B ∃ y ∈ B ∃ z ∈ B x = y ⨣ ˙ z
18 foov ⊢ ⨣ ˙ : B × B ⟶ onto B ↔ ⨣ ˙ : B × B ⟶ B ∧ ∀ x ∈ B ∃ y ∈ B ∃ z ∈ B x = y ⨣ ˙ z
19 3 17 18 sylanbrc ⊢ G ∈ Mnd → ⨣ ˙ : B × B ⟶ onto B