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

Proof

Step	Hyp	Ref	Expression
1		nelsubginvcld.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
2		nelsubginvcld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
3		nelsubginvcld.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑆 ) )
4		nelsubginvcld.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
5		nelsubgcld.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
6		nelsubgcld.p	⊢ + = ( +g ‘ 𝐺 )
7	3	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8	4	subgss	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
9	2 8	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
10	9 5	sseldd	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
11	4 6	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
12	1 7 10 11	syl3anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
13	3	eldifbd	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑆 )
14		eqid	⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
15	4 6 14	grppncan	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝐺 ) 𝑌 ) = 𝑋 )
16	1 7 10 15	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝐺 ) 𝑌 ) = 𝑋 )
17	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑆 ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝐺 ) 𝑌 ) = 𝑋 )
18	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
19		simpr	⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )
20	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑆 ) → 𝑌 ∈ 𝑆 )
21	14	subgsubcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 + 𝑌 ) ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝐺 ) 𝑌 ) ∈ 𝑆 )
22	18 19 20 21	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑆 ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝐺 ) 𝑌 ) ∈ 𝑆 )
23	17 22	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
24	13 23	mtand	⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) ∈ 𝑆 )
25	12 24	eldifd	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐵 ∖ 𝑆 ) )