Step | Hyp | Ref
| Expression |
1 | | vtsval.l |
. . . 4
β’ (π β πΏ:ββΆβ) |
2 | | cnex 11053 |
. . . . 5
β’ β
β V |
3 | | nnex 12080 |
. . . . 5
β’ β
β V |
4 | 2, 3 | elmap 8730 |
. . . 4
β’ (πΏ β (β
βm β) β πΏ:ββΆβ) |
5 | 1, 4 | sylibr 233 |
. . 3
β’ (π β πΏ β (β βm
β)) |
6 | | vtsval.n |
. . 3
β’ (π β π β
β0) |
7 | | fveq1 6824 |
. . . . . . 7
β’ (π = πΏ β (πβπ) = (πΏβπ)) |
8 | 7 | oveq1d 7352 |
. . . . . 6
β’ (π = πΏ β ((πβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) = ((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯))))) |
9 | 8 | sumeq2sdv 15515 |
. . . . 5
β’ (π = πΏ β Ξ£π β (1...π)((πβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) =
Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯))))) |
10 | 9 | mpteq2dv 5194 |
. . . 4
β’ (π = πΏ β (π₯ β β β¦ Ξ£π β (1...π)((πβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯))))) = (π₯ β β β¦
Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))))) |
11 | | oveq2 7345 |
. . . . . 6
β’ (π = π β (1...π) = (1...π)) |
12 | 11 | sumeq1d 15512 |
. . . . 5
β’ (π = π β Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) =
Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯))))) |
13 | 12 | mpteq2dv 5194 |
. . . 4
β’ (π = π β (π₯ β β β¦ Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯))))) = (π₯ β β β¦
Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))))) |
14 | | df-vts 32916 |
. . . 4
β’ vts =
(π β (β
βm β), π β β0 β¦ (π₯ β β β¦
Ξ£π β (1...π)((πβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))))) |
15 | 2 | mptex 7155 |
. . . 4
β’ (π₯ β β β¦
Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯))))) β
V |
16 | 10, 13, 14, 15 | ovmpo 7495 |
. . 3
β’ ((πΏ β (β
βm β) β§ π β β0) β (πΏvtsπ) = (π₯ β β β¦ Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))))) |
17 | 5, 6, 16 | syl2anc 584 |
. 2
β’ (π β (πΏvtsπ) = (π₯ β β β¦ Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))))) |
18 | | oveq2 7345 |
. . . . . . 7
β’ (π₯ = π β (π Β· π₯) = (π Β· π)) |
19 | 18 | oveq2d 7353 |
. . . . . 6
β’ (π₯ = π β ((i Β· (2 Β· Ο))
Β· (π Β· π₯)) = ((i Β· (2 Β·
Ο)) Β· (π Β·
π))) |
20 | 19 | fveq2d 6829 |
. . . . 5
β’ (π₯ = π β (expβ((i Β· (2 Β·
Ο)) Β· (π Β·
π₯))) = (expβ((i
Β· (2 Β· Ο)) Β· (π Β· π)))) |
21 | 20 | oveq2d 7353 |
. . . 4
β’ (π₯ = π β ((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) = ((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π))))) |
22 | 21 | sumeq2sdv 15515 |
. . 3
β’ (π₯ = π β Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) =
Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π))))) |
23 | 22 | adantl 482 |
. 2
β’ ((π β§ π₯ = π) β Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) =
Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π))))) |
24 | | vtsval.x |
. 2
β’ (π β π β β) |
25 | | sumex 15498 |
. . 3
β’
Ξ£π β
(1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π)))) β
V |
26 | 25 | a1i 11 |
. 2
β’ (π β Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π)))) β
V) |
27 | 17, 23, 24, 26 | fvmptd 6938 |
1
β’ (π β ((πΏvtsπ)βπ) = Ξ£π β (1...π)((πΏβπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π))))) |