Database
BASIC ALGEBRAIC STRUCTURES
Groups
Definition and basic properties
grpplusfo
Metamath Proof Explorer
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 → 𝐵 )