Step | Hyp | Ref
| Expression |
1 | | oveq1 6929 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 ↑ 𝑋) = (0 ↑ 𝑋)) |
2 | 1 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (0 ↑ 𝑋))) |
3 | | oveq1 6929 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥𝐸𝑅) = (0𝐸𝑅)) |
4 | 3 | oveq1d 6937 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥𝐸𝑅) · 𝑋) = ((0𝐸𝑅) · 𝑋)) |
5 | 2, 4 | eqeq12d 2793 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋))) |
6 | 5 | imbi2d 332 |
. . . . . 6
⊢ (𝑥 = 0 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋)))) |
7 | | oveq1 6929 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ↑ 𝑋) = (𝑦 ↑ 𝑋)) |
8 | 7 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (𝑦 ↑ 𝑋))) |
9 | | oveq1 6929 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥𝐸𝑅) = (𝑦𝐸𝑅)) |
10 | 9 | oveq1d 6937 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥𝐸𝑅) · 𝑋) = ((𝑦𝐸𝑅) · 𝑋)) |
11 | 8, 10 | eqeq12d 2793 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋))) |
12 | 11 | imbi2d 332 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)))) |
13 | | oveq1 6929 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ↑ 𝑋) = ((𝑦 + 1) ↑ 𝑋)) |
14 | 13 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · ((𝑦 + 1) ↑ 𝑋))) |
15 | | oveq1 6929 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥𝐸𝑅) = ((𝑦 + 1)𝐸𝑅)) |
16 | 15 | oveq1d 6937 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → ((𝑥𝐸𝑅) · 𝑋) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
17 | 14, 16 | eqeq12d 2793 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋))) |
18 | 17 | imbi2d 332 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
19 | | oveq1 6929 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥 ↑ 𝑋) = (𝑁 ↑ 𝑋)) |
20 | 19 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (𝑁 ↑ 𝑋))) |
21 | | oveq1 6929 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥𝐸𝑅) = (𝑁𝐸𝑅)) |
22 | 21 | oveq1d 6937 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑥𝐸𝑅) · 𝑋) = ((𝑁𝐸𝑅) · 𝑋)) |
23 | 20, 22 | eqeq12d 2793 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
24 | 23 | imbi2d 332 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)))) |
25 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
26 | 25 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑋 ∈ 𝑉) |
27 | | lmodvsmdi.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑊) |
28 | | eqid 2778 |
. . . . . . . . . 10
⊢
(0g‘𝑊) = (0g‘𝑊) |
29 | | lmodvsmdi.p |
. . . . . . . . . 10
⊢ ↑ =
(.g‘𝑊) |
30 | 27, 28, 29 | mulg0 17933 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑉 → (0 ↑ 𝑋) = (0g‘𝑊)) |
31 | 26, 30 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (0 ↑ 𝑋) = (0g‘𝑊)) |
32 | 31 | oveq2d 6938 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = (𝑅 ·
(0g‘𝑊))) |
33 | | simpl 476 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑅 ∈ 𝐾) |
34 | 33 | anim1i 608 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ∈ 𝐾 ∧ 𝑊 ∈ LMod)) |
35 | 34 | ancomd 455 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾)) |
36 | | lmodvsmdi.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
37 | | lmodvsmdi.s |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑊) |
38 | | lmodvsmdi.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝐹) |
39 | 36, 37, 38, 28 | lmodvs0 19289 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → (𝑅 ·
(0g‘𝑊)) =
(0g‘𝑊)) |
40 | 35, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ·
(0g‘𝑊)) =
(0g‘𝑊)) |
41 | 25 | anim1i 608 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑋 ∈ 𝑉 ∧ 𝑊 ∈ LMod)) |
42 | 41 | ancomd 455 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉)) |
43 | | eqid 2778 |
. . . . . . . . . 10
⊢
(0g‘𝐹) = (0g‘𝐹) |
44 | 27, 36, 37, 43, 28 | lmod0vs 19288 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((0g‘𝐹) · 𝑋) = (0g‘𝑊)) |
45 | 42, 44 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
((0g‘𝐹)
·
𝑋) =
(0g‘𝑊)) |
46 | 33 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑅 ∈ 𝐾) |
47 | | lmodvsmdi.e |
. . . . . . . . . . . 12
⊢ 𝐸 = (.g‘𝐹) |
48 | 38, 43, 47 | mulg0 17933 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝐾 → (0𝐸𝑅) = (0g‘𝐹)) |
49 | 48 | eqcomd 2784 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝐾 → (0g‘𝐹) = (0𝐸𝑅)) |
50 | 46, 49 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
(0g‘𝐹) =
(0𝐸𝑅)) |
51 | 50 | oveq1d 6937 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
((0g‘𝐹)
·
𝑋) = ((0𝐸𝑅) · 𝑋)) |
52 | 40, 45, 51 | 3eqtr2d 2820 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ·
(0g‘𝑊)) =
((0𝐸𝑅) · 𝑋)) |
53 | 32, 52 | eqtrd 2814 |
. . . . . 6
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋)) |
54 | | lmodgrp 19262 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
55 | | grpmnd 17816 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Grp → 𝑊 ∈ Mnd) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Mnd) |
57 | 56 | ad2antll 719 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ Mnd) |
58 | | simpl 476 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑦 ∈ ℕ0) |
59 | 26 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑋 ∈ 𝑉) |
60 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑊) = (+g‘𝑊) |
61 | 27, 29, 60 | mulgnn0p1 17939 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝑉) → ((𝑦 + 1) ↑ 𝑋) = ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) |
62 | 57, 58, 59, 61 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1) ↑ 𝑋) = ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) |
63 | 62 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋))) |
64 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑊 ∈ LMod) |
65 | 64 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ LMod) |
66 | | simprll 769 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑅 ∈ 𝐾) |
67 | 27, 29 | mulgnn0cl 17944 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝑉) → (𝑦 ↑ 𝑋) ∈ 𝑉) |
68 | 57, 58, 59, 67 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦 ↑ 𝑋) ∈ 𝑉) |
69 | 27, 60, 36, 37, 38 | lmodvsdi 19278 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ (𝑦 ↑ 𝑋) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
70 | 65, 66, 68, 59, 69 | syl13anc 1440 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
71 | 63, 70 | eqtrd 2814 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
72 | | oveq1 6929 |
. . . . . . . . . 10
⊢ ((𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋) → ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
73 | 71, 72 | sylan9eq 2834 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
74 | 36 | lmodfgrp 19264 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
75 | | grpmnd 17816 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Grp → 𝐹 ∈ Mnd) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Mnd) |
77 | 76 | ad2antll 719 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝐹 ∈ Mnd) |
78 | 38, 47 | mulgnn0cl 17944 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑅 ∈ 𝐾) → (𝑦𝐸𝑅) ∈ 𝐾) |
79 | 77, 58, 66, 78 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦𝐸𝑅) ∈ 𝐾) |
80 | | eqid 2778 |
. . . . . . . . . . . . 13
⊢
(+g‘𝐹) = (+g‘𝐹) |
81 | 27, 60, 36, 37, 38, 80 | lmodvsdir 19279 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ ((𝑦𝐸𝑅) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
82 | 65, 79, 66, 59, 81 | syl13anc 1440 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
83 | 38, 47, 80 | mulgnn0p1 17939 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑅 ∈ 𝐾) → ((𝑦 + 1)𝐸𝑅) = ((𝑦𝐸𝑅)(+g‘𝐹)𝑅)) |
84 | 77, 58, 66, 83 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1)𝐸𝑅) = ((𝑦𝐸𝑅)(+g‘𝐹)𝑅)) |
85 | 84 | eqcomd 2784 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦𝐸𝑅)(+g‘𝐹)𝑅) = ((𝑦 + 1)𝐸𝑅)) |
86 | 85 | oveq1d 6937 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
87 | 82, 86 | eqtr3d 2816 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
88 | 87 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
89 | 73, 88 | eqtrd 2814 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
90 | 89 | exp31 412 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
91 | 90 | a2d 29 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
92 | 6, 12, 18, 24, 53, 91 | nn0ind 11824 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
93 | 92 | exp4c 425 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑅 ∈ 𝐾 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))))) |
94 | 93 | com12 32 |
. . 3
⊢ (𝑅 ∈ 𝐾 → (𝑁 ∈ ℕ0 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))))) |
95 | 94 | 3imp 1098 |
. 2
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
96 | 95 | impcom 398 |
1
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)) |