Step | Hyp | Ref
| Expression |
1 | | ftc2nc.a |
. . . . . . 7
β’ (π β π΄ β β) |
2 | 1 | rexrd 11206 |
. . . . . 6
β’ (π β π΄ β
β*) |
3 | | ftc2nc.b |
. . . . . . 7
β’ (π β π΅ β β) |
4 | 3 | rexrd 11206 |
. . . . . 6
β’ (π β π΅ β
β*) |
5 | | ftc2nc.le |
. . . . . 6
β’ (π β π΄ β€ π΅) |
6 | | ubicc2 13383 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΅ β (π΄[,]π΅)) |
7 | 2, 4, 5, 6 | syl3anc 1372 |
. . . . 5
β’ (π β π΅ β (π΄[,]π΅)) |
8 | | fvex 6856 |
. . . . . 6
β’ ((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄) β V |
9 | 8 | fvconst2 7154 |
. . . . 5
β’ (π΅ β (π΄[,]π΅) β (((π΄[,]π΅) Γ {((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄)})βπ΅) = ((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄)) |
10 | 7, 9 | syl 17 |
. . . 4
β’ (π β (((π΄[,]π΅) Γ {((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄)})βπ΅) = ((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄)) |
11 | | eqid 2737 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
12 | 11 | subcn 24232 |
. . . . . . . . 9
β’ β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ (π β β β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
14 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘) = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘) |
15 | | ssidd 3968 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β (π΄(,)π΅)) |
16 | | ioossre 13326 |
. . . . . . . . . 10
β’ (π΄(,)π΅) β β |
17 | 16 | a1i 11 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β β) |
18 | | ftc2nc.i |
. . . . . . . . 9
β’ (π β (β D πΉ) β
πΏ1) |
19 | | ftc2nc.c |
. . . . . . . . . 10
β’ (π β (β D πΉ) β ((π΄(,)π΅)βcnββ)) |
20 | | cncff 24259 |
. . . . . . . . . 10
β’ ((β
D πΉ) β ((π΄(,)π΅)βcnββ) β (β D πΉ):(π΄(,)π΅)βΆβ) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
β’ (π β (β D πΉ):(π΄(,)π΅)βΆβ) |
22 | | ioof 13365 |
. . . . . . . . . . . . 13
β’
(,):(β* Γ β*)βΆπ«
β |
23 | | ffun 6672 |
. . . . . . . . . . . . 13
β’
((,):(β* Γ β*)βΆπ«
β β Fun (,)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
β’ Fun
(,) |
25 | | fvelima 6909 |
. . . . . . . . . . . 12
β’ ((Fun (,)
β§ π β ((,) β
((π΄[,]π΅) Γ (π΄[,]π΅)))) β βπ₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))((,)βπ₯) = π ) |
26 | 24, 25 | mpan 689 |
. . . . . . . . . . 11
β’ (π β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅))) β βπ₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))((,)βπ₯) = π ) |
27 | | 1st2nd2 7961 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅)) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
28 | 27 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅)) β ((,)βπ₯) = ((,)ββ¨(1st
βπ₯), (2nd
βπ₯)β©)) |
29 | | df-ov 7361 |
. . . . . . . . . . . . . . . 16
β’
((1st βπ₯)(,)(2nd βπ₯)) = ((,)ββ¨(1st
βπ₯), (2nd
βπ₯)β©) |
30 | 28, 29 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
β’ (π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅)) β ((,)βπ₯) = ((1st βπ₯)(,)(2nd βπ₯))) |
31 | 30 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
β’ (π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅)) β (((,)βπ₯) = π β ((1st βπ₯)(,)(2nd βπ₯)) = π )) |
32 | 31 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (((,)βπ₯) = π β ((1st βπ₯)(,)(2nd βπ₯)) = π )) |
33 | 2, 4 | jca 513 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π΄ β β* β§ π΅ β
β*)) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π΄ β β* β§ π΅ β
β*)) |
35 | | xp1st 7954 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅)) β (1st βπ₯) β (π΄[,]π΅)) |
36 | | elicc1 13309 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄ β β*
β§ π΅ β
β*) β ((1st βπ₯) β (π΄[,]π΅) β ((1st βπ₯) β β*
β§ π΄ β€
(1st βπ₯)
β§ (1st βπ₯) β€ π΅))) |
37 | 2, 4, 36 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1st
βπ₯) β (π΄[,]π΅) β ((1st βπ₯) β β*
β§ π΄ β€
(1st βπ₯)
β§ (1st βπ₯) β€ π΅))) |
38 | 37 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (1st
βπ₯) β (π΄[,]π΅)) β ((1st βπ₯) β β*
β§ π΄ β€
(1st βπ₯)
β§ (1st βπ₯) β€ π΅)) |
39 | 38 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (1st
βπ₯) β (π΄[,]π΅)) β π΄ β€ (1st βπ₯)) |
40 | 35, 39 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β π΄ β€ (1st βπ₯)) |
41 | | xp2nd 7955 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅)) β (2nd βπ₯) β (π΄[,]π΅)) |
42 | | iccleub 13320 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β β*
β§ π΅ β
β* β§ (2nd βπ₯) β (π΄[,]π΅)) β (2nd βπ₯) β€ π΅) |
43 | 42 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄ β β*
β§ π΅ β
β*) β§ (2nd βπ₯) β (π΄[,]π΅)) β (2nd βπ₯) β€ π΅) |
44 | 33, 41, 43 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (2nd βπ₯) β€ π΅) |
45 | | ioossioo 13359 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β β*
β§ π΅ β
β*) β§ (π΄ β€ (1st βπ₯) β§ (2nd
βπ₯) β€ π΅)) β ((1st
βπ₯)(,)(2nd
βπ₯)) β (π΄(,)π΅)) |
46 | 34, 40, 44, 45 | syl12anc 836 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β ((1st βπ₯)(,)(2nd βπ₯)) β (π΄(,)π΅)) |
47 | 46 | sselda 3945 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β§ π‘ β ((1st βπ₯)(,)(2nd βπ₯))) β π‘ β (π΄(,)π΅)) |
48 | 21 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π‘ β (π΄(,)π΅)) β ((β D πΉ)βπ‘) β β) |
49 | 48 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β§ π‘ β (π΄(,)π΅)) β ((β D πΉ)βπ‘) β β) |
50 | 47, 49 | syldan 592 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β§ π‘ β ((1st βπ₯)(,)(2nd βπ₯))) β ((β D πΉ)βπ‘) β β) |
51 | | ioombl 24932 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ₯)(,)(2nd βπ₯)) β dom vol |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β ((1st βπ₯)(,)(2nd βπ₯)) β dom
vol) |
53 | | fvexd 6858 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β§ π‘ β (π΄(,)π΅)) β ((β D πΉ)βπ‘) β V) |
54 | 21 | feqmptd 6911 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β D πΉ) = (π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘))) |
55 | 54, 18 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘)) β
πΏ1) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘)) β
πΏ1) |
57 | 46, 52, 53, 56 | iblss 25172 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ ((β D πΉ)βπ‘)) β
πΏ1) |
58 | | ax-resscn 11109 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
β β |
59 | | ssid 3967 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
β β |
60 | | cncfss 24265 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β
β β β§ β β β) β (ββcnββ) β (ββcnββ)) |
61 | 58, 59, 60 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . 20
β’
(ββcnββ)
β (ββcnββ) |
62 | | abscncf 24267 |
. . . . . . . . . . . . . . . . . . . 20
β’ abs
β (ββcnββ) |
63 | 61, 62 | sselii 3942 |
. . . . . . . . . . . . . . . . . . 19
β’ abs
β (ββcnββ) |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β abs β (ββcnββ)) |
65 | 54 | reseq1d 5937 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((β D πΉ) βΎ ((1st
βπ₯)(,)(2nd
βπ₯))) = ((π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘)) βΎ ((1st βπ₯)(,)(2nd βπ₯)))) |
66 | 65 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β ((β D πΉ) βΎ ((1st βπ₯)(,)(2nd βπ₯))) = ((π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘)) βΎ ((1st βπ₯)(,)(2nd βπ₯)))) |
67 | 46 | resmptd 5995 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β ((π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘)) βΎ ((1st βπ₯)(,)(2nd βπ₯))) = (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ ((β D πΉ)βπ‘))) |
68 | 66, 67 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β ((β D πΉ) βΎ ((1st βπ₯)(,)(2nd βπ₯))) = (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ ((β D πΉ)βπ‘))) |
69 | 19 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (β D πΉ) β ((π΄(,)π΅)βcnββ)) |
70 | | rescncf 24263 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((1st βπ₯)(,)(2nd βπ₯)) β (π΄(,)π΅) β ((β D πΉ) β ((π΄(,)π΅)βcnββ) β ((β D πΉ) βΎ ((1st βπ₯)(,)(2nd βπ₯))) β (((1st
βπ₯)(,)(2nd
βπ₯))βcnββ))) |
71 | 46, 69, 70 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β ((β D πΉ) βΎ ((1st βπ₯)(,)(2nd βπ₯))) β (((1st
βπ₯)(,)(2nd
βπ₯))βcnββ)) |
72 | 68, 71 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ ((β D πΉ)βπ‘)) β (((1st βπ₯)(,)(2nd βπ₯))βcnββ)) |
73 | 64, 72 | cncfmpt1f 24280 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ (absβ((β
D πΉ)βπ‘))) β (((1st
βπ₯)(,)(2nd
βπ₯))βcnββ)) |
74 | | cnmbf 25026 |
. . . . . . . . . . . . . . . . 17
β’
((((1st βπ₯)(,)(2nd βπ₯)) β dom vol β§ (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ (absβ((β
D πΉ)βπ‘))) β (((1st
βπ₯)(,)(2nd
βπ₯))βcnββ)) β (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ (absβ((β
D πΉ)βπ‘))) β
MblFn) |
75 | 51, 73, 74 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ (absβ((β
D πΉ)βπ‘))) β
MblFn) |
76 | 50, 57 | itgcl 25151 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β β«((1st
βπ₯)(,)(2nd
βπ₯))((β D πΉ)βπ‘) dπ‘ β β) |
77 | 76 | cjcld 15082 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β
(βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘) β β) |
78 | | ioossre 13326 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((1st βπ₯)(,)(2nd βπ₯)) β β |
79 | 78, 58 | sstri 3954 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1st βπ₯)(,)(2nd βπ₯)) β β |
80 | | cncfmptc 24278 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘) β β β§ ((1st
βπ₯)(,)(2nd
βπ₯)) β β
β§ β β β) β (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦
(βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘)) β (((1st βπ₯)(,)(2nd βπ₯))βcnββ)) |
81 | 79, 59, 80 | mp3an23 1454 |
. . . . . . . . . . . . . . . . . . 19
β’
((βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘) β β β (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦
(βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘)) β (((1st βπ₯)(,)(2nd βπ₯))βcnββ)) |
82 | 77, 81 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦
(βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘)) β (((1st βπ₯)(,)(2nd βπ₯))βcnββ)) |
83 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π ((β D πΉ)βπ‘) |
84 | | nfcsb1v 3881 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π‘β¦π / π‘β¦((β D πΉ)βπ‘) |
85 | | csbeq1a 3870 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π β ((β D πΉ)βπ‘) = β¦π / π‘β¦((β D πΉ)βπ‘)) |
86 | 83, 84, 85 | cbvmpt 5217 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β ((1st
βπ₯)(,)(2nd
βπ₯)) β¦
((β D πΉ)βπ‘)) = (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦ β¦π / π‘β¦((β D πΉ)βπ‘)) |
87 | 86, 72 | eqeltrrid 2843 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦ β¦π / π‘β¦((β D πΉ)βπ‘)) β (((1st βπ₯)(,)(2nd βπ₯))βcnββ)) |
88 | 82, 87 | mulcncf 24813 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦
((βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘) Β· β¦π / π‘β¦((β D πΉ)βπ‘))) β (((1st βπ₯)(,)(2nd βπ₯))βcnββ)) |
89 | | cnmbf 25026 |
. . . . . . . . . . . . . . . . 17
β’
((((1st βπ₯)(,)(2nd βπ₯)) β dom vol β§ (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦
((βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘) Β· β¦π / π‘β¦((β D πΉ)βπ‘))) β (((1st βπ₯)(,)(2nd βπ₯))βcnββ)) β (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦
((βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘) Β· β¦π / π‘β¦((β D πΉ)βπ‘))) β MblFn) |
90 | 51, 88, 89 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π β ((1st βπ₯)(,)(2nd βπ₯)) β¦
((βββ«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘) Β· β¦π / π‘β¦((β D πΉ)βπ‘))) β MblFn) |
91 | 50, 57, 75, 90 | itgabsnc 36150 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (absββ«((1st
βπ₯)(,)(2nd
βπ₯))((β D πΉ)βπ‘) dπ‘) β€ β«((1st βπ₯)(,)(2nd βπ₯))(absβ((β D πΉ)βπ‘)) dπ‘) |
92 | 50 | abscld 15322 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β§ π‘ β ((1st βπ₯)(,)(2nd βπ₯))) β (absβ((β
D πΉ)βπ‘)) β
β) |
93 | | fvexd 6858 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β§ π‘ β ((1st βπ₯)(,)(2nd βπ₯))) β ((β D πΉ)βπ‘) β V) |
94 | 93, 57, 75 | iblabsnc 36145 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β¦ (absβ((β
D πΉ)βπ‘))) β
πΏ1) |
95 | 50 | absge0d 15330 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β§ π‘ β ((1st βπ₯)(,)(2nd βπ₯))) β 0 β€
(absβ((β D πΉ)βπ‘))) |
96 | 92, 94, 95 | itgposval 25163 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β β«((1st
βπ₯)(,)(2nd
βπ₯))(absβ((β D πΉ)βπ‘)) dπ‘ = (β«2β(π‘ β β β¦ if(π‘ β ((1st
βπ₯)(,)(2nd
βπ₯)),
(absβ((β D πΉ)βπ‘)), 0)))) |
97 | 91, 96 | breqtrd 5132 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (absββ«((1st
βπ₯)(,)(2nd
βπ₯))((β D πΉ)βπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β ((1st
βπ₯)(,)(2nd
βπ₯)),
(absβ((β D πΉ)βπ‘)), 0)))) |
98 | | itgeq1 25140 |
. . . . . . . . . . . . . . . 16
β’
(((1st βπ₯)(,)(2nd βπ₯)) = π β β«((1st βπ₯)(,)(2nd βπ₯))((β D πΉ)βπ‘) dπ‘ = β«π ((β D πΉ)βπ‘) dπ‘) |
99 | 98 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’
(((1st βπ₯)(,)(2nd βπ₯)) = π β (absββ«((1st
βπ₯)(,)(2nd
βπ₯))((β D πΉ)βπ‘) dπ‘) = (absββ«π ((β D πΉ)βπ‘) dπ‘)) |
100 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . 18
β’
(((1st βπ₯)(,)(2nd βπ₯)) = π β (π‘ β ((1st βπ₯)(,)(2nd βπ₯)) β π‘ β π )) |
101 | 100 | ifbid 4510 |
. . . . . . . . . . . . . . . . 17
β’
(((1st βπ₯)(,)(2nd βπ₯)) = π β if(π‘ β ((1st βπ₯)(,)(2nd βπ₯)), (absβ((β D πΉ)βπ‘)), 0) = if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0)) |
102 | 101 | mpteq2dv 5208 |
. . . . . . . . . . . . . . . 16
β’
(((1st βπ₯)(,)(2nd βπ₯)) = π β (π‘ β β β¦ if(π‘ β ((1st βπ₯)(,)(2nd βπ₯)), (absβ((β D πΉ)βπ‘)), 0)) = (π‘ β β β¦ if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0))) |
103 | 102 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’
(((1st βπ₯)(,)(2nd βπ₯)) = π β (β«2β(π‘ β β β¦ if(π‘ β ((1st
βπ₯)(,)(2nd
βπ₯)),
(absβ((β D πΉ)βπ‘)), 0))) = (β«2β(π‘ β β β¦ if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0)))) |
104 | 99, 103 | breq12d 5119 |
. . . . . . . . . . . . . 14
β’
(((1st βπ₯)(,)(2nd βπ₯)) = π β ((absββ«((1st
βπ₯)(,)(2nd
βπ₯))((β D πΉ)βπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β ((1st
βπ₯)(,)(2nd
βπ₯)),
(absβ((β D πΉ)βπ‘)), 0))) β (absββ«π ((β D πΉ)βπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0))))) |
105 | 97, 104 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (((1st βπ₯)(,)(2nd βπ₯)) = π β (absββ«π ((β D πΉ)βπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0))))) |
106 | 32, 105 | sylbid 239 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (((,)βπ₯) = π β (absββ«π ((β D πΉ)βπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0))))) |
107 | 106 | rexlimdva 3153 |
. . . . . . . . . . 11
β’ (π β (βπ₯ β ((π΄[,]π΅) Γ (π΄[,]π΅))((,)βπ₯) = π β (absββ«π ((β D πΉ)βπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0))))) |
108 | 26, 107 | syl5 34 |
. . . . . . . . . 10
β’ (π β (π β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅))) β (absββ«π ((β D πΉ)βπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0))))) |
109 | 108 | ralrimiv 3143 |
. . . . . . . . 9
β’ (π β βπ β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))(absββ«π ((β D πΉ)βπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ((β D πΉ)βπ‘)), 0)))) |
110 | 14, 1, 3, 5, 15, 17, 18, 21, 109 | ftc1anc 36162 |
. . . . . . . 8
β’ (π β (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘) β ((π΄[,]π΅)βcnββ)) |
111 | | ftc2nc.f |
. . . . . . . . . . 11
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
112 | | cncff 24259 |
. . . . . . . . . . 11
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
113 | 111, 112 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
114 | 113 | feqmptd 6911 |
. . . . . . . . 9
β’ (π β πΉ = (π₯ β (π΄[,]π΅) β¦ (πΉβπ₯))) |
115 | 114, 111 | eqeltrrd 2839 |
. . . . . . . 8
β’ (π β (π₯ β (π΄[,]π΅) β¦ (πΉβπ₯)) β ((π΄[,]π΅)βcnββ)) |
116 | 11, 13, 110, 115 | cncfmpt2f 24281 |
. . . . . . 7
β’ (π β (π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯))) β ((π΄[,]π΅)βcnββ)) |
117 | 58 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
β) |
118 | | iccssre 13347 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
119 | 1, 3, 118 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π΄[,]π΅) β β) |
120 | | fvexd 6858 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π‘ β (π΄(,)π₯)) β ((β D πΉ)βπ‘) β V) |
121 | 3 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β β) |
122 | 121 | rexrd 11206 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β
β*) |
123 | | elicc2 13330 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ π΅ β β) β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
124 | 1, 3, 123 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
125 | 124 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅)) |
126 | 125 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β€ π΅) |
127 | | iooss2 13301 |
. . . . . . . . . . . . . 14
β’ ((π΅ β β*
β§ π₯ β€ π΅) β (π΄(,)π₯) β (π΄(,)π΅)) |
128 | 122, 126,
127 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π΄(,)π₯) β (π΄(,)π΅)) |
129 | | ioombl 24932 |
. . . . . . . . . . . . . 14
β’ (π΄(,)π₯) β dom vol |
130 | 129 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π΄(,)π₯) β dom vol) |
131 | | fvexd 6858 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π‘ β (π΄(,)π΅)) β ((β D πΉ)βπ‘) β V) |
132 | 55 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π‘ β (π΄(,)π΅) β¦ ((β D πΉ)βπ‘)) β
πΏ1) |
133 | 128, 130,
131, 132 | iblss 25172 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π‘ β (π΄(,)π₯) β¦ ((β D πΉ)βπ‘)) β
πΏ1) |
134 | 120, 133 | itgcl 25151 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄[,]π΅)) β β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β β) |
135 | 113 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) |
136 | 134, 135 | subcld 11513 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)) β β) |
137 | 11 | tgioo2 24169 |
. . . . . . . . . 10
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
138 | | iccntr 24187 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β) β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
139 | 1, 3, 138 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
140 | 117, 119,
136, 137, 11, 139 | dvmptntr 25338 |
. . . . . . . . 9
β’ (π β (β D (π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))) = (β D (π₯ β (π΄(,)π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯))))) |
141 | | reelprrecn 11144 |
. . . . . . . . . . 11
β’ β
β {β, β} |
142 | 141 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β {β,
β}) |
143 | | ioossicc 13351 |
. . . . . . . . . . . 12
β’ (π΄(,)π΅) β (π΄[,]π΅) |
144 | 143 | sseli 3941 |
. . . . . . . . . . 11
β’ (π₯ β (π΄(,)π΅) β π₯ β (π΄[,]π΅)) |
145 | 144, 134 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β β) |
146 | 21 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D πΉ)βπ₯) β β) |
147 | 14, 1, 3, 5, 19, 18 | ftc1cnnc 36153 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘)) = (β D πΉ)) |
148 | 117, 119,
134, 137, 11, 139 | dvmptntr 25338 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘)) = (β D (π₯ β (π΄(,)π΅) β¦ β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘))) |
149 | 21 | feqmptd 6911 |
. . . . . . . . . . 11
β’ (π β (β D πΉ) = (π₯ β (π΄(,)π΅) β¦ ((β D πΉ)βπ₯))) |
150 | 147, 148,
149 | 3eqtr3d 2785 |
. . . . . . . . . 10
β’ (π β (β D (π₯ β (π΄(,)π΅) β¦ β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘)) = (π₯ β (π΄(,)π΅) β¦ ((β D πΉ)βπ₯))) |
151 | 144, 135 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) β β) |
152 | 114 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π β (β D πΉ) = (β D (π₯ β (π΄[,]π΅) β¦ (πΉβπ₯)))) |
153 | 117, 119,
135, 137, 11, 139 | dvmptntr 25338 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π΄[,]π΅) β¦ (πΉβπ₯))) = (β D (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)))) |
154 | 152, 149,
153 | 3eqtr3rd 2786 |
. . . . . . . . . 10
β’ (π β (β D (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯))) = (π₯ β (π΄(,)π΅) β¦ ((β D πΉ)βπ₯))) |
155 | 142, 145,
146, 150, 151, 146, 154 | dvmptsub 25334 |
. . . . . . . . 9
β’ (π β (β D (π₯ β (π΄(,)π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))) = (π₯ β (π΄(,)π΅) β¦ (((β D πΉ)βπ₯) β ((β D πΉ)βπ₯)))) |
156 | 146 | subidd 11501 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β (((β D πΉ)βπ₯) β ((β D πΉ)βπ₯)) = 0) |
157 | 156 | mpteq2dva 5206 |
. . . . . . . . 9
β’ (π β (π₯ β (π΄(,)π΅) β¦ (((β D πΉ)βπ₯) β ((β D πΉ)βπ₯))) = (π₯ β (π΄(,)π΅) β¦ 0)) |
158 | 140, 155,
157 | 3eqtrd 2781 |
. . . . . . . 8
β’ (π β (β D (π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))) = (π₯ β (π΄(,)π΅) β¦ 0)) |
159 | | fconstmpt 5695 |
. . . . . . . 8
β’ ((π΄(,)π΅) Γ {0}) = (π₯ β (π΄(,)π΅) β¦ 0) |
160 | 158, 159 | eqtr4di 2795 |
. . . . . . 7
β’ (π β (β D (π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))) = ((π΄(,)π΅) Γ {0})) |
161 | 1, 3, 116, 160 | dveq0 25367 |
. . . . . 6
β’ (π β (π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯))) = ((π΄[,]π΅) Γ {((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄)})) |
162 | 161 | fveq1d 6845 |
. . . . 5
β’ (π β ((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΅) = (((π΄[,]π΅) Γ {((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄)})βπ΅)) |
163 | | oveq2 7366 |
. . . . . . . . 9
β’ (π₯ = π΅ β (π΄(,)π₯) = (π΄(,)π΅)) |
164 | | itgeq1 25140 |
. . . . . . . . 9
β’ ((π΄(,)π₯) = (π΄(,)π΅) β β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ = β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘) |
165 | 163, 164 | syl 17 |
. . . . . . . 8
β’ (π₯ = π΅ β β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ = β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘) |
166 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = π΅ β (πΉβπ₯) = (πΉβπ΅)) |
167 | 165, 166 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = π΅ β (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)) = (β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β (πΉβπ΅))) |
168 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯))) = (π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯))) |
169 | | ovex 7391 |
. . . . . . 7
β’
(β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β (πΉβπ΅)) β V |
170 | 167, 168,
169 | fvmpt 6949 |
. . . . . 6
β’ (π΅ β (π΄[,]π΅) β ((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΅) = (β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β (πΉβπ΅))) |
171 | 7, 170 | syl 17 |
. . . . 5
β’ (π β ((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΅) = (β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β (πΉβπ΅))) |
172 | 162, 171 | eqtr3d 2779 |
. . . 4
β’ (π β (((π΄[,]π΅) Γ {((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄)})βπ΅) = (β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β (πΉβπ΅))) |
173 | | lbicc2 13382 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
174 | 2, 4, 5, 173 | syl3anc 1372 |
. . . . 5
β’ (π β π΄ β (π΄[,]π΅)) |
175 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π₯ = π΄ β (π΄(,)π₯) = (π΄(,)π΄)) |
176 | | iooid 13293 |
. . . . . . . . . . 11
β’ (π΄(,)π΄) = β
|
177 | 175, 176 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π₯ = π΄ β (π΄(,)π₯) = β
) |
178 | | itgeq1 25140 |
. . . . . . . . . 10
β’ ((π΄(,)π₯) = β
β β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ = β«β
((β D πΉ)βπ‘) dπ‘) |
179 | 177, 178 | syl 17 |
. . . . . . . . 9
β’ (π₯ = π΄ β β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ = β«β
((β D πΉ)βπ‘) dπ‘) |
180 | | itg0 25147 |
. . . . . . . . 9
β’
β«β
((β D πΉ)βπ‘) dπ‘ = 0 |
181 | 179, 180 | eqtrdi 2793 |
. . . . . . . 8
β’ (π₯ = π΄ β β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ = 0) |
182 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = π΄ β (πΉβπ₯) = (πΉβπ΄)) |
183 | 181, 182 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = π΄ β (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)) = (0 β (πΉβπ΄))) |
184 | | df-neg 11389 |
. . . . . . 7
β’ -(πΉβπ΄) = (0 β (πΉβπ΄)) |
185 | 183, 184 | eqtr4di 2795 |
. . . . . 6
β’ (π₯ = π΄ β (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)) = -(πΉβπ΄)) |
186 | | negex 11400 |
. . . . . 6
β’ -(πΉβπ΄) β V |
187 | 185, 168,
186 | fvmpt 6949 |
. . . . 5
β’ (π΄ β (π΄[,]π΅) β ((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄) = -(πΉβπ΄)) |
188 | 174, 187 | syl 17 |
. . . 4
β’ (π β ((π₯ β (π΄[,]π΅) β¦ (β«(π΄(,)π₯)((β D πΉ)βπ‘) dπ‘ β (πΉβπ₯)))βπ΄) = -(πΉβπ΄)) |
189 | 10, 172, 188 | 3eqtr3d 2785 |
. . 3
β’ (π β (β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β (πΉβπ΅)) = -(πΉβπ΄)) |
190 | 189 | oveq2d 7374 |
. 2
β’ (π β ((πΉβπ΅) + (β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β (πΉβπ΅))) = ((πΉβπ΅) + -(πΉβπ΄))) |
191 | 113, 7 | ffvelcdmd 7037 |
. . 3
β’ (π β (πΉβπ΅) β β) |
192 | | fvexd 6858 |
. . . 4
β’ ((π β§ π‘ β (π΄(,)π΅)) β ((β D πΉ)βπ‘) β V) |
193 | 192, 55 | itgcl 25151 |
. . 3
β’ (π β β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β β) |
194 | 191, 193 | pncan3d 11516 |
. 2
β’ (π β ((πΉβπ΅) + (β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ β (πΉβπ΅))) = β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘) |
195 | 113, 174 | ffvelcdmd 7037 |
. . 3
β’ (π β (πΉβπ΄) β β) |
196 | 191, 195 | negsubd 11519 |
. 2
β’ (π β ((πΉβπ΅) + -(πΉβπ΄)) = ((πΉβπ΅) β (πΉβπ΄))) |
197 | 190, 194,
196 | 3eqtr3d 2785 |
1
β’ (π β β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) |