Step | Hyp | Ref
| Expression |
1 | | dvnprod.s |
. . 3
β’ (π β π β {β, β}) |
2 | | dvnprod.x |
. . 3
β’ (π β π β
((TopOpenββfld) βΎt π)) |
3 | | dvnprod.t |
. . 3
β’ (π β π β Fin) |
4 | | dvnprod.h |
. . 3
β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) |
5 | | dvnprod.n |
. . 3
β’ (π β π β
β0) |
6 | | dvnprod.dvnh |
. . 3
β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) |
7 | | dvnprod.f |
. . 3
β’ πΉ = (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)) |
8 | | fveq2 6842 |
. . . . . . . . . . 11
β’ (π’ = π‘ β (πβπ’) = (πβπ‘)) |
9 | 8 | cbvsumv 15581 |
. . . . . . . . . 10
β’
Ξ£π’ β
π (πβπ’) = Ξ£π‘ β π (πβπ‘) |
10 | 9 | eqeq1i 2741 |
. . . . . . . . 9
β’
(Ξ£π’ β
π (πβπ’) = π β Ξ£π‘ β π (πβπ‘) = π) |
11 | 10 | rabbii 3413 |
. . . . . . . 8
β’ {π β ((0...π) βm π) β£ Ξ£π’ β π (πβπ’) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} |
12 | | fveq1 6841 |
. . . . . . . . . . 11
β’ (π = π β (πβπ‘) = (πβπ‘)) |
13 | 12 | sumeq2sdv 15589 |
. . . . . . . . . 10
β’ (π = π β Ξ£π‘ β π (πβπ‘) = Ξ£π‘ β π (πβπ‘)) |
14 | 13 | eqeq1d 2738 |
. . . . . . . . 9
β’ (π = π β (Ξ£π‘ β π (πβπ‘) = π β Ξ£π‘ β π (πβπ‘) = π)) |
15 | 14 | cbvrabv 3417 |
. . . . . . . 8
β’ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} |
16 | 11, 15 | eqtri 2764 |
. . . . . . 7
β’ {π β ((0...π) βm π) β£ Ξ£π’ β π (πβπ’) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} |
17 | 16 | mpteq2i 5210 |
. . . . . 6
β’ (π β β0
β¦ {π β
((0...π) βm
π) β£ Ξ£π’ β π (πβπ’) = π}) = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
18 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π = π β (Ξ£π‘ β π (πβπ‘) = π β Ξ£π‘ β π (πβπ‘) = π)) |
19 | 18 | rabbidv 3415 |
. . . . . . . 8
β’ (π = π β {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
20 | | oveq2 7365 |
. . . . . . . . . 10
β’ (π = π β (0...π) = (0...π)) |
21 | 20 | oveq1d 7372 |
. . . . . . . . 9
β’ (π = π β ((0...π) βm π) = ((0...π) βm π)) |
22 | | rabeq 3421 |
. . . . . . . . 9
β’
(((0...π)
βm π) =
((0...π) βm
π) β {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
β’ (π = π β {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
24 | 19, 23 | eqtrd 2776 |
. . . . . . 7
β’ (π = π β {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
25 | 24 | cbvmptv 5218 |
. . . . . 6
β’ (π β β0
β¦ {π β
((0...π) βm
π) β£ Ξ£π‘ β π (πβπ‘) = π}) = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
26 | 17, 25 | eqtri 2764 |
. . . . 5
β’ (π β β0
β¦ {π β
((0...π) βm
π) β£ Ξ£π’ β π (πβπ’) = π}) = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
27 | 26 | mpteq2i 5210 |
. . . 4
β’ (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π’ β π (πβπ’) = π})) = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π})) |
28 | | sumeq1 15573 |
. . . . . . . . 9
β’ (π = π β Ξ£π‘ β π (πβπ‘) = Ξ£π‘ β π (πβπ‘)) |
29 | 28 | eqeq1d 2738 |
. . . . . . . 8
β’ (π = π β (Ξ£π‘ β π (πβπ‘) = π β Ξ£π‘ β π (πβπ‘) = π)) |
30 | 29 | rabbidv 3415 |
. . . . . . 7
β’ (π = π β {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
31 | | oveq2 7365 |
. . . . . . . 8
β’ (π = π β ((0...π) βm π) = ((0...π) βm π )) |
32 | | rabeq 3421 |
. . . . . . . 8
β’
(((0...π)
βm π) =
((0...π) βm
π ) β {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π}) |
33 | 31, 32 | syl 17 |
. . . . . . 7
β’ (π = π β {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π}) |
34 | 30, 33 | eqtrd 2776 |
. . . . . 6
β’ (π = π β {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π}) |
35 | 34 | mpteq2dv 5207 |
. . . . 5
β’ (π = π β (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) = (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) |
36 | 35 | cbvmptv 5218 |
. . . 4
β’ (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π})) = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) |
37 | 27, 36 | eqtri 2764 |
. . 3
β’ (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π’ β π (πβπ’) = π})) = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) |
38 | | dvnprod.c |
. . . 4
β’ πΆ = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
39 | | fveq1 6841 |
. . . . . . . 8
β’ (π = π β (πβπ‘) = (πβπ‘)) |
40 | 39 | sumeq2sdv 15589 |
. . . . . . 7
β’ (π = π β Ξ£π‘ β π (πβπ‘) = Ξ£π‘ β π (πβπ‘)) |
41 | 40 | eqeq1d 2738 |
. . . . . 6
β’ (π = π β (Ξ£π‘ β π (πβπ‘) = π β Ξ£π‘ β π (πβπ‘) = π)) |
42 | 41 | cbvrabv 3417 |
. . . . 5
β’ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π} |
43 | 42 | mpteq2i 5210 |
. . . 4
β’ (π β β0
β¦ {π β
((0...π) βm
π) β£ Ξ£π‘ β π (πβπ‘) = π}) = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
44 | 38, 43 | eqtri 2764 |
. . 3
β’ πΆ = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) |
45 | 1, 2, 3, 4, 5, 6, 7, 37, 44 | dvnprodlem3 44179 |
. 2
β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
46 | | fveq1 6841 |
. . . . . . . . . 10
β’ (π = π β (πβπ‘) = (πβπ‘)) |
47 | 46 | fveq2d 6846 |
. . . . . . . . 9
β’ (π = π β (!β(πβπ‘)) = (!β(πβπ‘))) |
48 | 47 | prodeq2ad 43823 |
. . . . . . . 8
β’ (π = π β βπ‘ β π (!β(πβπ‘)) = βπ‘ β π (!β(πβπ‘))) |
49 | 48 | oveq2d 7373 |
. . . . . . 7
β’ (π = π β ((!βπ) / βπ‘ β π (!β(πβπ‘))) = ((!βπ) / βπ‘ β π (!β(πβπ‘)))) |
50 | 46 | fveq2d 6846 |
. . . . . . . . 9
β’ (π = π β ((π Dπ (π»βπ‘))β(πβπ‘)) = ((π Dπ (π»βπ‘))β(πβπ‘))) |
51 | 50 | fveq1d 6844 |
. . . . . . . 8
β’ (π = π β (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) = (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
52 | 51 | prodeq2ad 43823 |
. . . . . . 7
β’ (π = π β βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) = βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
53 | 49, 52 | oveq12d 7375 |
. . . . . 6
β’ (π = π β (((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) = (((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
54 | 53 | cbvsumv 15581 |
. . . . 5
β’
Ξ£π β
(πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) = Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
55 | | eqid 2736 |
. . . . 5
β’
Ξ£π β
(πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) = Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
56 | 54, 55 | eqtri 2764 |
. . . 4
β’
Ξ£π β
(πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) = Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
57 | 56 | mpteq2i 5210 |
. . 3
β’ (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
58 | 57 | a1i 11 |
. 2
β’ (π β (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
59 | 45, 58 | eqtrd 2776 |
1
β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |