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 ⊢ B = Base G
grpsubcld.m ⊢ - ˙ = - G
grpsubcld.g ⊢ φ → G ∈ Grp
grpsubcld.x ⊢ φ → X ∈ B
grpsubcld.y ⊢ φ → Y ∈ B
Assertion grpsubcld ⊢ φ → X - ˙ Y ∈ B

Proof

Step Hyp Ref Expression
1 grpsubcld.b ⊢ B = Base G
2 grpsubcld.m ⊢ - ˙ = - G
3 grpsubcld.g ⊢ φ → G ∈ Grp
4 grpsubcld.x ⊢ φ → X ∈ B
5 grpsubcld.y ⊢ φ → Y ∈ B
6 1 2 grpsubcl ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → X - ˙ Y ∈ B
7 3 4 5 6 syl3anc ⊢ φ → X - ˙ Y ∈ B