Theorem nelsubgcld

Description: A non-subgroup-member plus 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$$
	nelsubgcld.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	nelsubgcld	$$⊢\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		nelsubgcld.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	4 6	grpcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
12	1 7 10 11	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$
13	3	eldifbd	$$⊢\phi \to \neg X\in S$$
14		eqid	$$⊢{-}_G={-}_G$$
15	4 6 14	grppncan	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}Y\right){-}_{G}Y=X$$
16	1 7 10 15	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right){-}_{G}Y=X$$
17	16	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in S\right)\to \left(X\underset{\dot{}}{+}Y\right){-}_{G}Y=X$$
18	2	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in S\right)\to S\in \mathrm{SubGrp}\left(G\right)$$
19		simpr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in S\right)\to X\underset{\dot{}}{+}Y\in S$$
20	5	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in S\right)\to Y\in S$$
21	14	subgsubcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge X\underset{\dot{}}{+}Y\in S\wedge Y\in S\right)\to \left(X\underset{\dot{}}{+}Y\right){-}_{G}Y\in S$$
22	18 19 20 21	syl3anc	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in S\right)\to \left(X\underset{\dot{}}{+}Y\right){-}_{G}Y\in S$$
23	17 22	eqeltrrd	$$⊢\left(\phi \wedge X\underset{\dot{}}{+}Y\in S\right)\to X\in S$$
24	13 23	mtand	$$⊢\phi \to \neg X\underset{\dot{}}{+}Y\in S$$
25	12 24	eldifd	$$⊢\phi \to X\underset{\dot{}}{+}Y\in \left(B\setminus S\right)$$