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	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	nelsubginvcld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
	nelsubginvcld.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑆 ) )
	nelsubginvcld.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	nelsubginvcld.p	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	nelsubginvcld	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ ( 𝐵 ∖ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		nelsubginvcld.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
2		nelsubginvcld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
3		nelsubginvcld.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑆 ) )
4		nelsubginvcld.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
5		nelsubginvcld.p	⊢ 𝑁 = ( invg ‘ 𝐺 )
6	3	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7	4 5	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
8	1 6 7	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
9	3	eldifbd	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑆 )
10	4 5	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
11	1 6 10	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
12	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
13	5	subginvcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝑆 )
14	2 13	sylan	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝑆 )
15	12 14	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
16	9 15	mtand	⊢ ( 𝜑 → ¬ ( 𝑁 ‘ 𝑋 ) ∈ 𝑆 )
17	8 16	eldifd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ ( 𝐵 ∖ 𝑆 ) )