Step |
Hyp |
Ref |
Expression |
1 |
|
subgsubcl.p |
|- .- = ( -g ` G ) |
2 |
|
subgsub.h |
|- H = ( G |`s S ) |
3 |
|
subgsub.n |
|- N = ( -g ` H ) |
4 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
5 |
2 4
|
ressplusg |
|- ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) ) |
6 |
5
|
3ad2ant1 |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( +g ` G ) = ( +g ` H ) ) |
7 |
|
eqidd |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X = X ) |
8 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
9 |
|
eqid |
|- ( invg ` H ) = ( invg ` H ) |
10 |
2 8 9
|
subginv |
|- ( ( S e. ( SubGrp ` G ) /\ Y e. S ) -> ( ( invg ` G ) ` Y ) = ( ( invg ` H ) ` Y ) ) |
11 |
10
|
3adant2 |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( ( invg ` G ) ` Y ) = ( ( invg ` H ) ` Y ) ) |
12 |
6 7 11
|
oveq123d |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) = ( X ( +g ` H ) ( ( invg ` H ) ` Y ) ) ) |
13 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
14 |
13
|
subgss |
|- ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) ) |
15 |
14
|
3ad2ant1 |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> S C_ ( Base ` G ) ) |
16 |
|
simp2 |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. S ) |
17 |
15 16
|
sseldd |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. ( Base ` G ) ) |
18 |
|
simp3 |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. S ) |
19 |
15 18
|
sseldd |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. ( Base ` G ) ) |
20 |
13 4 8 1
|
grpsubval |
|- ( ( X e. ( Base ` G ) /\ Y e. ( Base ` G ) ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) ) |
21 |
17 19 20
|
syl2anc |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) ) |
22 |
2
|
subgbas |
|- ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) ) |
23 |
22
|
3ad2ant1 |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> S = ( Base ` H ) ) |
24 |
16 23
|
eleqtrd |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. ( Base ` H ) ) |
25 |
18 23
|
eleqtrd |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. ( Base ` H ) ) |
26 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
27 |
|
eqid |
|- ( +g ` H ) = ( +g ` H ) |
28 |
26 27 9 3
|
grpsubval |
|- ( ( X e. ( Base ` H ) /\ Y e. ( Base ` H ) ) -> ( X N Y ) = ( X ( +g ` H ) ( ( invg ` H ) ` Y ) ) ) |
29 |
24 25 28
|
syl2anc |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X N Y ) = ( X ( +g ` H ) ( ( invg ` H ) ` Y ) ) ) |
30 |
12 21 29
|
3eqtr4d |
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) = ( X N Y ) ) |