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	|- ( 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 )
	nelsubgsubcld.p	|- .- = ( -g ` G )
Assertion	nelsubgsubcld	|- ( 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		nelsubgsubcld.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		eqid	|- ( +g ` G ) = ( +g ` G )
12		eqid	|- ( invg ` G ) = ( invg ` G )
13	4 11 12 6	grpsubval	|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
14	7 10 13	syl2anc	|- ( ph -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
15	12	subginvcl	|- ( ( S e. ( SubGrp ` G ) /\ Y e. S ) -> ( ( invg ` G ) ` Y ) e. S )
16	2 5 15	syl2anc	|- ( ph -> ( ( invg ` G ) ` Y ) e. S )
17	1 2 3 4 16 11	nelsubgcld	|- ( ph -> ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) e. ( B \ S ) )
18	14 17	eqeltrd	|- ( ph -> ( X .- Y ) e. ( B \ S ) )