Theorem subgsubcld

Description: A subgroup is closed under group subtraction. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	subgsubcld.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	subgsubcld.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
	subgsubcld.x	$$⊢\phi \to X\in S$$
	subgsubcld.y	$$⊢\phi \to Y\in S$$
Assertion	subgsubcld	$$⊢\phi \to X\underset{\dot{}}{-}Y\in S$$

Proof

Step	Hyp	Ref	Expression
1		subgsubcld.m	$$⊢\underset{\dot{}}{-}={-}_G$$
2		subgsubcld.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
3		subgsubcld.x	$$⊢\phi \to X\in S$$
4		subgsubcld.y	$$⊢\phi \to Y\in S$$
5	1	subgsubcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge X\in S\wedge Y\in S\right)\to X\underset{\dot{}}{-}Y\in S$$
6	2 3 4 5	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Y\in S$$