Theorem nelsubginvcld

Description: The inverse of a non-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$$
	nelsubginvcld.p	$$⊢N={inv}_g\left(G\right)$$
Assertion	nelsubginvcld	$$⊢\phi \to N\left(X\right)\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		nelsubginvcld.p	$$⊢N={inv}_g\left(G\right)$$
6	3	eldifad	$$⊢\phi \to X\in B$$
7	4 5	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in B$$
8	1 6 7	syl2anc	$$⊢\phi \to N\left(X\right)\in B$$
9	3	eldifbd	$$⊢\phi \to \neg X\in S$$
10	4 5	grpinvinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(N\left(X\right)\right)=X$$
11	1 6 10	syl2anc	$$⊢\phi \to N\left(N\left(X\right)\right)=X$$
12	11	adantr	$$⊢\left(\phi \wedge N\left(X\right)\in S\right)\to N\left(N\left(X\right)\right)=X$$
13	5	subginvcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge N\left(X\right)\in S\right)\to N\left(N\left(X\right)\right)\in S$$
14	2 13	sylan	$$⊢\left(\phi \wedge N\left(X\right)\in S\right)\to N\left(N\left(X\right)\right)\in S$$
15	12 14	eqeltrrd	$$⊢\left(\phi \wedge N\left(X\right)\in S\right)\to X\in S$$
16	9 15	mtand	$$⊢\phi \to \neg N\left(X\right)\in S$$
17	8 16	eldifd	$$⊢\phi \to N\left(X\right)\in \left(B\setminus S\right)$$