Step |
Hyp |
Ref |
Expression |
1 |
|
lmodvsmmulgdi.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lmodvsmmulgdi.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
3 |
|
lmodvsmmulgdi.s |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
4 |
|
lmodvsmmulgdi.k |
⊢ 𝐾 = ( Base ‘ 𝐹 ) |
5 |
|
lmodvsmmulgdi.p |
⊢ ↑ = ( .g ‘ 𝑊 ) |
6 |
|
lmodvsmmulgdi.e |
⊢ 𝐸 = ( .g ‘ 𝐹 ) |
7 |
|
oveq1 |
⊢ ( 𝑥 = 0 → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( 0 ↑ ( 𝐶 · 𝑋 ) ) ) |
8 |
|
oveq1 |
⊢ ( 𝑥 = 0 → ( 𝑥 𝐸 𝐶 ) = ( 0 𝐸 𝐶 ) ) |
9 |
8
|
oveq1d |
⊢ ( 𝑥 = 0 → ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) = ( ( 0 𝐸 𝐶 ) · 𝑋 ) ) |
10 |
7 9
|
eqeq12d |
⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ↔ ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 0 𝐸 𝐶 ) · 𝑋 ) ) ) |
11 |
10
|
imbi2d |
⊢ ( 𝑥 = 0 → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ) ↔ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 0 𝐸 𝐶 ) · 𝑋 ) ) ) ) |
12 |
|
oveq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ) |
13 |
|
oveq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐸 𝐶 ) = ( 𝑦 𝐸 𝐶 ) ) |
14 |
13
|
oveq1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) |
15 |
12 14
|
eqeq12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ↔ ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) ) |
16 |
15
|
imbi2d |
⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ) ↔ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) ) ) |
17 |
|
oveq1 |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) ) |
18 |
|
oveq1 |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 𝐸 𝐶 ) = ( ( 𝑦 + 1 ) 𝐸 𝐶 ) ) |
19 |
18
|
oveq1d |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) |
20 |
17 19
|
eqeq12d |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ↔ ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) ) |
21 |
20
|
imbi2d |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ) ↔ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) ) ) |
22 |
|
oveq1 |
⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) ) |
23 |
|
oveq1 |
⊢ ( 𝑥 = 𝑁 → ( 𝑥 𝐸 𝐶 ) = ( 𝑁 𝐸 𝐶 ) ) |
24 |
23
|
oveq1d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) |
25 |
22 24
|
eqeq12d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ↔ ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) ) |
26 |
25
|
imbi2d |
⊢ ( 𝑥 = 𝑁 → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ) ↔ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) ) ) |
27 |
|
simpr |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝑊 ∈ LMod ) |
28 |
|
simpr |
⊢ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 ) |
29 |
28
|
adantr |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝑋 ∈ 𝑉 ) |
30 |
|
eqid |
⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 ) |
31 |
|
eqid |
⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 ) |
32 |
1 2 3 30 31
|
lmod0vs |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) ) |
33 |
27 29 32
|
syl2anc |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) ) |
34 |
|
simpl |
⊢ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝐶 ∈ 𝐾 ) |
35 |
34
|
adantr |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝐶 ∈ 𝐾 ) |
36 |
4 30 6
|
mulg0 |
⊢ ( 𝐶 ∈ 𝐾 → ( 0 𝐸 𝐶 ) = ( 0g ‘ 𝐹 ) ) |
37 |
35 36
|
syl |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 𝐸 𝐶 ) = ( 0g ‘ 𝐹 ) ) |
38 |
37
|
oveq1d |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 0 𝐸 𝐶 ) · 𝑋 ) = ( ( 0g ‘ 𝐹 ) · 𝑋 ) ) |
39 |
1 2 3 4
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐶 · 𝑋 ) ∈ 𝑉 ) |
40 |
27 35 29 39
|
syl3anc |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝐶 · 𝑋 ) ∈ 𝑉 ) |
41 |
1 31 5
|
mulg0 |
⊢ ( ( 𝐶 · 𝑋 ) ∈ 𝑉 → ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( 0g ‘ 𝑊 ) ) |
42 |
40 41
|
syl |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( 0g ‘ 𝑊 ) ) |
43 |
33 38 42
|
3eqtr4rd |
⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 0 𝐸 𝐶 ) · 𝑋 ) ) |
44 |
|
lmodgrp |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp ) |
45 |
44
|
grpmndd |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Mnd ) |
46 |
45
|
ad2antll |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑊 ∈ Mnd ) |
47 |
|
simpl |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑦 ∈ ℕ0 ) |
48 |
40
|
adantl |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝐶 · 𝑋 ) ∈ 𝑉 ) |
49 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
50 |
1 5 49
|
mulgnn0p1 |
⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ ( 𝐶 · 𝑋 ) ∈ 𝑉 ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) ) |
51 |
46 47 48 50
|
syl3anc |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) ) |
52 |
51
|
adantr |
⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) ) |
53 |
|
oveq1 |
⊢ ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) → ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) ) |
54 |
27
|
adantl |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑊 ∈ LMod ) |
55 |
2
|
lmodring |
⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring ) |
56 |
|
ringmnd |
⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Mnd ) |
57 |
55 56
|
syl |
⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Mnd ) |
58 |
57
|
ad2antll |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝐹 ∈ Mnd ) |
59 |
|
simprll |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝐶 ∈ 𝐾 ) |
60 |
4 6
|
mulgnn0cl |
⊢ ( ( 𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ 𝐾 ) → ( 𝑦 𝐸 𝐶 ) ∈ 𝐾 ) |
61 |
58 47 59 60
|
syl3anc |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝑦 𝐸 𝐶 ) ∈ 𝐾 ) |
62 |
29
|
adantl |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑋 ∈ 𝑉 ) |
63 |
|
eqid |
⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 ) |
64 |
1 49 2 3 4 63
|
lmodvsdir |
⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 𝐸 𝐶 ) ∈ 𝐾 ∧ 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) · 𝑋 ) = ( ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) ) |
65 |
54 61 59 62 64
|
syl13anc |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) · 𝑋 ) = ( ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) ) |
66 |
4 6 63
|
mulgnn0p1 |
⊢ ( ( 𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ 𝐾 ) → ( ( 𝑦 + 1 ) 𝐸 𝐶 ) = ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) ) |
67 |
58 47 59 66
|
syl3anc |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 + 1 ) 𝐸 𝐶 ) = ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) ) |
68 |
67
|
eqcomd |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) = ( ( 𝑦 + 1 ) 𝐸 𝐶 ) ) |
69 |
68
|
oveq1d |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) · 𝑋 ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) |
70 |
65 69
|
eqtr3d |
⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) |
71 |
53 70
|
sylan9eqr |
⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) → ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) |
72 |
52 71
|
eqtrd |
⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) |
73 |
72
|
exp31 |
⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) ) ) |
74 |
73
|
a2d |
⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) → ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) ) ) |
75 |
11 16 21 26 43 74
|
nn0ind |
⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) ) |
76 |
75
|
exp4c |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝐶 ∈ 𝐾 → ( 𝑋 ∈ 𝑉 → ( 𝑊 ∈ LMod → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) ) ) ) |
77 |
76
|
3imp21 |
⊢ ( ( 𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ∈ LMod → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) ) |
78 |
77
|
impcom |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) |