Step |
Hyp |
Ref |
Expression |
1 |
|
itgioo.1 |
|- ( ph -> A e. RR ) |
2 |
|
itgioo.2 |
|- ( ph -> B e. RR ) |
3 |
|
itgioo.3 |
|- ( ( ph /\ x e. ( A [,] B ) ) -> C e. CC ) |
4 |
|
ioossicc |
|- ( A (,) B ) C_ ( A [,] B ) |
5 |
4
|
a1i |
|- ( ph -> ( A (,) B ) C_ ( A [,] B ) ) |
6 |
|
iccssre |
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR ) |
7 |
1 2 6
|
syl2anc |
|- ( ph -> ( A [,] B ) C_ RR ) |
8 |
1
|
rexrd |
|- ( ph -> A e. RR* ) |
9 |
2
|
rexrd |
|- ( ph -> B e. RR* ) |
10 |
|
icc0 |
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) ) |
11 |
8 9 10
|
syl2anc |
|- ( ph -> ( ( A [,] B ) = (/) <-> B < A ) ) |
12 |
11
|
biimpar |
|- ( ( ph /\ B < A ) -> ( A [,] B ) = (/) ) |
13 |
12
|
difeq1d |
|- ( ( ph /\ B < A ) -> ( ( A [,] B ) \ ( A (,) B ) ) = ( (/) \ ( A (,) B ) ) ) |
14 |
|
0dif |
|- ( (/) \ ( A (,) B ) ) = (/) |
15 |
|
0ss |
|- (/) C_ { A , B } |
16 |
14 15
|
eqsstri |
|- ( (/) \ ( A (,) B ) ) C_ { A , B } |
17 |
13 16
|
eqsstrdi |
|- ( ( ph /\ B < A ) -> ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } ) |
18 |
|
uncom |
|- ( { A , B } u. ( A (,) B ) ) = ( ( A (,) B ) u. { A , B } ) |
19 |
8
|
adantr |
|- ( ( ph /\ A <_ B ) -> A e. RR* ) |
20 |
9
|
adantr |
|- ( ( ph /\ A <_ B ) -> B e. RR* ) |
21 |
|
simpr |
|- ( ( ph /\ A <_ B ) -> A <_ B ) |
22 |
|
prunioo |
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) ) |
23 |
19 20 21 22
|
syl3anc |
|- ( ( ph /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) ) |
24 |
18 23
|
eqtr2id |
|- ( ( ph /\ A <_ B ) -> ( A [,] B ) = ( { A , B } u. ( A (,) B ) ) ) |
25 |
24
|
difeq1d |
|- ( ( ph /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = ( ( { A , B } u. ( A (,) B ) ) \ ( A (,) B ) ) ) |
26 |
|
difun2 |
|- ( ( { A , B } u. ( A (,) B ) ) \ ( A (,) B ) ) = ( { A , B } \ ( A (,) B ) ) |
27 |
25 26
|
eqtrdi |
|- ( ( ph /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = ( { A , B } \ ( A (,) B ) ) ) |
28 |
|
difss |
|- ( { A , B } \ ( A (,) B ) ) C_ { A , B } |
29 |
27 28
|
eqsstrdi |
|- ( ( ph /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } ) |
30 |
17 29 2 1
|
ltlecasei |
|- ( ph -> ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } ) |
31 |
1 2
|
prssd |
|- ( ph -> { A , B } C_ RR ) |
32 |
|
prfi |
|- { A , B } e. Fin |
33 |
|
ovolfi |
|- ( ( { A , B } e. Fin /\ { A , B } C_ RR ) -> ( vol* ` { A , B } ) = 0 ) |
34 |
32 31 33
|
sylancr |
|- ( ph -> ( vol* ` { A , B } ) = 0 ) |
35 |
|
ovolssnul |
|- ( ( ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } /\ { A , B } C_ RR /\ ( vol* ` { A , B } ) = 0 ) -> ( vol* ` ( ( A [,] B ) \ ( A (,) B ) ) ) = 0 ) |
36 |
30 31 34 35
|
syl3anc |
|- ( ph -> ( vol* ` ( ( A [,] B ) \ ( A (,) B ) ) ) = 0 ) |
37 |
5 7 36 3
|
itgss3 |
|- ( ph -> ( ( ( x e. ( A (,) B ) |-> C ) e. L^1 <-> ( x e. ( A [,] B ) |-> C ) e. L^1 ) /\ S. ( A (,) B ) C _d x = S. ( A [,] B ) C _d x ) ) |
38 |
37
|
simprd |
|- ( ph -> S. ( A (,) B ) C _d x = S. ( A [,] B ) C _d x ) |