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 ` G )
	grpsubcld.g	|- ( ph -> G e. Grp )
	grpsubcld.x	|- ( ph -> X e. B )
	grpsubcld.y	|- ( ph -> Y e. B )
Assertion	grpsubcld	|- ( ph -> ( X .- Y ) e. B )

Proof

Step	Hyp	Ref	Expression
1		grpsubcld.b	|- B = ( Base ` G )
2		grpsubcld.m	|- .- = ( -g ` G )
3		grpsubcld.g	|- ( ph -> G e. Grp )
4		grpsubcld.x	|- ( ph -> X e. B )
5		grpsubcld.y	|- ( ph -> Y e. B )
6	1 2	grpsubcl	|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) e. B )
7	3 4 5 6	syl3anc	|- ( ph -> ( X .- Y ) e. B )