Step |
Hyp |
Ref |
Expression |
1 |
|
subgmulgcl.t |
⊢ · = ( .g ‘ 𝐺 ) |
2 |
|
subgmulg.h |
⊢ 𝐻 = ( 𝐺 ↾s 𝑆 ) |
3 |
|
subgmulg.t |
⊢ ∙ = ( .g ‘ 𝐻 ) |
4 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
5 |
2 4
|
subg0 |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) ) |
6 |
5
|
3ad2ant1 |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) ) |
7 |
6
|
ifeq1d |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → if ( 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) = if ( 𝑁 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) ) |
8 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
9 |
2 8
|
ressplusg |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) ) |
10 |
9
|
3ad2ant1 |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) ) |
11 |
10
|
seqeq2d |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ) |
12 |
11
|
adantr |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ¬ 𝑁 = 0 ) → seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ) |
13 |
12
|
fveq1d |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ¬ 𝑁 = 0 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) ) |
14 |
13
|
ifeq1d |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ¬ 𝑁 = 0 ) → if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) = if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) |
15 |
|
simp2 |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑁 ∈ ℤ ) |
16 |
15
|
zred |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑁 ∈ ℝ ) |
17 |
|
0re |
⊢ 0 ∈ ℝ |
18 |
|
axlttri |
⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑁 < 0 ↔ ¬ ( 𝑁 = 0 ∨ 0 < 𝑁 ) ) ) |
19 |
16 17 18
|
sylancl |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 < 0 ↔ ¬ ( 𝑁 = 0 ∨ 0 < 𝑁 ) ) ) |
20 |
|
ioran |
⊢ ( ¬ ( 𝑁 = 0 ∨ 0 < 𝑁 ) ↔ ( ¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁 ) ) |
21 |
19 20
|
bitrdi |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 < 0 ↔ ( ¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁 ) ) ) |
22 |
21
|
biimpar |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ( ¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁 ) ) → 𝑁 < 0 ) |
23 |
|
simpl1 |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
24 |
15
|
adantr |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → 𝑁 ∈ ℤ ) |
25 |
24
|
znegcld |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → - 𝑁 ∈ ℤ ) |
26 |
16
|
lt0neg1d |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 < 0 ↔ 0 < - 𝑁 ) ) |
27 |
26
|
biimpa |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → 0 < - 𝑁 ) |
28 |
|
elnnz |
⊢ ( - 𝑁 ∈ ℕ ↔ ( - 𝑁 ∈ ℤ ∧ 0 < - 𝑁 ) ) |
29 |
25 27 28
|
sylanbrc |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → - 𝑁 ∈ ℕ ) |
30 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
31 |
30
|
subgss |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
32 |
31
|
3ad2ant1 |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
33 |
|
simp3 |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 ) |
34 |
32 33
|
sseldd |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) ) |
35 |
34
|
adantr |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) ) |
36 |
|
eqid |
⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) |
37 |
30 8 1 36
|
mulgnn |
⊢ ( ( - 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( - 𝑁 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) |
38 |
29 35 37
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → ( - 𝑁 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) |
39 |
33
|
adantr |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → 𝑋 ∈ 𝑆 ) |
40 |
1
|
subgmulgcl |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ - 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( - 𝑁 · 𝑋 ) ∈ 𝑆 ) |
41 |
23 25 39 40
|
syl3anc |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → ( - 𝑁 · 𝑋 ) ∈ 𝑆 ) |
42 |
38 41
|
eqeltrrd |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ∈ 𝑆 ) |
43 |
|
eqid |
⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 ) |
44 |
|
eqid |
⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 ) |
45 |
2 43 44
|
subginv |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) |
46 |
23 42 45
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 < 0 ) → ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) |
47 |
22 46
|
syldan |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ( ¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) |
48 |
11
|
adantr |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ( ¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁 ) ) → seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ) |
49 |
48
|
fveq1d |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ( ¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁 ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) |
50 |
49
|
fveq2d |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ( ¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁 ) ) → ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) |
51 |
47 50
|
eqtrd |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ( ¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) |
52 |
51
|
anassrs |
⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ¬ 𝑁 = 0 ) ∧ ¬ 0 < 𝑁 ) → ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) |
53 |
52
|
ifeq2da |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ¬ 𝑁 = 0 ) → if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) = if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) |
54 |
14 53
|
eqtrd |
⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ¬ 𝑁 = 0 ) → if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) = if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) |
55 |
54
|
ifeq2da |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → if ( 𝑁 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) = if ( 𝑁 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) ) |
56 |
7 55
|
eqtrd |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → if ( 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) = if ( 𝑁 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) ) |
57 |
30 8 4 43 1 36
|
mulgval |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑁 · 𝑋 ) = if ( 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) ) |
58 |
15 34 57
|
syl2anc |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) = if ( 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) ) |
59 |
2
|
subgbas |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) ) |
60 |
59
|
3ad2ant1 |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑆 = ( Base ‘ 𝐻 ) ) |
61 |
33 60
|
eleqtrd |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐻 ) ) |
62 |
|
eqid |
⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 ) |
63 |
|
eqid |
⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 ) |
64 |
|
eqid |
⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 ) |
65 |
|
eqid |
⊢ seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) |
66 |
62 63 64 44 3 65
|
mulgval |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑁 ∙ 𝑋 ) = if ( 𝑁 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) ) |
67 |
15 61 66
|
syl2anc |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 ∙ 𝑋 ) = if ( 𝑁 = 0 , ( 0g ‘ 𝐻 ) , if ( 0 < 𝑁 , ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) , ( ( invg ‘ 𝐻 ) ‘ ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) ) ) ) ) |
68 |
56 58 67
|
3eqtr4d |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) = ( 𝑁 ∙ 𝑋 ) ) |