Step | Hyp | Ref
| Expression |
1 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 ↑ 𝑋) = (0 ↑ 𝑋)) |
2 | 1 | oveq2d 7373 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (0 ↑ 𝑋))) |
3 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥𝐸𝑅) = (0𝐸𝑅)) |
4 | 3 | oveq1d 7372 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥𝐸𝑅) · 𝑋) = ((0𝐸𝑅) · 𝑋)) |
5 | 2, 4 | eqeq12d 2752 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋))) |
6 | 5 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 0 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋)))) |
7 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ↑ 𝑋) = (𝑦 ↑ 𝑋)) |
8 | 7 | oveq2d 7373 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (𝑦 ↑ 𝑋))) |
9 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥𝐸𝑅) = (𝑦𝐸𝑅)) |
10 | 9 | oveq1d 7372 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥𝐸𝑅) · 𝑋) = ((𝑦𝐸𝑅) · 𝑋)) |
11 | 8, 10 | eqeq12d 2752 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋))) |
12 | 11 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)))) |
13 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ↑ 𝑋) = ((𝑦 + 1) ↑ 𝑋)) |
14 | 13 | oveq2d 7373 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · ((𝑦 + 1) ↑ 𝑋))) |
15 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥𝐸𝑅) = ((𝑦 + 1)𝐸𝑅)) |
16 | 15 | oveq1d 7372 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → ((𝑥𝐸𝑅) · 𝑋) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
17 | 14, 16 | eqeq12d 2752 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋))) |
18 | 17 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
19 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥 ↑ 𝑋) = (𝑁 ↑ 𝑋)) |
20 | 19 | oveq2d 7373 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (𝑁 ↑ 𝑋))) |
21 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥𝐸𝑅) = (𝑁𝐸𝑅)) |
22 | 21 | oveq1d 7372 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑥𝐸𝑅) · 𝑋) = ((𝑁𝐸𝑅) · 𝑋)) |
23 | 20, 22 | eqeq12d 2752 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
24 | 23 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)))) |
25 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
26 | 25 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑋 ∈ 𝑉) |
27 | | lmodvsmdi.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑊) |
28 | | eqid 2736 |
. . . . . . . . . 10
⊢
(0g‘𝑊) = (0g‘𝑊) |
29 | | lmodvsmdi.p |
. . . . . . . . . 10
⊢ ↑ =
(.g‘𝑊) |
30 | 27, 28, 29 | mulg0 18879 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑉 → (0 ↑ 𝑋) = (0g‘𝑊)) |
31 | 26, 30 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (0 ↑ 𝑋) = (0g‘𝑊)) |
32 | 31 | oveq2d 7373 |
. . . . . . 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 20356 |
. . . . . . . . 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 2736 |
. . . . . . . . . 10
⊢
(0g‘𝐹) = (0g‘𝐹) |
44 | 27, 36, 37, 43, 28 | lmod0vs 20355 |
. . . . . . . . 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 18879 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝐾 → (0𝐸𝑅) = (0g‘𝐹)) |
49 | 48 | eqcomd 2742 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝐾 → (0g‘𝐹) = (0𝐸𝑅)) |
50 | 46, 49 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
(0g‘𝐹) =
(0𝐸𝑅)) |
51 | 50 | oveq1d 7372 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
((0g‘𝐹)
·
𝑋) = ((0𝐸𝑅) · 𝑋)) |
52 | 40, 45, 51 | 3eqtr2d 2782 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ·
(0g‘𝑊)) =
((0𝐸𝑅) · 𝑋)) |
53 | 32, 52 | eqtrd 2776 |
. . . . . 6
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋)) |
54 | | lmodgrp 20329 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
55 | 54 | grpmndd 18760 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Mnd) |
56 | 55 | ad2antll 727 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ Mnd) |
57 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑦 ∈ ℕ0) |
58 | 26 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑋 ∈ 𝑉) |
59 | | eqid 2736 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑊) = (+g‘𝑊) |
60 | 27, 29, 59 | mulgnn0p1 18887 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝑉) → ((𝑦 + 1) ↑ 𝑋) = ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) |
61 | 56, 57, 58, 60 | syl3anc 1371 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1) ↑ 𝑋) = ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) |
62 | 61 | oveq2d 7373 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋))) |
63 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑊 ∈ LMod) |
64 | 63 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ LMod) |
65 | | simprll 777 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑅 ∈ 𝐾) |
66 | 27, 29, 56, 57, 58 | mulgnn0cld 18897 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦 ↑ 𝑋) ∈ 𝑉) |
67 | 27, 59, 36, 37, 38 | lmodvsdi 20345 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ (𝑦 ↑ 𝑋) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
68 | 64, 65, 66, 58, 67 | syl13anc 1372 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
69 | 62, 68 | eqtrd 2776 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
70 | | oveq1 7364 |
. . . . . . . . . 10
⊢ ((𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋) → ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
71 | 69, 70 | sylan9eq 2796 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
72 | 36 | lmodfgrp 20331 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
73 | 72 | grpmndd 18760 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Mnd) |
74 | 73 | ad2antll 727 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝐹 ∈ Mnd) |
75 | 38, 47, 74, 57, 65 | mulgnn0cld 18897 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦𝐸𝑅) ∈ 𝐾) |
76 | | eqid 2736 |
. . . . . . . . . . . . 13
⊢
(+g‘𝐹) = (+g‘𝐹) |
77 | 27, 59, 36, 37, 38, 76 | lmodvsdir 20346 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ ((𝑦𝐸𝑅) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
78 | 64, 75, 65, 58, 77 | syl13anc 1372 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
79 | 38, 47, 76 | mulgnn0p1 18887 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑅 ∈ 𝐾) → ((𝑦 + 1)𝐸𝑅) = ((𝑦𝐸𝑅)(+g‘𝐹)𝑅)) |
80 | 74, 57, 65, 79 | syl3anc 1371 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1)𝐸𝑅) = ((𝑦𝐸𝑅)(+g‘𝐹)𝑅)) |
81 | 80 | eqcomd 2742 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦𝐸𝑅)(+g‘𝐹)𝑅) = ((𝑦 + 1)𝐸𝑅)) |
82 | 81 | oveq1d 7372 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
83 | 78, 82 | eqtr3d 2778 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
84 | 83 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
85 | 71, 84 | eqtrd 2776 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
86 | 85 | exp31 420 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
87 | 86 | a2d 29 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
88 | 6, 12, 18, 24, 53, 87 | nn0ind 12598 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
89 | 88 | exp4c 433 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑅 ∈ 𝐾 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))))) |
90 | 89 | com12 32 |
. . 3
⊢ (𝑅 ∈ 𝐾 → (𝑁 ∈ ℕ0 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))))) |
91 | 90 | 3imp 1111 |
. 2
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
92 | 91 | impcom 408 |
1
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)) |