Theorem subgsubcld

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

	Ref	Expression
Hypotheses	subgsubcld.m	|- .- = ( -g ` G )
	subgsubcld.s	|- ( ph -> S e. ( SubGrp ` G ) )
	subgsubcld.x	|- ( ph -> X e. S )
	subgsubcld.y	|- ( ph -> Y e. S )
Assertion	subgsubcld	|- ( ph -> ( X .- Y ) e. S )

Proof

Step	Hyp	Ref	Expression
1		subgsubcld.m	|- .- = ( -g ` G )
2		subgsubcld.s	|- ( ph -> S e. ( SubGrp ` G ) )
3		subgsubcld.x	|- ( ph -> X e. S )
4		subgsubcld.y	|- ( ph -> Y e. S )
5	1	subgsubcl	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) e. S )
6	2 3 4 5	syl3anc	|- ( ph -> ( X .- Y ) e. S )