| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 ↑ 𝑋) = (0 ↑ 𝑋)) |
| 2 | 1 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (0 ↑ 𝑋))) |
| 3 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥𝐸𝑅) = (0𝐸𝑅)) |
| 4 | 3 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥𝐸𝑅) · 𝑋) = ((0𝐸𝑅) · 𝑋)) |
| 5 | 2, 4 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋))) |
| 6 | 5 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 0 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋)))) |
| 7 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ↑ 𝑋) = (𝑦 ↑ 𝑋)) |
| 8 | 7 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (𝑦 ↑ 𝑋))) |
| 9 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥𝐸𝑅) = (𝑦𝐸𝑅)) |
| 10 | 9 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥𝐸𝑅) · 𝑋) = ((𝑦𝐸𝑅) · 𝑋)) |
| 11 | 8, 10 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋))) |
| 12 | 11 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)))) |
| 13 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ↑ 𝑋) = ((𝑦 + 1) ↑ 𝑋)) |
| 14 | 13 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · ((𝑦 + 1) ↑ 𝑋))) |
| 15 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥𝐸𝑅) = ((𝑦 + 1)𝐸𝑅)) |
| 16 | 15 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → ((𝑥𝐸𝑅) · 𝑋) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
| 17 | 14, 16 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋))) |
| 18 | 17 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
| 19 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥 ↑ 𝑋) = (𝑁 ↑ 𝑋)) |
| 20 | 19 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑅 · (𝑥 ↑ 𝑋)) = (𝑅 · (𝑁 ↑ 𝑋))) |
| 21 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥𝐸𝑅) = (𝑁𝐸𝑅)) |
| 22 | 21 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑥𝐸𝑅) · 𝑋) = ((𝑁𝐸𝑅) · 𝑋)) |
| 23 | 20, 22 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋) ↔ (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
| 24 | 23 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑥 ↑ 𝑋)) = ((𝑥𝐸𝑅) · 𝑋)) ↔ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)))) |
| 25 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
| 26 | 25 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑋 ∈ 𝑉) |
| 27 | | lmodvsmdi.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑊) |
| 28 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 29 | | lmodvsmdi.p |
. . . . . . . . . 10
⊢ ↑ =
(.g‘𝑊) |
| 30 | 27, 28, 29 | mulg0 19092 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑉 → (0 ↑ 𝑋) = (0g‘𝑊)) |
| 31 | 26, 30 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (0 ↑ 𝑋) = (0g‘𝑊)) |
| 32 | 31 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = (𝑅 ·
(0g‘𝑊))) |
| 33 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑅 ∈ 𝐾) |
| 34 | 33 | anim1i 615 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ∈ 𝐾 ∧ 𝑊 ∈ LMod)) |
| 35 | 34 | ancomd 461 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾)) |
| 36 | | lmodvsmdi.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
| 37 | | lmodvsmdi.s |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑊) |
| 38 | | lmodvsmdi.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝐹) |
| 39 | 36, 37, 38, 28 | lmodvs0 20894 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → (𝑅 ·
(0g‘𝑊)) =
(0g‘𝑊)) |
| 40 | 35, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ·
(0g‘𝑊)) =
(0g‘𝑊)) |
| 41 | 25 | anim1i 615 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑋 ∈ 𝑉 ∧ 𝑊 ∈ LMod)) |
| 42 | 41 | ancomd 461 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉)) |
| 43 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝐹) = (0g‘𝐹) |
| 44 | 27, 36, 37, 43, 28 | lmod0vs 20893 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((0g‘𝐹) · 𝑋) = (0g‘𝑊)) |
| 45 | 42, 44 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
((0g‘𝐹)
·
𝑋) =
(0g‘𝑊)) |
| 46 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑅 ∈ 𝐾) |
| 47 | | lmodvsmdi.e |
. . . . . . . . . . . 12
⊢ 𝐸 = (.g‘𝐹) |
| 48 | 38, 43, 47 | mulg0 19092 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝐾 → (0𝐸𝑅) = (0g‘𝐹)) |
| 49 | 48 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝐾 → (0g‘𝐹) = (0𝐸𝑅)) |
| 50 | 46, 49 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
(0g‘𝐹) =
(0𝐸𝑅)) |
| 51 | 50 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) →
((0g‘𝐹)
·
𝑋) = ((0𝐸𝑅) · 𝑋)) |
| 52 | 40, 45, 51 | 3eqtr2d 2783 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 ·
(0g‘𝑊)) =
((0𝐸𝑅) · 𝑋)) |
| 53 | 32, 52 | eqtrd 2777 |
. . . . . 6
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (0 ↑ 𝑋)) = ((0𝐸𝑅) · 𝑋)) |
| 54 | | lmodgrp 20865 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
| 55 | 54 | grpmndd 18964 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Mnd) |
| 56 | 55 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ Mnd) |
| 57 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑦 ∈ ℕ0) |
| 58 | 26 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑋 ∈ 𝑉) |
| 59 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 60 | 27, 29, 59 | mulgnn0p1 19103 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝑉) → ((𝑦 + 1) ↑ 𝑋) = ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) |
| 61 | 56, 57, 58, 60 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1) ↑ 𝑋) = ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) |
| 62 | 61 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋))) |
| 63 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑊 ∈ LMod) |
| 64 | 63 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ LMod) |
| 65 | | simprll 779 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑅 ∈ 𝐾) |
| 66 | 27, 29, 56, 57, 58 | mulgnn0cld 19113 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦 ↑ 𝑋) ∈ 𝑉) |
| 67 | 27, 59, 36, 37, 38 | lmodvsdi 20883 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ (𝑦 ↑ 𝑋) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
| 68 | 64, 65, 66, 58, 67 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 ↑ 𝑋)(+g‘𝑊)𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
| 69 | 62, 68 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋))) |
| 70 | | oveq1 7438 |
. . . . . . . . . 10
⊢ ((𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋) → ((𝑅 · (𝑦 ↑ 𝑋))(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
| 71 | 69, 70 | sylan9eq 2797 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
| 72 | 36 | lmodfgrp 20867 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
| 73 | 72 | grpmndd 18964 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Mnd) |
| 74 | 73 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝐹 ∈ Mnd) |
| 75 | 38, 47, 74, 57, 65 | mulgnn0cld 19113 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦𝐸𝑅) ∈ 𝐾) |
| 76 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝐹) = (+g‘𝐹) |
| 77 | 27, 59, 36, 37, 38, 76 | lmodvsdir 20884 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ ((𝑦𝐸𝑅) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
| 78 | 64, 75, 65, 58, 77 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) |
| 79 | 38, 47, 76 | mulgnn0p1 19103 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑅 ∈ 𝐾) → ((𝑦 + 1)𝐸𝑅) = ((𝑦𝐸𝑅)(+g‘𝐹)𝑅)) |
| 80 | 74, 57, 65, 79 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1)𝐸𝑅) = ((𝑦𝐸𝑅)(+g‘𝐹)𝑅)) |
| 81 | 80 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦𝐸𝑅)(+g‘𝐹)𝑅) = ((𝑦 + 1)𝐸𝑅)) |
| 82 | 81 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅)(+g‘𝐹)𝑅) · 𝑋) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
| 83 | 78, 82 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
| 84 | 83 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (((𝑦𝐸𝑅) · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
| 85 | 71, 84 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)) |
| 86 | 85 | exp31 419 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
| 87 | 86 | a2d 29 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑦 ↑ 𝑋)) = ((𝑦𝐸𝑅) · 𝑋)) → (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · ((𝑦 + 1) ↑ 𝑋)) = (((𝑦 + 1)𝐸𝑅) · 𝑋)))) |
| 88 | 6, 12, 18, 24, 53, 87 | nn0ind 12713 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
| 89 | 88 | exp4c 432 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑅 ∈ 𝐾 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))))) |
| 90 | 89 | com12 32 |
. . 3
⊢ (𝑅 ∈ 𝐾 → (𝑁 ∈ ℕ0 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))))) |
| 91 | 90 | 3imp 1111 |
. 2
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝑊 ∈ LMod → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))) |
| 92 | 91 | impcom 407 |
1
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)) |