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 φGGrp
nelsubginvcld.s φSSubGrpG
nelsubginvcld.x φXBS
nelsubginvcld.b B=BaseG
nelsubgcld.y φYS
nelsubgsubcld.p -˙=-G
Assertion nelsubgsubcld φX-˙YBS

Proof

Step Hyp Ref Expression
1 nelsubginvcld.g φGGrp
2 nelsubginvcld.s φSSubGrpG
3 nelsubginvcld.x φXBS
4 nelsubginvcld.b B=BaseG
5 nelsubgcld.y φYS
6 nelsubgsubcld.p -˙=-G
7 3 eldifad φXB
8 4 subgss SSubGrpGSB
9 2 8 syl φSB
10 9 5 sseldd φYB
11 eqid +G=+G
12 eqid invgG=invgG
13 4 11 12 6 grpsubval XBYBX-˙Y=X+GinvgGY
14 7 10 13 syl2anc φX-˙Y=X+GinvgGY
15 12 subginvcl SSubGrpGYSinvgGYS
16 2 5 15 syl2anc φinvgGYS
17 1 2 3 4 16 11 nelsubgcld φX+GinvgGYBS
18 14 17 eqeltrd φX-˙YBS