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