Step | Hyp | Ref
| Expression |
1 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 ↑ 𝑋) = (0 ↑ 𝑋)) |
2 | 1 | oveq2d 7293 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (0 ↑ 𝑋))) |
3 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥𝐸𝑅) = (0𝐸𝑅)) |
4 | 3 | oveq1d 7292 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥𝐸𝑅) · 𝑋) = ((0𝐸𝑅) · 𝑋)) |
5 | 2, 4 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋))) |
6 | 5 | imbi2d 341 |
. . . . . 6
⊢ (𝑥 = 0 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋)))) |
7 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ↑ 𝑋) = (𝑦 ↑ 𝑋)) |
8 | 7 | oveq2d 7293 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (𝑦 ↑ 𝑋))) |
9 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥𝐸𝑅) = (𝑦𝐸𝑅)) |
10 | 9 | oveq1d 7292 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥𝐸𝑅) · 𝑋) = ((𝑦𝐸𝑅) · 𝑋)) |
11 | 8, 10 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋))) |
12 | 11 | imbi2d 341 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)))) |
13 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ↑ 𝑋) = ((𝑦 + 1) ↑ 𝑋)) |
14 | 13 | oveq2d 7293 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · ((𝑦 + 1) ↑ 𝑋))) |
15 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥𝐸𝑅) = ((𝑦 + 1)𝐸𝑅)) |
16 | 15 | oveq1d 7292 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → ((𝑥𝐸𝑅) · 𝑋) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
17 | 14, 16 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋))) |
18 | 17 | imbi2d 341 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
19 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥 ↑ 𝑋) = (𝑁 ↑ 𝑋)) |
20 | 19 | oveq2d 7293 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (𝑁 ↑ 𝑋))) |
21 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥𝐸𝑅) = (𝑁𝐸𝑅)) |
22 | 21 | oveq1d 7292 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑥𝐸𝑅) · 𝑋) = ((𝑁𝐸𝑅) · 𝑋)) |
23 | 20, 22 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
24 | 23 | imbi2d 341 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)))) |
25 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
26 | 25 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑋 ∈ 𝑉) |
27 | | lmodvsmdi.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑊) |
28 | | eqid 2738 |
. . . . . . . . . 10
⊢
(0g‘𝑊) = (0g‘𝑊) |
29 | | lmodvsmdi.p |
. . . . . . . . . 10
⊢ ↑ =
(.g‘𝑊) |
30 | 27, 28, 29 | mulg0 18705 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑉 → (0 ↑ 𝑋) = (0g‘𝑊)) |
31 | 26, 30 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (0 ↑ 𝑋) = (0g‘𝑊)) |
32 | 31 | oveq2d 7293 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = (𝑅 ·
(0g‘𝑊))) |
33 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑅 ∈ 𝐾) |
34 | 33 | anim1i 615 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ∈ 𝐾 ∧ 𝑊 ∈ LMod)) |
35 | 34 | ancomd 462 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾)) |
36 | | lmodvsmdi.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
37 | | lmodvsmdi.s |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑊) |
38 | | lmodvsmdi.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝐹) |
39 | 36, 37, 38, 28 | lmodvs0 20155 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → (𝑅 ·
(0g‘𝑊)) =
(0g‘𝑊)) |
40 | 35, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ·
(0g‘𝑊)) =
(0g‘𝑊)) |
41 | 25 | anim1i 615 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑋 ∈ 𝑉 ∧ 𝑊 ∈ LMod)) |
42 | 41 | ancomd 462 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉)) |
43 | | eqid 2738 |
. . . . . . . . . 10
⊢
(0g‘𝐹) = (0g‘𝐹) |
44 | 27, 36, 37, 43, 28 | lmod0vs 20154 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((0g‘𝐹) · 𝑋) = (0g‘𝑊)) |
45 | 42, 44 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
((0g‘𝐹)
·
𝑋) =
(0g‘𝑊)) |
46 | 33 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑅 ∈ 𝐾) |
47 | | lmodvsmdi.e |
. . . . . . . . . . . 12
⊢ 𝐸 = (.g‘𝐹) |
48 | 38, 43, 47 | mulg0 18705 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝐾 → (0𝐸𝑅) = (0g‘𝐹)) |
49 | 48 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝐾 → (0g‘𝐹) = (0𝐸𝑅)) |
50 | 46, 49 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
(0g‘𝐹) =
(0𝐸𝑅)) |
51 | 50 | oveq1d 7292 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
((0g‘𝐹)
·
𝑋) = ((0𝐸𝑅) · 𝑋)) |
52 | 40, 45, 51 | 3eqtr2d 2784 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ·
(0g‘𝑊)) =
((0𝐸𝑅) · 𝑋)) |
53 | 32, 52 | eqtrd 2778 |
. . . . . 6
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋)) |
54 | | lmodgrp 20128 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
55 | 54 | grpmndd 18587 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Mnd) |
56 | 55 | ad2antll 726 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ Mnd) |
57 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑦 ∈ ℕ0) |
58 | 26 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑋 ∈ 𝑉) |
59 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑊) = (+g‘𝑊) |
60 | 27, 29, 59 | mulgnn0p1 18713 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝑉) → ((𝑦 + 1) ↑ 𝑋) = ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) |
61 | 56, 57, 58, 60 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1) ↑ 𝑋) = ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) |
62 | 61 | oveq2d 7293 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋))) |
63 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑊 ∈ LMod) |
64 | 63 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ LMod) |
65 | | simprll 776 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑅 ∈ 𝐾) |
66 | 27, 29 | mulgnn0cl 18718 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝑉) → (𝑦 ↑ 𝑋) ∈ 𝑉) |
67 | 56, 57, 58, 66 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦 ↑ 𝑋) ∈ 𝑉) |
68 | 27, 59, 36, 37, 38 | lmodvsdi 20144 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ (𝑦 ↑ 𝑋) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
69 | 64, 65, 67, 58, 68 | syl13anc 1371 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
70 | 62, 69 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
71 | | oveq1 7284 |
. . . . . . . . . 10
⊢ ((𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋) → ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
72 | 70, 71 | sylan9eq 2798 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
73 | 36 | lmodfgrp 20130 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
74 | 73 | grpmndd 18587 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Mnd) |
75 | 74 | ad2antll 726 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝐹 ∈ Mnd) |
76 | 38, 47 | mulgnn0cl 18718 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑅 ∈ 𝐾) → (𝑦𝐸𝑅) ∈ 𝐾) |
77 | 75, 57, 65, 76 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦𝐸𝑅) ∈ 𝐾) |
78 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(+g‘𝐹) = (+g‘𝐹) |
79 | 27, 59, 36, 37, 38, 78 | lmodvsdir 20145 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ ((𝑦𝐸𝑅) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
80 | 64, 77, 65, 58, 79 | syl13anc 1371 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
81 | 38, 47, 78 | mulgnn0p1 18713 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑅 ∈ 𝐾) → ((𝑦 + 1)𝐸𝑅) = ((𝑦𝐸𝑅)(+g‘𝐹)𝑅)) |
82 | 75, 57, 65, 81 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1)𝐸𝑅) = ((𝑦𝐸𝑅)(+g‘𝐹)𝑅)) |
83 | 82 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦𝐸𝑅)(+g‘𝐹)𝑅) = ((𝑦 + 1)𝐸𝑅)) |
84 | 83 | oveq1d 7292 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
85 | 80, 84 | eqtr3d 2780 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
86 | 85 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
87 | 72, 86 | eqtrd 2778 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
88 | 87 | exp31 420 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
89 | 88 | a2d 29 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
90 | 6, 12, 18, 24, 53, 89 | nn0ind 12413 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
91 | 90 | exp4c 433 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑅 ∈ 𝐾 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))))) |
92 | 91 | com12 32 |
. . 3
⊢ (𝑅 ∈ 𝐾 → (𝑁 ∈ ℕ0 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))))) |
93 | 92 | 3imp 1110 |
. 2
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
94 | 93 | impcom 408 |
1
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)) |