Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . 3
β’ ((π β§ π΄ β€ π΅) β π΄ β€ π΅) |
2 | 1 | ditgpos 25236 |
. 2
β’ ((π β§ π΄ β€ π΅) β β¨[π΄ β π΅]((β D πΉ)βπ‘) dπ‘ = β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘) |
3 | | ftc2ditg.x |
. . . . . . 7
β’ (π β π β β) |
4 | | ftc2ditg.y |
. . . . . . 7
β’ (π β π β β) |
5 | | iccssre 13353 |
. . . . . . 7
β’ ((π β β β§ π β β) β (π[,]π) β β) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . . 6
β’ (π β (π[,]π) β β) |
7 | | ftc2ditg.a |
. . . . . 6
β’ (π β π΄ β (π[,]π)) |
8 | 6, 7 | sseldd 3950 |
. . . . 5
β’ (π β π΄ β β) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β€ π΅) β π΄ β β) |
10 | | ftc2ditg.b |
. . . . . 6
β’ (π β π΅ β (π[,]π)) |
11 | 6, 10 | sseldd 3950 |
. . . . 5
β’ (π β π΅ β β) |
12 | 11 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β€ π΅) β π΅ β β) |
13 | | ax-resscn 11115 |
. . . . . . . 8
β’ β
β β |
14 | 13 | a1i 11 |
. . . . . . 7
β’ ((π β§ π΄ β€ π΅) β β β
β) |
15 | | ftc2ditg.f |
. . . . . . . . 9
β’ (π β πΉ β ((π[,]π)βcnββ)) |
16 | | cncff 24272 |
. . . . . . . . 9
β’ (πΉ β ((π[,]π)βcnββ) β πΉ:(π[,]π)βΆβ) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:(π[,]π)βΆβ) |
18 | 17 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β€ π΅) β πΉ:(π[,]π)βΆβ) |
19 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β€ π΅) β (π[,]π) β β) |
20 | | iccssre 13353 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
21 | 8, 11, 20 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄[,]π΅) β β) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β€ π΅) β (π΄[,]π΅) β β) |
23 | | eqid 2737 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
24 | 23 | tgioo2 24182 |
. . . . . . . 8
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
25 | 23, 24 | dvres 25291 |
. . . . . . 7
β’
(((β β β β§ πΉ:(π[,]π)βΆβ) β§ ((π[,]π) β β β§ (π΄[,]π΅) β β)) β (β D (πΉ βΎ (π΄[,]π΅))) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅)))) |
26 | 14, 18, 19, 22, 25 | syl22anc 838 |
. . . . . 6
β’ ((π β§ π΄ β€ π΅) β (β D (πΉ βΎ (π΄[,]π΅))) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅)))) |
27 | | iccntr 24200 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
28 | 8, 11, 27 | syl2anc 585 |
. . . . . . . 8
β’ (π β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β€ π΅) β ((intβ(topGenβran
(,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
30 | 29 | reseq2d 5942 |
. . . . . 6
β’ ((π β§ π΄ β€ π΅) β ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅))) = ((β D πΉ) βΎ (π΄(,)π΅))) |
31 | 26, 30 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π΄ β€ π΅) β (β D (πΉ βΎ (π΄[,]π΅))) = ((β D πΉ) βΎ (π΄(,)π΅))) |
32 | 3 | rexrd 11212 |
. . . . . . . . 9
β’ (π β π β
β*) |
33 | | elicc2 13336 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β (π΄ β (π[,]π) β (π΄ β β β§ π β€ π΄ β§ π΄ β€ π))) |
34 | 3, 4, 33 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π΄ β (π[,]π) β (π΄ β β β§ π β€ π΄ β§ π΄ β€ π))) |
35 | 7, 34 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (π΄ β β β§ π β€ π΄ β§ π΄ β€ π)) |
36 | 35 | simp2d 1144 |
. . . . . . . . 9
β’ (π β π β€ π΄) |
37 | | iooss1 13306 |
. . . . . . . . 9
β’ ((π β β*
β§ π β€ π΄) β (π΄(,)π΅) β (π(,)π΅)) |
38 | 32, 36, 37 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β (π(,)π΅)) |
39 | 4 | rexrd 11212 |
. . . . . . . . 9
β’ (π β π β
β*) |
40 | | elicc2 13336 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β (π΅ β (π[,]π) β (π΅ β β β§ π β€ π΅ β§ π΅ β€ π))) |
41 | 3, 4, 40 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π΅ β (π[,]π) β (π΅ β β β§ π β€ π΅ β§ π΅ β€ π))) |
42 | 10, 41 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (π΅ β β β§ π β€ π΅ β§ π΅ β€ π)) |
43 | 42 | simp3d 1145 |
. . . . . . . . 9
β’ (π β π΅ β€ π) |
44 | | iooss2 13307 |
. . . . . . . . 9
β’ ((π β β*
β§ π΅ β€ π) β (π(,)π΅) β (π(,)π)) |
45 | 39, 43, 44 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π(,)π΅) β (π(,)π)) |
46 | 38, 45 | sstrd 3959 |
. . . . . . 7
β’ (π β (π΄(,)π΅) β (π(,)π)) |
47 | 46 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β€ π΅) β (π΄(,)π΅) β (π(,)π)) |
48 | | ftc2ditg.c |
. . . . . . 7
β’ (π β (β D πΉ) β ((π(,)π)βcnββ)) |
49 | 48 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β€ π΅) β (β D πΉ) β ((π(,)π)βcnββ)) |
50 | | rescncf 24276 |
. . . . . 6
β’ ((π΄(,)π΅) β (π(,)π) β ((β D πΉ) β ((π(,)π)βcnββ) β ((β D πΉ) βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ))) |
51 | 47, 49, 50 | sylc 65 |
. . . . 5
β’ ((π β§ π΄ β€ π΅) β ((β D πΉ) βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) |
52 | 31, 51 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π΄ β€ π΅) β (β D (πΉ βΎ (π΄[,]π΅))) β ((π΄(,)π΅)βcnββ)) |
53 | | cncff 24272 |
. . . . . . . . . . 11
β’ ((β
D πΉ) β ((π(,)π)βcnββ) β (β D πΉ):(π(,)π)βΆβ) |
54 | 48, 53 | syl 17 |
. . . . . . . . . 10
β’ (π β (β D πΉ):(π(,)π)βΆβ) |
55 | 54 | feqmptd 6915 |
. . . . . . . . 9
β’ (π β (β D πΉ) = (π‘ β (π(,)π) β¦ ((β D πΉ)βπ‘))) |
56 | 55 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΄ β€ π΅) β (β D πΉ) = (π‘ β (π(,)π) β¦ ((β D πΉ)βπ‘))) |
57 | 56 | reseq1d 5941 |
. . . . . . 7
β’ ((π β§ π΄ β€ π΅) β ((β D πΉ) βΎ (π΄(,)π΅)) = ((π‘ β (π(,)π) β¦ ((β D πΉ)βπ‘)) βΎ (π΄(,)π΅))) |
58 | 47 | resmptd 5999 |
. . . . . . 7
β’ ((π β§ π΄ β€ π΅) β ((π‘ β (π(,)π) β¦ ((β D πΉ)βπ‘)) βΎ (π΄(,)π΅)) = (π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘))) |
59 | 57, 58 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π΄ β€ π΅) β ((β D πΉ) βΎ (π΄(,)π΅)) = (π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘))) |
60 | 31, 59 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π΄ β€ π΅) β (β D (πΉ βΎ (π΄[,]π΅))) = (π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘))) |
61 | | ioombl 24945 |
. . . . . . 7
β’ (π΄(,)π΅) β dom vol |
62 | 61 | a1i 11 |
. . . . . 6
β’ ((π β§ π΄ β€ π΅) β (π΄(,)π΅) β dom vol) |
63 | | fvexd 6862 |
. . . . . 6
β’ (((π β§ π΄ β€ π΅) β§ π‘ β (π(,)π)) β ((β D πΉ)βπ‘) β V) |
64 | | ftc2ditg.i |
. . . . . . . 8
β’ (π β (β D πΉ) β
πΏ1) |
65 | 64 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β€ π΅) β (β D πΉ) β
πΏ1) |
66 | 56, 65 | eqeltrrd 2839 |
. . . . . 6
β’ ((π β§ π΄ β€ π΅) β (π‘ β (π(,)π) β¦ ((β D πΉ)βπ‘)) β
πΏ1) |
67 | 47, 62, 63, 66 | iblss 25185 |
. . . . 5
β’ ((π β§ π΄ β€ π΅) β (π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘)) β
πΏ1) |
68 | 60, 67 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π΄ β€ π΅) β (β D (πΉ βΎ (π΄[,]π΅))) β
πΏ1) |
69 | | iccss2 13342 |
. . . . . . 7
β’ ((π΄ β (π[,]π) β§ π΅ β (π[,]π)) β (π΄[,]π΅) β (π[,]π)) |
70 | 7, 10, 69 | syl2anc 585 |
. . . . . 6
β’ (π β (π΄[,]π΅) β (π[,]π)) |
71 | | rescncf 24276 |
. . . . . 6
β’ ((π΄[,]π΅) β (π[,]π) β (πΉ β ((π[,]π)βcnββ) β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ))) |
72 | 70, 15, 71 | sylc 65 |
. . . . 5
β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
73 | 72 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β€ π΅) β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
74 | 9, 12, 1, 52, 68, 73 | ftc2 25424 |
. . 3
β’ ((π β§ π΄ β€ π΅) β β«(π΄(,)π΅)((β D (πΉ βΎ (π΄[,]π΅)))βπ‘) dπ‘ = (((πΉ βΎ (π΄[,]π΅))βπ΅) β ((πΉ βΎ (π΄[,]π΅))βπ΄))) |
75 | 31 | fveq1d 6849 |
. . . . 5
β’ ((π β§ π΄ β€ π΅) β ((β D (πΉ βΎ (π΄[,]π΅)))βπ‘) = (((β D πΉ) βΎ (π΄(,)π΅))βπ‘)) |
76 | | fvres 6866 |
. . . . 5
β’ (π‘ β (π΄(,)π΅) β (((β D πΉ) βΎ (π΄(,)π΅))βπ‘) = ((β D πΉ)βπ‘)) |
77 | 75, 76 | sylan9eq 2797 |
. . . 4
β’ (((π β§ π΄ β€ π΅) β§ π‘ β (π΄(,)π΅)) β ((β D (πΉ βΎ (π΄[,]π΅)))βπ‘) = ((β D πΉ)βπ‘)) |
78 | 77 | itgeq2dv 25162 |
. . 3
β’ ((π β§ π΄ β€ π΅) β β«(π΄(,)π΅)((β D (πΉ βΎ (π΄[,]π΅)))βπ‘) dπ‘ = β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘) |
79 | 9 | rexrd 11212 |
. . . 4
β’ ((π β§ π΄ β€ π΅) β π΄ β
β*) |
80 | 12 | rexrd 11212 |
. . . 4
β’ ((π β§ π΄ β€ π΅) β π΅ β
β*) |
81 | | ubicc2 13389 |
. . . . 5
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΅ β (π΄[,]π΅)) |
82 | | lbicc2 13388 |
. . . . 5
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
83 | | fvres 6866 |
. . . . . 6
β’ (π΅ β (π΄[,]π΅) β ((πΉ βΎ (π΄[,]π΅))βπ΅) = (πΉβπ΅)) |
84 | | fvres 6866 |
. . . . . 6
β’ (π΄ β (π΄[,]π΅) β ((πΉ βΎ (π΄[,]π΅))βπ΄) = (πΉβπ΄)) |
85 | 83, 84 | oveqan12d 7381 |
. . . . 5
β’ ((π΅ β (π΄[,]π΅) β§ π΄ β (π΄[,]π΅)) β (((πΉ βΎ (π΄[,]π΅))βπ΅) β ((πΉ βΎ (π΄[,]π΅))βπ΄)) = ((πΉβπ΅) β (πΉβπ΄))) |
86 | 81, 82, 85 | syl2anc 585 |
. . . 4
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β (((πΉ βΎ (π΄[,]π΅))βπ΅) β ((πΉ βΎ (π΄[,]π΅))βπ΄)) = ((πΉβπ΅) β (πΉβπ΄))) |
87 | 79, 80, 1, 86 | syl3anc 1372 |
. . 3
β’ ((π β§ π΄ β€ π΅) β (((πΉ βΎ (π΄[,]π΅))βπ΅) β ((πΉ βΎ (π΄[,]π΅))βπ΄)) = ((πΉβπ΅) β (πΉβπ΄))) |
88 | 74, 78, 87 | 3eqtr3d 2785 |
. 2
β’ ((π β§ π΄ β€ π΅) β β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) |
89 | 2, 88 | eqtrd 2777 |
1
β’ ((π β§ π΄ β€ π΅) β β¨[π΄ β π΅]((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) |