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, 17-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mndfo.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
| mndfo.p | ⊢ + = ( +g ‘ 𝐺 ) | ||
| Assertion | mndfo | ⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mndfo.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
| 2 | mndfo.p | ⊢ + = ( +g ‘ 𝐺 ) | |
| 3 | mndmgm | ⊢ ( 𝐺 ∈ Mnd → 𝐺 ∈ Mgm ) | |
| 4 | 3 | adantr | ⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → 𝐺 ∈ Mgm ) |
| 5 | 1 2 | mndid | ⊢ ( 𝐺 ∈ Mnd → ∃ 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ) |
| 6 | 5 | adantr | ⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ) |
| 7 | simpr | ⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → + Fn ( 𝐵 × 𝐵 ) ) | |
| 8 | 1 2 4 6 7 | mgmfod | ⊢ ( ( 𝐺 ∈ Mnd ∧ + Fn ( 𝐵 × 𝐵 ) ) → + : ( 𝐵 × 𝐵 ) –onto→ 𝐵 ) |