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

Metamath Proof Explorer

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