Metamath Proof Explorer


Theorem grpplusfo

Description: The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006) (Revised by AV, 30-Aug-2021)

Ref Expression
Hypotheses grpplusf.1 𝐵 = ( Base ‘ 𝐺 )
grpplusf.2 𝐹 = ( +𝑓𝐺 )
Assertion grpplusfo ( 𝐺 ∈ Grp → 𝐹 : ( 𝐵 × 𝐵 ) –onto𝐵 )

Proof

Step Hyp Ref Expression
1 grpplusf.1 𝐵 = ( Base ‘ 𝐺 )
2 grpplusf.2 𝐹 = ( +𝑓𝐺 )
3 grpmnd ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
4 1 2 mndpfo ( 𝐺 ∈ Mnd → 𝐹 : ( 𝐵 × 𝐵 ) –onto𝐵 )
5 3 4 syl ( 𝐺 ∈ Grp → 𝐹 : ( 𝐵 × 𝐵 ) –onto𝐵 )