Theorem nelsubgsubcld

Description: A non-subgroup-member minus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023)

	Ref	Expression
Hypotheses	nelsubginvcld.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	nelsubginvcld.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
	nelsubginvcld.x	$$⊢\phi \to X\in \left(B\setminus S\right)$$
	nelsubginvcld.b	$$⊢B={\mathrm{Base}}_G$$
	nelsubgcld.y	$$⊢\phi \to Y\in S$$
	nelsubgsubcld.p	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	nelsubgsubcld	$$⊢\phi \to X\underset{\dot{}}{-}Y\in \left(B\setminus S\right)$$

Proof

Step	Hyp	Ref	Expression
1		nelsubginvcld.g	$$⊢\phi \to G\in \mathrm{Grp}$$
2		nelsubginvcld.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
3		nelsubginvcld.x	$$⊢\phi \to X\in \left(B\setminus S\right)$$
4		nelsubginvcld.b	$$⊢B={\mathrm{Base}}_G$$
5		nelsubgcld.y	$$⊢\phi \to Y\in S$$
6		nelsubgsubcld.p	$$⊢\underset{\dot{}}{-}={-}_G$$
7	3	eldifad	$$⊢\phi \to X\in B$$
8	4	subgss	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\subseteq B$$
9	2 8	syl	$$⊢\phi \to S\subseteq B$$
10	9 5	sseldd	$$⊢\phi \to Y\in B$$
11		eqid	$$⊢{+}_G={+}_G$$
12		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
13	4 11 12 6	grpsubval	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X{+}_G{inv}_g\left(G\right)\left(Y\right)$$
14	7 10 13	syl2anc	$$⊢\phi \to X\underset{\dot{}}{-}Y=X{+}_G{inv}_g\left(G\right)\left(Y\right)$$
15	12	subginvcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge Y\in S\right)\to {inv}_g\left(G\right)\left(Y\right)\in S$$
16	2 5 15	syl2anc	$$⊢\phi \to {inv}_g\left(G\right)\left(Y\right)\in S$$
17	1 2 3 4 16 11	nelsubgcld	$$⊢\phi \to X{+}_G{inv}_g\left(G\right)\left(Y\right)\in \left(B\setminus S\right)$$
18	14 17	eqeltrd	$$⊢\phi \to X\underset{\dot{}}{-}Y\in \left(B\setminus S\right)$$