Step |
Hyp |
Ref |
Expression |
1 |
|
subgmulgcl.t |
|- .x. = ( .g ` G ) |
2 |
|
subgmulg.h |
|- H = ( G |`s S ) |
3 |
|
subgmulg.t |
|- .xb = ( .g ` H ) |
4 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
5 |
2 4
|
subg0 |
|- ( S e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) ) |
6 |
5
|
3ad2ant1 |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( 0g ` G ) = ( 0g ` H ) ) |
7 |
6
|
ifeq1d |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) ) |
8 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
9 |
2 8
|
ressplusg |
|- ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) ) |
10 |
9
|
3ad2ant1 |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( +g ` G ) = ( +g ` H ) ) |
11 |
10
|
seqeq2d |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ) |
12 |
11
|
adantr |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ) |
13 |
12
|
fveq1d |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) ) |
14 |
13
|
ifeq1d |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) = if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) |
15 |
|
simp2 |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> N e. ZZ ) |
16 |
15
|
zred |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> N e. RR ) |
17 |
|
0re |
|- 0 e. RR |
18 |
|
axlttri |
|- ( ( N e. RR /\ 0 e. RR ) -> ( N < 0 <-> -. ( N = 0 \/ 0 < N ) ) ) |
19 |
16 17 18
|
sylancl |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N < 0 <-> -. ( N = 0 \/ 0 < N ) ) ) |
20 |
|
ioran |
|- ( -. ( N = 0 \/ 0 < N ) <-> ( -. N = 0 /\ -. 0 < N ) ) |
21 |
19 20
|
bitrdi |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N < 0 <-> ( -. N = 0 /\ -. 0 < N ) ) ) |
22 |
21
|
biimpar |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> N < 0 ) |
23 |
|
simpl1 |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> S e. ( SubGrp ` G ) ) |
24 |
15
|
adantr |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> N e. ZZ ) |
25 |
24
|
znegcld |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> -u N e. ZZ ) |
26 |
16
|
lt0neg1d |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N < 0 <-> 0 < -u N ) ) |
27 |
26
|
biimpa |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> 0 < -u N ) |
28 |
|
elnnz |
|- ( -u N e. NN <-> ( -u N e. ZZ /\ 0 < -u N ) ) |
29 |
25 27 28
|
sylanbrc |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> -u N e. NN ) |
30 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
31 |
30
|
subgss |
|- ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) ) |
32 |
31
|
3ad2ant1 |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> S C_ ( Base ` G ) ) |
33 |
|
simp3 |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> X e. S ) |
34 |
32 33
|
sseldd |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> X e. ( Base ` G ) ) |
35 |
34
|
adantr |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> X e. ( Base ` G ) ) |
36 |
|
eqid |
|- seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) |
37 |
30 8 1 36
|
mulgnn |
|- ( ( -u N e. NN /\ X e. ( Base ` G ) ) -> ( -u N .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) |
38 |
29 35 37
|
syl2anc |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> ( -u N .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) |
39 |
33
|
adantr |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> X e. S ) |
40 |
1
|
subgmulgcl |
|- ( ( S e. ( SubGrp ` G ) /\ -u N e. ZZ /\ X e. S ) -> ( -u N .x. X ) e. S ) |
41 |
23 25 39 40
|
syl3anc |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> ( -u N .x. X ) e. S ) |
42 |
38 41
|
eqeltrrd |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) e. S ) |
43 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
44 |
|
eqid |
|- ( invg ` H ) = ( invg ` H ) |
45 |
2 43 44
|
subginv |
|- ( ( S e. ( SubGrp ` G ) /\ ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) e. S ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) |
46 |
23 42 45
|
syl2anc |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) |
47 |
22 46
|
syldan |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) |
48 |
11
|
adantr |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ) |
49 |
48
|
fveq1d |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) |
50 |
49
|
fveq2d |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> ( ( invg ` H ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) |
51 |
47 50
|
eqtrd |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) |
52 |
51
|
anassrs |
|- ( ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) /\ -. 0 < N ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) |
53 |
52
|
ifeq2da |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) = if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) |
54 |
14 53
|
eqtrd |
|- ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) = if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) |
55 |
54
|
ifeq2da |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) ) |
56 |
7 55
|
eqtrd |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) ) |
57 |
30 8 4 43 1 36
|
mulgval |
|- ( ( N e. ZZ /\ X e. ( Base ` G ) ) -> ( N .x. X ) = if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) ) |
58 |
15 34 57
|
syl2anc |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) = if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) ) |
59 |
2
|
subgbas |
|- ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) ) |
60 |
59
|
3ad2ant1 |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> S = ( Base ` H ) ) |
61 |
33 60
|
eleqtrd |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> X e. ( Base ` H ) ) |
62 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
63 |
|
eqid |
|- ( +g ` H ) = ( +g ` H ) |
64 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
65 |
|
eqid |
|- seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) |
66 |
62 63 64 44 3 65
|
mulgval |
|- ( ( N e. ZZ /\ X e. ( Base ` H ) ) -> ( N .xb X ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) ) |
67 |
15 61 66
|
syl2anc |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .xb X ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) ) |
68 |
56 58 67
|
3eqtr4d |
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) = ( N .xb X ) ) |