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	|- ( ph -> G e. Grp )
	nelsubginvcld.s	|- ( ph -> S e. ( SubGrp ` G ) )
	nelsubginvcld.x	|- ( ph -> X e. ( B \ S ) )
	nelsubginvcld.b	|- B = ( Base ` G )
	nelsubgcld.y	|- ( ph -> Y e. S )
	nelsubgcld.p	|- .+ = ( +g ` G )
Assertion	nelsubgcld	|- ( ph -> ( X .+ Y ) e. ( B \ S ) )

Proof

Step	Hyp	Ref	Expression
1		nelsubginvcld.g	|- ( ph -> G e. Grp )
2		nelsubginvcld.s	|- ( ph -> S e. ( SubGrp ` G ) )
3		nelsubginvcld.x	|- ( ph -> X e. ( B \ S ) )
4		nelsubginvcld.b	|- B = ( Base ` G )
5		nelsubgcld.y	|- ( ph -> Y e. S )
6		nelsubgcld.p	|- .+ = ( +g ` G )
7	3	eldifad	|- ( ph -> X e. B )
8	4	subgss	|- ( S e. ( SubGrp ` G ) -> S C_ B )
9	2 8	syl	|- ( ph -> S C_ B )
10	9 5	sseldd	|- ( ph -> Y e. B )
11	4 6	grpcl	|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
12	1 7 10 11	syl3anc	|- ( ph -> ( X .+ Y ) e. B )
13	3	eldifbd	|- ( ph -> -. X e. S )
14		eqid	|- ( -g ` G ) = ( -g ` G )
15	4 6 14	grppncan	|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) ( -g ` G ) Y ) = X )
16	1 7 10 15	syl3anc	|- ( ph -> ( ( X .+ Y ) ( -g ` G ) Y ) = X )
17	16	adantr	|- ( ( ph /\ ( X .+ Y ) e. S ) -> ( ( X .+ Y ) ( -g ` G ) Y ) = X )
18	2	adantr	|- ( ( ph /\ ( X .+ Y ) e. S ) -> S e. ( SubGrp ` G ) )
19		simpr	|- ( ( ph /\ ( X .+ Y ) e. S ) -> ( X .+ Y ) e. S )
20	5	adantr	|- ( ( ph /\ ( X .+ Y ) e. S ) -> Y e. S )
21	14	subgsubcl	|- ( ( S e. ( SubGrp ` G ) /\ ( X .+ Y ) e. S /\ Y e. S ) -> ( ( X .+ Y ) ( -g ` G ) Y ) e. S )
22	18 19 20 21	syl3anc	|- ( ( ph /\ ( X .+ Y ) e. S ) -> ( ( X .+ Y ) ( -g ` G ) Y ) e. S )
23	17 22	eqeltrrd	|- ( ( ph /\ ( X .+ Y ) e. S ) -> X e. S )
24	13 23	mtand	|- ( ph -> -. ( X .+ Y ) e. S )
25	12 24	eldifd	|- ( ph -> ( X .+ Y ) e. ( B \ S ) )