Metamath Proof Explorer

Theorem itgcn

Description: Transfer itg2cn to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses itgcn.1 
|- ( ( ph /\ x e. A ) -> B e. V )
itgcn.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgcn.3 
|- ( ph -> C e. RR+ )
Assertion itgcn 
|- ( ph -> E. d e. RR+ A. u e. dom vol ( ( u C_ A /\ ( vol ` u ) < d ) -> S. u ( abs ` B ) _d x < C ) )

Proof

Step Hyp Ref Expression
1 itgcn.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 itgcn.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 itgcn.3 
 |-  ( ph -> C e. RR+ )
4 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
5 2 4 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
6 5 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
7 6 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
8 6 absge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( abs ` B ) )
9 elrege0 
 |-  ( ( abs ` B ) e. ( 0 [,) +oo ) <-> ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) )
10 7 8 9 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. ( 0 [,) +oo ) )
11 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
12 11 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
13 10 12 ifclda 
 |-  ( ph -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,) +oo ) )
14 13 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,) +oo ) )
15 14 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
16 5 1 mbfdm2 
 |-  ( ph -> A e. dom vol )
17 mblss 
 |-  ( A e. dom vol -> A C_ RR )
18 16 17 syl 
 |-  ( ph -> A C_ RR )
19 rembl 
 |-  RR e. dom vol
20 19 a1i 
 |-  ( ph -> RR e. dom vol )
21 13 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,) +oo ) )
22 eldifn 
 |-  ( x e. ( RR \ A ) -> -. x e. A )
23 22 adantl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> -. x e. A )
24 23 iffalsed 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( x e. A , ( abs ` B ) , 0 ) = 0 )
25 iftrue 
 |-  ( x e. A -> if ( x e. A , ( abs ` B ) , 0 ) = ( abs ` B ) )
26 25 mpteq2ia 
 |-  ( x e. A |-> if ( x e. A , ( abs ` B ) , 0 ) ) = ( x e. A |-> ( abs ` B ) )
27 1 2 iblabs 
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )
28 7 8 iblpos 
 |-  ( ph -> ( ( x e. A |-> ( abs ` B ) ) e. L^1 <-> ( ( x e. A |-> ( abs ` B ) ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) e. RR ) ) )
29 27 28 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( abs ` B ) ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) e. RR ) )
30 29 simpld 
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) e. MblFn )
31 26 30 eqeltrid 
 |-  ( ph -> ( x e. A |-> if ( x e. A , ( abs ` B ) , 0 ) ) e. MblFn )
32 18 20 21 24 31 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) e. MblFn )
33 29 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) e. RR )
34 15 32 33 3 itg2cn 
 |-  ( ph -> E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C ) )
35 simprr 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> u C_ A )
36 35 sselda 
 |-  ( ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) /\ x e. u ) -> x e. A )
37 6 adantlr 
 |-  ( ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) /\ x e. A ) -> B e. CC )
38 36 37 syldan 
 |-  ( ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) /\ x e. u ) -> B e. CC )
39 38 abscld 
 |-  ( ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) /\ x e. u ) -> ( abs ` B ) e. RR )
40 simprl 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> u e. dom vol )
41 37 abscld 
 |-  ( ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) /\ x e. A ) -> ( abs ` B ) e. RR )
42 27 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( x e. A |-> ( abs ` B ) ) e. L^1 )
43 35 40 41 42 iblss 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( x e. u |-> ( abs ` B ) ) e. L^1 )
44 38 absge0d 
 |-  ( ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) /\ x e. u ) -> 0 <_ ( abs ` B ) )
45 39 43 44 itgposval 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> S. u ( abs ` B ) _d x = ( S.2 ` ( x e. RR |-> if ( x e. u , ( abs ` B ) , 0 ) ) ) )
46 35 sseld 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( x e. u -> x e. A ) )
47 46 pm4.71d 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( x e. u <-> ( x e. u /\ x e. A ) ) )
48 47 ifbid 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> if ( x e. u , ( abs ` B ) , 0 ) = if ( ( x e. u /\ x e. A ) , ( abs ` B ) , 0 ) )
49 ifan 
 |-  if ( ( x e. u /\ x e. A ) , ( abs ` B ) , 0 ) = if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 )
50 48 49 eqtrdi 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> if ( x e. u , ( abs ` B ) , 0 ) = if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 ) )
51 50 mpteq2dv 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( x e. RR |-> if ( x e. u , ( abs ` B ) , 0 ) ) = ( x e. RR |-> if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 ) ) )
52 51 fveq2d 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( abs ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 ) ) ) )
53 45 52 eqtrd 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> S. u ( abs ` B ) _d x = ( S.2 ` ( x e. RR |-> if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 ) ) ) )
54 nfv 
 |-  F/ x y e. u
55 nffvmpt1 
 |-  F/_ x ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y )
56 nfcv 
 |-  F/_ x 0
57 54 55 56 nfif 
 |-  F/_ x if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 )
58 nfcv 
 |-  F/_ y if ( x e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` x ) , 0 )
59 elequ1 
 |-  ( y = x -> ( y e. u <-> x e. u ) )
60 fveq2 
 |-  ( y = x -> ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` x ) )
61 59 60 ifbieq1d 
 |-  ( y = x -> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) = if ( x e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` x ) , 0 ) )
62 57 58 61 cbvmpt 
 |-  ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) = ( x e. RR |-> if ( x e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` x ) , 0 ) )
63 fvex 
 |-  ( abs ` B ) e. _V
64 c0ex 
 |-  0 e. _V
65 63 64 ifex 
 |-  if ( x e. A , ( abs ` B ) , 0 ) e. _V
66 eqid 
 |-  ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) )
67 66 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. A , ( abs ` B ) , 0 ) e. _V ) -> ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` x ) = if ( x e. A , ( abs ` B ) , 0 ) )
68 65 67 mpan2 
 |-  ( x e. RR -> ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` x ) = if ( x e. A , ( abs ` B ) , 0 ) )
69 68 ifeq1d 
 |-  ( x e. RR -> if ( x e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` x ) , 0 ) = if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 ) )
70 69 mpteq2ia 
 |-  ( x e. RR |-> if ( x e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 ) )
71 62 70 eqtri 
 |-  ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) = ( x e. RR |-> if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 ) )
72 71 fveq2i 
 |-  ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. u , if ( x e. A , ( abs ` B ) , 0 ) , 0 ) ) )
73 53 72 eqtr4di 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> S. u ( abs ` B ) _d x = ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) )
74 73 breq1d 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( S. u ( abs ` B ) _d x < C <-> ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C ) )
75 74 biimprd 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C -> S. u ( abs ` B ) _d x < C ) )
76 75 imim2d 
 |-  ( ( ph /\ ( u e. dom vol /\ u C_ A ) ) -> ( ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C ) -> ( ( vol ` u ) < d -> S. u ( abs ` B ) _d x < C ) ) )
77 76 expr 
 |-  ( ( ph /\ u e. dom vol ) -> ( u C_ A -> ( ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C ) -> ( ( vol ` u ) < d -> S. u ( abs ` B ) _d x < C ) ) ) )
78 77 com23 
 |-  ( ( ph /\ u e. dom vol ) -> ( ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C ) -> ( u C_ A -> ( ( vol ` u ) < d -> S. u ( abs ` B ) _d x < C ) ) ) )
79 78 imp4a 
 |-  ( ( ph /\ u e. dom vol ) -> ( ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C ) -> ( ( u C_ A /\ ( vol ` u ) < d ) -> S. u ( abs ` B ) _d x < C ) ) )
80 79 ralimdva 
 |-  ( ph -> ( A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C ) -> A. u e. dom vol ( ( u C_ A /\ ( vol ` u ) < d ) -> S. u ( abs ` B ) _d x < C ) ) )
81 80 reximdv 
 |-  ( ph -> ( E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( y e. RR |-> if ( y e. u , ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ` y ) , 0 ) ) ) < C ) -> E. d e. RR+ A. u e. dom vol ( ( u C_ A /\ ( vol ` u ) < d ) -> S. u ( abs ` B ) _d x < C ) ) )
82 34 81 mpd 
 |-  ( ph -> E. d e. RR+ A. u e. dom vol ( ( u C_ A /\ ( vol ` u ) < d ) -> S. u ( abs ` B ) _d x < C ) )