Metamath Proof Explorer


Theorem grpsubcl

Description: Closure of group subtraction. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses grpsubcl.b 𝐵 = ( Base ‘ 𝐺 )
grpsubcl.m = ( -g𝐺 )
Assertion grpsubcl ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 grpsubcl.b 𝐵 = ( Base ‘ 𝐺 )
2 grpsubcl.m = ( -g𝐺 )
3 1 2 grpsubf ( 𝐺 ∈ Grp → : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
4 fovrn ( ( : ( 𝐵 × 𝐵 ) ⟶ 𝐵𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
5 3 4 syl3an1 ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )