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

Metamath Proof Explorer

Theorem grpsubcld

Description: Closure of group subtraction. (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses grpsubcld.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grpsubcld.m ⊢ − = ( -g ‘ 𝐺 )
grpsubcld.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
grpsubcld.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
grpsubcld.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion grpsubcld ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 grpsubcld.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpsubcld.m ⊢ − = ( -g ‘ 𝐺 )
3 grpsubcld.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
4 grpsubcld.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 grpsubcld.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 1 2 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) ∈ 𝐵 )
7 3 4 5 6 syl3anc ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ 𝐵 )