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	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	nelsubginvcld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
	nelsubginvcld.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑆 ) )
	nelsubginvcld.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	nelsubgcld.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
	nelsubgsubcld.p	⊢ − = ( -g ‘ 𝐺 )
Assertion	nelsubgsubcld	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ( 𝐵 ∖ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		nelsubginvcld.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
2		nelsubginvcld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
3		nelsubginvcld.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑆 ) )
4		nelsubginvcld.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
5		nelsubgcld.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
6		nelsubgsubcld.p	⊢ − = ( -g ‘ 𝐺 )
7	3	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8	4	subgss	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
9	2 8	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
10	9 5	sseldd	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
11		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
12		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
13	4 11 12 6	grpsubval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
14	7 10 13	syl2anc	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
15	12	subginvcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑌 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑆 )
16	2 5 15	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑆 )
17	1 2 3 4 16 11	nelsubgcld	⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ∈ ( 𝐵 ∖ 𝑆 ) )
18	14 17	eqeltrd	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ( 𝐵 ∖ 𝑆 ) )