Step | Hyp | Ref
| Expression |
1 | | itgsubst.le |
. . 3
β’ (π β π β€ π) |
2 | 1 | ditgpos 25236 |
. 2
β’ (π β β¨[π β π](πΈ Β· π΅) dπ₯ = β«(π(,)π)(πΈ Β· π΅) dπ₯) |
3 | | itgsubst.x |
. . . 4
β’ (π β π β β) |
4 | | itgsubst.y |
. . . 4
β’ (π β π β β) |
5 | | ax-resscn 11115 |
. . . . . . . 8
β’ β
β β |
6 | 5 | a1i 11 |
. . . . . . 7
β’ (π β β β
β) |
7 | | iccssre 13353 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π[,]π) β β) |
8 | 3, 4, 7 | syl2anc 585 |
. . . . . . 7
β’ (π β (π[,]π) β β) |
9 | | itgsubst.cl2 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π[,]π)) β π΄ β (π(,)π)) |
10 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (π β (π₯ β (π[,]π) β¦ π΄) = (π₯ β (π[,]π) β¦ π΄)) |
11 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (π β (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’) = (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’)) |
12 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π£ = π΄ β (π(,)π£) = (π(,)π΄)) |
13 | | itgeq1 25153 |
. . . . . . . . . . . 12
β’ ((π(,)π£) = (π(,)π΄) β β«(π(,)π£)πΆ dπ’ = β«(π(,)π΄)πΆ dπ’) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
β’ (π£ = π΄ β β«(π(,)π£)πΆ dπ’ = β«(π(,)π΄)πΆ dπ’) |
15 | 9, 10, 11, 14 | fmptco 7080 |
. . . . . . . . . 10
β’ (π β ((π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’) β (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)) |
16 | 9 | fmpttd 7068 |
. . . . . . . . . . . 12
β’ (π β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆ(π(,)π)) |
17 | | ioossicc 13357 |
. . . . . . . . . . . . . . 15
β’ (π(,)π) β (π[,]π) |
18 | | itgsubst.z |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β*) |
19 | | itgsubst.w |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β*) |
20 | | itgsubst.m |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (π(,)π)) |
21 | | eliooord 13330 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π(,)π) β (π < π β§ π < π)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π < π β§ π < π)) |
23 | 22 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ (π β π < π) |
24 | | itgsubst.n |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (π(,)π)) |
25 | | eliooord 13330 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π(,)π) β (π < π β§ π < π)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π < π β§ π < π)) |
27 | 26 | simprd 497 |
. . . . . . . . . . . . . . . 16
β’ (π β π < π) |
28 | | iccssioo 13340 |
. . . . . . . . . . . . . . . 16
β’ (((π β β*
β§ π β
β*) β§ (π < π β§ π < π)) β (π[,]π) β (π(,)π)) |
29 | 18, 19, 23, 27, 28 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’ (π β (π[,]π) β (π(,)π)) |
30 | 17, 29 | sstrid 3960 |
. . . . . . . . . . . . . 14
β’ (π β (π(,)π) β (π(,)π)) |
31 | | ioossre 13332 |
. . . . . . . . . . . . . . . 16
β’ (π(,)π) β β |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (π(,)π) β β) |
33 | 32, 5 | sstrdi 3961 |
. . . . . . . . . . . . . 14
β’ (π β (π(,)π) β β) |
34 | 30, 33 | sstrd 3959 |
. . . . . . . . . . . . 13
β’ (π β (π(,)π) β β) |
35 | | itgsubst.a |
. . . . . . . . . . . . 13
β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π))) |
36 | | cncfcdm 24277 |
. . . . . . . . . . . . 13
β’ (((π(,)π) β β β§ (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π))) β ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π)) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆ(π(,)π))) |
37 | 34, 35, 36 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π)) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆ(π(,)π))) |
38 | 16, 37 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π))) |
39 | 17 | sseli 3945 |
. . . . . . . . . . . . . 14
β’ (π£ β (π(,)π) β π£ β (π[,]π)) |
40 | 31, 24 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β) |
41 | 40 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β
β*) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π£ β (π[,]π)) β π β
β*) |
43 | 31, 20 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
44 | | elicc2 13336 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β) β (π£ β (π[,]π) β (π£ β β β§ π β€ π£ β§ π£ β€ π))) |
45 | 43, 40, 44 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π£ β (π[,]π) β (π£ β β β§ π β€ π£ β§ π£ β€ π))) |
46 | 45 | biimpa 478 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π£ β (π[,]π)) β (π£ β β β§ π β€ π£ β§ π£ β€ π)) |
47 | 46 | simp3d 1145 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π£ β (π[,]π)) β π£ β€ π) |
48 | | iooss2 13307 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β*
β§ π£ β€ π) β (π(,)π£) β (π(,)π)) |
49 | 42, 47, 48 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π£ β (π[,]π)) β (π(,)π£) β (π(,)π)) |
50 | 49 | sselda 3949 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β (π[,]π)) β§ π’ β (π(,)π£)) β π’ β (π(,)π)) |
51 | 30 | sselda 3949 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π(,)π)) β π’ β (π(,)π)) |
52 | | itgsubst.c |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π’ β (π(,)π) β¦ πΆ) β ((π(,)π)βcnββ)) |
53 | | cncff 24272 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π’ β (π(,)π) β¦ πΆ) β ((π(,)π)βcnββ) β (π’ β (π(,)π) β¦ πΆ):(π(,)π)βΆβ) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π’ β (π(,)π) β¦ πΆ):(π(,)π)βΆβ) |
55 | 54 | fvmptelcdm 7066 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π(,)π)) β πΆ β β) |
56 | 51, 55 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π(,)π)) β πΆ β β) |
57 | 56 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β (π[,]π)) β§ π’ β (π(,)π)) β πΆ β β) |
58 | 50, 57 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β (π[,]π)) β§ π’ β (π(,)π£)) β πΆ β β) |
59 | | ioombl 24945 |
. . . . . . . . . . . . . . . . 17
β’ (π(,)π£) β dom vol |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π£ β (π[,]π)) β (π(,)π£) β dom vol) |
61 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π(,)π) β (π[,]π)) |
62 | | ioombl 24945 |
. . . . . . . . . . . . . . . . . . 19
β’ (π(,)π) β dom vol |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π(,)π) β dom vol) |
64 | 29 | sselda 3949 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β (π[,]π)) β π’ β (π(,)π)) |
65 | 64, 55 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π[,]π)) β πΆ β β) |
66 | 29 | resmptd 5999 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π’ β (π(,)π) β¦ πΆ) βΎ (π[,]π)) = (π’ β (π[,]π) β¦ πΆ)) |
67 | | rescncf 24276 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π[,]π) β (π(,)π) β ((π’ β (π(,)π) β¦ πΆ) β ((π(,)π)βcnββ) β ((π’ β (π(,)π) β¦ πΆ) βΎ (π[,]π)) β ((π[,]π)βcnββ))) |
68 | 29, 52, 67 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π’ β (π(,)π) β¦ πΆ) βΎ (π[,]π)) β ((π[,]π)βcnββ)) |
69 | 66, 68 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π’ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ)) |
70 | | cniccibl 25221 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β β§ (π’ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ)) β (π’ β (π[,]π) β¦ πΆ) β
πΏ1) |
71 | 43, 40, 69, 70 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π’ β (π[,]π) β¦ πΆ) β
πΏ1) |
72 | 61, 63, 65, 71 | iblss 25185 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π’ β (π(,)π) β¦ πΆ) β
πΏ1) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π£ β (π[,]π)) β (π’ β (π(,)π) β¦ πΆ) β
πΏ1) |
74 | 49, 60, 57, 73 | iblss 25185 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π£ β (π[,]π)) β (π’ β (π(,)π£) β¦ πΆ) β
πΏ1) |
75 | 58, 74 | itgcl 25164 |
. . . . . . . . . . . . . 14
β’ ((π β§ π£ β (π[,]π)) β β«(π(,)π£)πΆ dπ’ β β) |
76 | 39, 75 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ π£ β (π(,)π)) β β«(π(,)π£)πΆ dπ’ β β) |
77 | 76 | fmpttd 7068 |
. . . . . . . . . . . 12
β’ (π β (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’):(π(,)π)βΆβ) |
78 | 30, 31 | sstrdi 3961 |
. . . . . . . . . . . 12
β’ (π β (π(,)π) β β) |
79 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π’ β ((π’ β (π(,)π) β¦ πΆ)βπ‘) = ((π’ β (π(,)π) β¦ πΆ)βπ’)) |
80 | | nffvmpt1 6858 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π’((π’ β (π(,)π) β¦ πΆ)βπ‘) |
81 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π‘((π’ β (π(,)π) β¦ πΆ)βπ’) |
82 | 79, 80, 81 | cbvitg 25156 |
. . . . . . . . . . . . . . . . . 18
β’
β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ‘) dπ‘ = β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ’) dπ’ |
83 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π’ β (π(,)π) β¦ πΆ) = (π’ β (π(,)π) β¦ πΆ) |
84 | 83 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π’ β (π(,)π) β§ πΆ β β) β ((π’ β (π(,)π) β¦ πΆ)βπ’) = πΆ) |
85 | 50, 58, 84 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π£ β (π[,]π)) β§ π’ β (π(,)π£)) β ((π’ β (π(,)π) β¦ πΆ)βπ’) = πΆ) |
86 | 85 | itgeq2dv 25162 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π£ β (π[,]π)) β β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ’) dπ’ = β«(π(,)π£)πΆ dπ’) |
87 | 82, 86 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π£ β (π[,]π)) β β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ‘) dπ‘ = β«(π(,)π£)πΆ dπ’) |
88 | 87 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . 16
β’ (π β (π£ β (π[,]π) β¦ β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ‘) dπ‘) = (π£ β (π[,]π) β¦ β«(π(,)π£)πΆ dπ’)) |
89 | 88 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π β (β D (π£ β (π[,]π) β¦ β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ‘) dπ‘)) = (β D (π£ β (π[,]π) β¦ β«(π(,)π£)πΆ dπ’))) |
90 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (π£ β (π[,]π) β¦ β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ‘) dπ‘) = (π£ β (π[,]π) β¦ β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ‘) dπ‘) |
91 | 3 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β
β*) |
92 | 4 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β
β*) |
93 | | lbicc2 13388 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
94 | 91, 92, 1, 93 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (π[,]π)) |
95 | | n0i 4298 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π[,]π) β Β¬ (π[,]π) = β
) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Β¬ (π[,]π) = β
) |
97 | | feq3 6656 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π(,)π) = β
β ((π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆ(π(,)π) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ
)) |
98 | 16, 97 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π(,)π) = β
β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ
)) |
99 | | f00 6729 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ
β ((π₯ β (π[,]π) β¦ π΄) = β
β§ (π[,]π) = β
)) |
100 | 99 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ
β (π[,]π) = β
) |
101 | 98, 100 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π(,)π) = β
β (π[,]π) = β
)) |
102 | 96, 101 | mtod 197 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Β¬ (π(,)π) = β
) |
103 | 43 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β
β*) |
104 | | ioo0 13296 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β*
β§ π β
β*) β ((π(,)π) = β
β π β€ π)) |
105 | 103, 41, 104 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π(,)π) = β
β π β€ π)) |
106 | 102, 105 | mtbid 324 |
. . . . . . . . . . . . . . . . 17
β’ (π β Β¬ π β€ π) |
107 | 40, 43 | letrid 11314 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π β€ π β¨ π β€ π)) |
108 | 107 | ord 863 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Β¬ π β€ π β π β€ π)) |
109 | 106, 108 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ (π β π β€ π) |
110 | | resmpt 5996 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(,)π) β (π[,]π) β ((π’ β (π[,]π) β¦ πΆ) βΎ (π(,)π)) = (π’ β (π(,)π) β¦ πΆ)) |
111 | 17, 110 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β (π[,]π) β¦ πΆ) βΎ (π(,)π)) = (π’ β (π(,)π) β¦ πΆ) |
112 | | rescncf 24276 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(,)π) β (π[,]π) β ((π’ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ) β ((π’ β (π[,]π) β¦ πΆ) βΎ (π(,)π)) β ((π(,)π)βcnββ))) |
113 | 17, 69, 112 | mpsyl 68 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π’ β (π[,]π) β¦ πΆ) βΎ (π(,)π)) β ((π(,)π)βcnββ)) |
114 | 111, 113 | eqeltrrid 2843 |
. . . . . . . . . . . . . . . 16
β’ (π β (π’ β (π(,)π) β¦ πΆ) β ((π(,)π)βcnββ)) |
115 | 90, 43, 40, 109, 114, 72 | ftc1cn 25423 |
. . . . . . . . . . . . . . 15
β’ (π β (β D (π£ β (π[,]π) β¦ β«(π(,)π£)((π’ β (π(,)π) β¦ πΆ)βπ‘) dπ‘)) = (π’ β (π(,)π) β¦ πΆ)) |
116 | 29, 31 | sstrdi 3961 |
. . . . . . . . . . . . . . . 16
β’ (π β (π[,]π) β β) |
117 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(TopOpenββfld) =
(TopOpenββfld) |
118 | 117 | tgioo2 24182 |
. . . . . . . . . . . . . . . 16
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
119 | | iccntr 24200 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β
((intβ(topGenβran (,)))β(π[,]π)) = (π(,)π)) |
120 | 43, 40, 119 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β
((intβ(topGenβran (,)))β(π[,]π)) = (π(,)π)) |
121 | 6, 116, 75, 118, 117, 120 | dvmptntr 25351 |
. . . . . . . . . . . . . . 15
β’ (π β (β D (π£ β (π[,]π) β¦ β«(π(,)π£)πΆ dπ’)) = (β D (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’))) |
122 | 89, 115, 121 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . 14
β’ (π β (β D (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’)) = (π’ β (π(,)π) β¦ πΆ)) |
123 | 122 | dmeqd 5866 |
. . . . . . . . . . . . 13
β’ (π β dom (β D (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’)) = dom (π’ β (π(,)π) β¦ πΆ)) |
124 | 83, 56 | dmmptd 6651 |
. . . . . . . . . . . . 13
β’ (π β dom (π’ β (π(,)π) β¦ πΆ) = (π(,)π)) |
125 | 123, 124 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β dom (β D (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’)) = (π(,)π)) |
126 | | dvcn 25301 |
. . . . . . . . . . . 12
β’
(((β β β β§ (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’):(π(,)π)βΆβ β§ (π(,)π) β β) β§ dom (β D
(π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’)) = (π(,)π)) β (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’) β ((π(,)π)βcnββ)) |
127 | 6, 77, 78, 125, 126 | syl31anc 1374 |
. . . . . . . . . . 11
β’ (π β (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’) β ((π(,)π)βcnββ)) |
128 | 38, 127 | cncfco 24286 |
. . . . . . . . . 10
β’ (π β ((π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’) β (π₯ β (π[,]π) β¦ π΄)) β ((π[,]π)βcnββ)) |
129 | 15, 128 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (π β (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’) β ((π[,]π)βcnββ)) |
130 | | cncff 24272 |
. . . . . . . . 9
β’ ((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’) β ((π[,]π)βcnββ) β (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’):(π[,]π)βΆβ) |
131 | 129, 130 | syl 17 |
. . . . . . . 8
β’ (π β (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’):(π[,]π)βΆβ) |
132 | 131 | fvmptelcdm 7066 |
. . . . . . 7
β’ ((π β§ π₯ β (π[,]π)) β β«(π(,)π΄)πΆ dπ’ β β) |
133 | | iccntr 24200 |
. . . . . . . 8
β’ ((π β β β§ π β β) β
((intβ(topGenβran (,)))β(π[,]π)) = (π(,)π)) |
134 | 3, 4, 133 | syl2anc 585 |
. . . . . . 7
β’ (π β
((intβ(topGenβran (,)))β(π[,]π)) = (π(,)π)) |
135 | 6, 8, 132, 118, 117, 134 | dvmptntr 25351 |
. . . . . 6
β’ (π β (β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)) = (β D (π₯ β (π(,)π) β¦ β«(π(,)π΄)πΆ dπ’))) |
136 | | reelprrecn 11150 |
. . . . . . . 8
β’ β
β {β, β} |
137 | 136 | a1i 11 |
. . . . . . 7
β’ (π β β β {β,
β}) |
138 | | ioossicc 13357 |
. . . . . . . . 9
β’ (π(,)π) β (π[,]π) |
139 | 138 | sseli 3945 |
. . . . . . . 8
β’ (π₯ β (π(,)π) β π₯ β (π[,]π)) |
140 | 139, 9 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π₯ β (π(,)π)) β π΄ β (π(,)π)) |
141 | | itgsubst.b |
. . . . . . . . . . 11
β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β©
πΏ1)) |
142 | | elin 3931 |
. . . . . . . . . . 11
β’ ((π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1) β
((π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ) β§ (π₯ β (π(,)π) β¦ π΅) β
πΏ1)) |
143 | 141, 142 | sylib 217 |
. . . . . . . . . 10
β’ (π β ((π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ) β§ (π₯ β (π(,)π) β¦ π΅) β
πΏ1)) |
144 | 143 | simpld 496 |
. . . . . . . . 9
β’ (π β (π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ)) |
145 | | cncff 24272 |
. . . . . . . . 9
β’ ((π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ) β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ) |
146 | 144, 145 | syl 17 |
. . . . . . . 8
β’ (π β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ) |
147 | 146 | fvmptelcdm 7066 |
. . . . . . 7
β’ ((π β§ π₯ β (π(,)π)) β π΅ β β) |
148 | 56 | fmpttd 7068 |
. . . . . . . . 9
β’ (π β (π’ β (π(,)π) β¦ πΆ):(π(,)π)βΆβ) |
149 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π£πΆ |
150 | | nfcsb1v 3885 |
. . . . . . . . . . 11
β’
β²π’β¦π£ / π’β¦πΆ |
151 | | csbeq1a 3874 |
. . . . . . . . . . 11
β’ (π’ = π£ β πΆ = β¦π£ / π’β¦πΆ) |
152 | 149, 150,
151 | cbvmpt 5221 |
. . . . . . . . . 10
β’ (π’ β (π(,)π) β¦ πΆ) = (π£ β (π(,)π) β¦ β¦π£ / π’β¦πΆ) |
153 | 152 | fmpt 7063 |
. . . . . . . . 9
β’
(βπ£ β
(π(,)π)β¦π£ / π’β¦πΆ β β β (π’ β (π(,)π) β¦ πΆ):(π(,)π)βΆβ) |
154 | 148, 153 | sylibr 233 |
. . . . . . . 8
β’ (π β βπ£ β (π(,)π)β¦π£ / π’β¦πΆ β β) |
155 | 154 | r19.21bi 3237 |
. . . . . . 7
β’ ((π β§ π£ β (π(,)π)) β β¦π£ / π’β¦πΆ β β) |
156 | 31, 5 | sstri 3958 |
. . . . . . . . . 10
β’ (π(,)π) β β |
157 | | cncff 24272 |
. . . . . . . . . . . 12
β’ ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π)) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆ(π(,)π)) |
158 | 35, 157 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆ(π(,)π)) |
159 | 158 | fvmptelcdm 7066 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π[,]π)) β π΄ β (π(,)π)) |
160 | 156, 159 | sselid 3947 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π[,]π)) β π΄ β β) |
161 | 6, 8, 160, 118, 117, 134 | dvmptntr 25351 |
. . . . . . . 8
β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (β D (π₯ β (π(,)π) β¦ π΄))) |
162 | | itgsubst.da |
. . . . . . . 8
β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
163 | 161, 162 | eqtr3d 2779 |
. . . . . . 7
β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
164 | 122, 152 | eqtrdi 2793 |
. . . . . . 7
β’ (π β (β D (π£ β (π(,)π) β¦ β«(π(,)π£)πΆ dπ’)) = (π£ β (π(,)π) β¦ β¦π£ / π’β¦πΆ)) |
165 | | csbeq1 3863 |
. . . . . . 7
β’ (π£ = π΄ β β¦π£ / π’β¦πΆ = β¦π΄ / π’β¦πΆ) |
166 | 137, 137,
140, 147, 76, 155, 163, 164, 14, 165 | dvmptco 25352 |
. . . . . 6
β’ (π β (β D (π₯ β (π(,)π) β¦ β«(π(,)π΄)πΆ dπ’)) = (π₯ β (π(,)π) β¦ (β¦π΄ / π’β¦πΆ Β· π΅))) |
167 | | nfcvd 2909 |
. . . . . . . . . 10
β’ (π΄ β (π(,)π) β β²π’πΈ) |
168 | | itgsubst.e |
. . . . . . . . . 10
β’ (π’ = π΄ β πΆ = πΈ) |
169 | 167, 168 | csbiegf 3894 |
. . . . . . . . 9
β’ (π΄ β (π(,)π) β β¦π΄ / π’β¦πΆ = πΈ) |
170 | 140, 169 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(,)π)) β β¦π΄ / π’β¦πΆ = πΈ) |
171 | 170 | oveq1d 7377 |
. . . . . . 7
β’ ((π β§ π₯ β (π(,)π)) β (β¦π΄ / π’β¦πΆ Β· π΅) = (πΈ Β· π΅)) |
172 | 171 | mpteq2dva 5210 |
. . . . . 6
β’ (π β (π₯ β (π(,)π) β¦ (β¦π΄ / π’β¦πΆ Β· π΅)) = (π₯ β (π(,)π) β¦ (πΈ Β· π΅))) |
173 | 135, 166,
172 | 3eqtrd 2781 |
. . . . 5
β’ (π β (β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)) = (π₯ β (π(,)π) β¦ (πΈ Β· π΅))) |
174 | | resmpt 5996 |
. . . . . . . 8
β’ ((π(,)π) β (π[,]π) β ((π₯ β (π[,]π) β¦ πΈ) βΎ (π(,)π)) = (π₯ β (π(,)π) β¦ πΈ)) |
175 | 138, 174 | ax-mp 5 |
. . . . . . 7
β’ ((π₯ β (π[,]π) β¦ πΈ) βΎ (π(,)π)) = (π₯ β (π(,)π) β¦ πΈ) |
176 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π β (π’ β (π(,)π) β¦ πΆ) = (π’ β (π(,)π) β¦ πΆ)) |
177 | 159, 10, 176, 168 | fmptco 7080 |
. . . . . . . . 9
β’ (π β ((π’ β (π(,)π) β¦ πΆ) β (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π[,]π) β¦ πΈ)) |
178 | 35, 52 | cncfco 24286 |
. . . . . . . . 9
β’ (π β ((π’ β (π(,)π) β¦ πΆ) β (π₯ β (π[,]π) β¦ π΄)) β ((π[,]π)βcnββ)) |
179 | 177, 178 | eqeltrrd 2839 |
. . . . . . . 8
β’ (π β (π₯ β (π[,]π) β¦ πΈ) β ((π[,]π)βcnββ)) |
180 | | rescncf 24276 |
. . . . . . . 8
β’ ((π(,)π) β (π[,]π) β ((π₯ β (π[,]π) β¦ πΈ) β ((π[,]π)βcnββ) β ((π₯ β (π[,]π) β¦ πΈ) βΎ (π(,)π)) β ((π(,)π)βcnββ))) |
181 | 138, 179,
180 | mpsyl 68 |
. . . . . . 7
β’ (π β ((π₯ β (π[,]π) β¦ πΈ) βΎ (π(,)π)) β ((π(,)π)βcnββ)) |
182 | 175, 181 | eqeltrrid 2843 |
. . . . . 6
β’ (π β (π₯ β (π(,)π) β¦ πΈ) β ((π(,)π)βcnββ)) |
183 | 182, 144 | mulcncf 24826 |
. . . . 5
β’ (π β (π₯ β (π(,)π) β¦ (πΈ Β· π΅)) β ((π(,)π)βcnββ)) |
184 | 173, 183 | eqeltrd 2838 |
. . . 4
β’ (π β (β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)) β ((π(,)π)βcnββ)) |
185 | | ioombl 24945 |
. . . . . . . 8
β’ (π(,)π) β dom vol |
186 | 185 | a1i 11 |
. . . . . . 7
β’ (π β (π(,)π) β dom vol) |
187 | | fco 6697 |
. . . . . . . . . . 11
β’ (((π’ β (π(,)π) β¦ πΆ):(π(,)π)βΆβ β§ (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆ(π(,)π)) β ((π’ β (π(,)π) β¦ πΆ) β (π₯ β (π[,]π) β¦ π΄)):(π[,]π)βΆβ) |
188 | 54, 158, 187 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ((π’ β (π(,)π) β¦ πΆ) β (π₯ β (π[,]π) β¦ π΄)):(π[,]π)βΆβ) |
189 | 177 | feq1d 6658 |
. . . . . . . . . 10
β’ (π β (((π’ β (π(,)π) β¦ πΆ) β (π₯ β (π[,]π) β¦ π΄)):(π[,]π)βΆβ β (π₯ β (π[,]π) β¦ πΈ):(π[,]π)βΆβ)) |
190 | 188, 189 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π₯ β (π[,]π) β¦ πΈ):(π[,]π)βΆβ) |
191 | 190 | fvmptelcdm 7066 |
. . . . . . . 8
β’ ((π β§ π₯ β (π[,]π)) β πΈ β β) |
192 | 139, 191 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π₯ β (π(,)π)) β πΈ β β) |
193 | | eqidd 2738 |
. . . . . . 7
β’ (π β (π₯ β (π(,)π) β¦ πΈ) = (π₯ β (π(,)π) β¦ πΈ)) |
194 | | eqidd 2738 |
. . . . . . 7
β’ (π β (π₯ β (π(,)π) β¦ π΅) = (π₯ β (π(,)π) β¦ π΅)) |
195 | 186, 192,
147, 193, 194 | offval2 7642 |
. . . . . 6
β’ (π β ((π₯ β (π(,)π) β¦ πΈ) βf Β· (π₯ β (π(,)π) β¦ π΅)) = (π₯ β (π(,)π) β¦ (πΈ Β· π΅))) |
196 | 173, 195 | eqtr4d 2780 |
. . . . 5
β’ (π β (β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)) = ((π₯ β (π(,)π) β¦ πΈ) βf Β· (π₯ β (π(,)π) β¦ π΅))) |
197 | 138 | a1i 11 |
. . . . . . . 8
β’ (π β (π(,)π) β (π[,]π)) |
198 | | cniccibl 25221 |
. . . . . . . . 9
β’ ((π β β β§ π β β β§ (π₯ β (π[,]π) β¦ πΈ) β ((π[,]π)βcnββ)) β (π₯ β (π[,]π) β¦ πΈ) β
πΏ1) |
199 | 3, 4, 179, 198 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π₯ β (π[,]π) β¦ πΈ) β
πΏ1) |
200 | 197, 186,
191, 199 | iblss 25185 |
. . . . . . 7
β’ (π β (π₯ β (π(,)π) β¦ πΈ) β
πΏ1) |
201 | | iblmbf 25148 |
. . . . . . 7
β’ ((π₯ β (π(,)π) β¦ πΈ) β πΏ1 β (π₯ β (π(,)π) β¦ πΈ) β MblFn) |
202 | 200, 201 | syl 17 |
. . . . . 6
β’ (π β (π₯ β (π(,)π) β¦ πΈ) β MblFn) |
203 | 143 | simprd 497 |
. . . . . 6
β’ (π β (π₯ β (π(,)π) β¦ π΅) β
πΏ1) |
204 | | cniccbdd 24841 |
. . . . . . . 8
β’ ((π β β β§ π β β β§ (π₯ β (π[,]π) β¦ πΈ) β ((π[,]π)βcnββ)) β βπ¦ β β βπ§ β (π[,]π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦) |
205 | 3, 4, 179, 204 | syl3anc 1372 |
. . . . . . 7
β’ (π β βπ¦ β β βπ§ β (π[,]π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦) |
206 | | ssralv 4015 |
. . . . . . . . . 10
β’ ((π(,)π) β (π[,]π) β (βπ§ β (π[,]π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦ β βπ§ β (π(,)π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦)) |
207 | 138, 206 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ§ β
(π[,]π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦ β βπ§ β (π(,)π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦) |
208 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π₯ β (π(,)π) β¦ πΈ) = (π₯ β (π(,)π) β¦ πΈ) |
209 | 208, 192 | dmmptd 6651 |
. . . . . . . . . . 11
β’ (π β dom (π₯ β (π(,)π) β¦ πΈ) = (π(,)π)) |
210 | 209 | raleqdv 3316 |
. . . . . . . . . 10
β’ (π β (βπ§ β dom (π₯ β (π(,)π) β¦ πΈ)(absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦ β βπ§ β (π(,)π)(absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦)) |
211 | 175 | fveq1i 6848 |
. . . . . . . . . . . . . 14
β’ (((π₯ β (π[,]π) β¦ πΈ) βΎ (π(,)π))βπ§) = ((π₯ β (π(,)π) β¦ πΈ)βπ§) |
212 | | fvres 6866 |
. . . . . . . . . . . . . 14
β’ (π§ β (π(,)π) β (((π₯ β (π[,]π) β¦ πΈ) βΎ (π(,)π))βπ§) = ((π₯ β (π[,]π) β¦ πΈ)βπ§)) |
213 | 211, 212 | eqtr3id 2791 |
. . . . . . . . . . . . 13
β’ (π§ β (π(,)π) β ((π₯ β (π(,)π) β¦ πΈ)βπ§) = ((π₯ β (π[,]π) β¦ πΈ)βπ§)) |
214 | 213 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π§ β (π(,)π) β (absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) = (absβ((π₯ β (π[,]π) β¦ πΈ)βπ§))) |
215 | 214 | breq1d 5120 |
. . . . . . . . . . 11
β’ (π§ β (π(,)π) β ((absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦ β (absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦)) |
216 | 215 | ralbiia 3095 |
. . . . . . . . . 10
β’
(βπ§ β
(π(,)π)(absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦ β βπ§ β (π(,)π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦) |
217 | 210, 216 | bitr2di 288 |
. . . . . . . . 9
β’ (π β (βπ§ β (π(,)π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦ β βπ§ β dom (π₯ β (π(,)π) β¦ πΈ)(absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦)) |
218 | 207, 217 | imbitrid 243 |
. . . . . . . 8
β’ (π β (βπ§ β (π[,]π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦ β βπ§ β dom (π₯ β (π(,)π) β¦ πΈ)(absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦)) |
219 | 218 | reximdv 3168 |
. . . . . . 7
β’ (π β (βπ¦ β β βπ§ β (π[,]π)(absβ((π₯ β (π[,]π) β¦ πΈ)βπ§)) β€ π¦ β βπ¦ β β βπ§ β dom (π₯ β (π(,)π) β¦ πΈ)(absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦)) |
220 | 205, 219 | mpd 15 |
. . . . . 6
β’ (π β βπ¦ β β βπ§ β dom (π₯ β (π(,)π) β¦ πΈ)(absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦) |
221 | | bddmulibl 25219 |
. . . . . 6
β’ (((π₯ β (π(,)π) β¦ πΈ) β MblFn β§ (π₯ β (π(,)π) β¦ π΅) β πΏ1 β§
βπ¦ β β
βπ§ β dom (π₯ β (π(,)π) β¦ πΈ)(absβ((π₯ β (π(,)π) β¦ πΈ)βπ§)) β€ π¦) β ((π₯ β (π(,)π) β¦ πΈ) βf Β· (π₯ β (π(,)π) β¦ π΅)) β
πΏ1) |
222 | 202, 203,
220, 221 | syl3anc 1372 |
. . . . 5
β’ (π β ((π₯ β (π(,)π) β¦ πΈ) βf Β· (π₯ β (π(,)π) β¦ π΅)) β
πΏ1) |
223 | 196, 222 | eqeltrd 2838 |
. . . 4
β’ (π β (β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)) β
πΏ1) |
224 | 3, 4, 1, 184, 223, 129 | ftc2 25424 |
. . 3
β’ (π β β«(π(,)π)((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ‘) dπ‘ = (((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ) β ((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ))) |
225 | | fveq2 6847 |
. . . . 5
β’ (π‘ = π₯ β ((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ‘) = ((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ₯)) |
226 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯β |
227 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯
D |
228 | | nfmpt1 5218 |
. . . . . . 7
β’
β²π₯(π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’) |
229 | 226, 227,
228 | nfov 7392 |
. . . . . 6
β’
β²π₯(β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)) |
230 | | nfcv 2908 |
. . . . . 6
β’
β²π₯π‘ |
231 | 229, 230 | nffv 6857 |
. . . . 5
β’
β²π₯((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ‘) |
232 | | nfcv 2908 |
. . . . 5
β’
β²π‘((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ₯) |
233 | 225, 231,
232 | cbvitg 25156 |
. . . 4
β’
β«(π(,)π)((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ‘) dπ‘ = β«(π(,)π)((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ₯) dπ₯ |
234 | 173 | fveq1d 6849 |
. . . . . 6
β’ (π β ((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ₯) = ((π₯ β (π(,)π) β¦ (πΈ Β· π΅))βπ₯)) |
235 | | ovex 7395 |
. . . . . . 7
β’ (πΈ Β· π΅) β V |
236 | | eqid 2737 |
. . . . . . . 8
β’ (π₯ β (π(,)π) β¦ (πΈ Β· π΅)) = (π₯ β (π(,)π) β¦ (πΈ Β· π΅)) |
237 | 236 | fvmpt2 6964 |
. . . . . . 7
β’ ((π₯ β (π(,)π) β§ (πΈ Β· π΅) β V) β ((π₯ β (π(,)π) β¦ (πΈ Β· π΅))βπ₯) = (πΈ Β· π΅)) |
238 | 235, 237 | mpan2 690 |
. . . . . 6
β’ (π₯ β (π(,)π) β ((π₯ β (π(,)π) β¦ (πΈ Β· π΅))βπ₯) = (πΈ Β· π΅)) |
239 | 234, 238 | sylan9eq 2797 |
. . . . 5
β’ ((π β§ π₯ β (π(,)π)) β ((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ₯) = (πΈ Β· π΅)) |
240 | 239 | itgeq2dv 25162 |
. . . 4
β’ (π β β«(π(,)π)((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ₯) dπ₯ = β«(π(,)π)(πΈ Β· π΅) dπ₯) |
241 | 233, 240 | eqtrid 2789 |
. . 3
β’ (π β β«(π(,)π)((β D (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’))βπ‘) dπ‘ = β«(π(,)π)(πΈ Β· π΅) dπ₯) |
242 | 17, 9 | sselid 3947 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π[,]π)) β π΄ β (π[,]π)) |
243 | | elicc2 13336 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β (π΄ β (π[,]π) β (π΄ β β β§ π β€ π΄ β§ π΄ β€ π))) |
244 | 43, 40, 243 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π΄ β (π[,]π) β (π΄ β β β§ π β€ π΄ β§ π΄ β€ π))) |
245 | 244 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π[,]π)) β (π΄ β (π[,]π) β (π΄ β β β§ π β€ π΄ β§ π΄ β€ π))) |
246 | 242, 245 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π[,]π)) β (π΄ β β β§ π β€ π΄ β§ π΄ β€ π)) |
247 | 246 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π[,]π)) β π β€ π΄) |
248 | 247 | ditgpos 25236 |
. . . . . . . 8
β’ ((π β§ π₯ β (π[,]π)) β β¨[π β π΄]πΆ dπ’ = β«(π(,)π΄)πΆ dπ’) |
249 | 248 | mpteq2dva 5210 |
. . . . . . 7
β’ (π β (π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’) = (π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)) |
250 | 249 | fveq1d 6849 |
. . . . . 6
β’ (π β ((π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’)βπ) = ((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ)) |
251 | | ubicc2 13389 |
. . . . . . . 8
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
252 | 91, 92, 1, 251 | syl3anc 1372 |
. . . . . . 7
β’ (π β π β (π[,]π)) |
253 | | itgsubst.l |
. . . . . . . . 9
β’ (π₯ = π β π΄ = πΏ) |
254 | | ditgeq2 25229 |
. . . . . . . . 9
β’ (π΄ = πΏ β β¨[π β π΄]πΆ dπ’ = β¨[π β πΏ]πΆ dπ’) |
255 | 253, 254 | syl 17 |
. . . . . . . 8
β’ (π₯ = π β β¨[π β π΄]πΆ dπ’ = β¨[π β πΏ]πΆ dπ’) |
256 | | eqid 2737 |
. . . . . . . 8
β’ (π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’) = (π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’) |
257 | | ditgex 25232 |
. . . . . . . 8
β’
β¨[π β
πΏ]πΆ dπ’ β V |
258 | 255, 256,
257 | fvmpt 6953 |
. . . . . . 7
β’ (π β (π[,]π) β ((π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’)βπ) = β¨[π β πΏ]πΆ dπ’) |
259 | 252, 258 | syl 17 |
. . . . . 6
β’ (π β ((π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’)βπ) = β¨[π β πΏ]πΆ dπ’) |
260 | 250, 259 | eqtr3d 2779 |
. . . . 5
β’ (π β ((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ) = β¨[π β πΏ]πΆ dπ’) |
261 | 249 | fveq1d 6849 |
. . . . . 6
β’ (π β ((π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’)βπ) = ((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ)) |
262 | | itgsubst.k |
. . . . . . . . 9
β’ (π₯ = π β π΄ = πΎ) |
263 | | ditgeq2 25229 |
. . . . . . . . 9
β’ (π΄ = πΎ β β¨[π β π΄]πΆ dπ’ = β¨[π β πΎ]πΆ dπ’) |
264 | 262, 263 | syl 17 |
. . . . . . . 8
β’ (π₯ = π β β¨[π β π΄]πΆ dπ’ = β¨[π β πΎ]πΆ dπ’) |
265 | | ditgex 25232 |
. . . . . . . 8
β’
β¨[π β
πΎ]πΆ dπ’ β V |
266 | 264, 256,
265 | fvmpt 6953 |
. . . . . . 7
β’ (π β (π[,]π) β ((π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’)βπ) = β¨[π β πΎ]πΆ dπ’) |
267 | 94, 266 | syl 17 |
. . . . . 6
β’ (π β ((π₯ β (π[,]π) β¦ β¨[π β π΄]πΆ dπ’)βπ) = β¨[π β πΎ]πΆ dπ’) |
268 | 261, 267 | eqtr3d 2779 |
. . . . 5
β’ (π β ((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ) = β¨[π β πΎ]πΆ dπ’) |
269 | 260, 268 | oveq12d 7380 |
. . . 4
β’ (π β (((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ) β ((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ)) = (β¨[π β πΏ]πΆ dπ’ β β¨[π β πΎ]πΆ dπ’)) |
270 | | lbicc2 13388 |
. . . . . . 7
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
271 | 103, 41, 109, 270 | syl3anc 1372 |
. . . . . 6
β’ (π β π β (π[,]π)) |
272 | 262 | eleq1d 2823 |
. . . . . . 7
β’ (π₯ = π β (π΄ β (π[,]π) β πΎ β (π[,]π))) |
273 | 242 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ₯ β (π[,]π)π΄ β (π[,]π)) |
274 | 272, 273,
94 | rspcdva 3585 |
. . . . . 6
β’ (π β πΎ β (π[,]π)) |
275 | 253 | eleq1d 2823 |
. . . . . . 7
β’ (π₯ = π β (π΄ β (π[,]π) β πΏ β (π[,]π))) |
276 | 275, 273,
252 | rspcdva 3585 |
. . . . . 6
β’ (π β πΏ β (π[,]π)) |
277 | 43, 40, 271, 274, 276, 56, 72 | ditgsplit 25241 |
. . . . 5
β’ (π β β¨[π β πΏ]πΆ dπ’ = (β¨[π β πΎ]πΆ dπ’ + β¨[πΎ β πΏ]πΆ dπ’)) |
278 | 277 | oveq1d 7377 |
. . . 4
β’ (π β (β¨[π β πΏ]πΆ dπ’ β β¨[π β πΎ]πΆ dπ’) = ((β¨[π β πΎ]πΆ dπ’ + β¨[πΎ β πΏ]πΆ dπ’) β β¨[π β πΎ]πΆ dπ’)) |
279 | 43, 40, 271, 274, 56, 72 | ditgcl 25238 |
. . . . 5
β’ (π β β¨[π β πΎ]πΆ dπ’ β β) |
280 | 43, 40, 274, 276, 56, 72 | ditgcl 25238 |
. . . . 5
β’ (π β β¨[πΎ β πΏ]πΆ dπ’ β β) |
281 | 279, 280 | pncan2d 11521 |
. . . 4
β’ (π β ((β¨[π β πΎ]πΆ dπ’ + β¨[πΎ β πΏ]πΆ dπ’) β β¨[π β πΎ]πΆ dπ’) = β¨[πΎ β πΏ]πΆ dπ’) |
282 | 269, 278,
281 | 3eqtrd 2781 |
. . 3
β’ (π β (((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ) β ((π₯ β (π[,]π) β¦ β«(π(,)π΄)πΆ dπ’)βπ)) = β¨[πΎ β πΏ]πΆ dπ’) |
283 | 224, 241,
282 | 3eqtr3d 2785 |
. 2
β’ (π β β«(π(,)π)(πΈ Β· π΅) dπ₯ = β¨[πΎ β πΏ]πΆ dπ’) |
284 | 2, 283 | eqtr2d 2778 |
1
β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) |