This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Groups Definition and basic properties 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 → 𝐵 )