Metamath Proof Explorer


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 ) )