Metamath Proof Explorer

Theorem itggt0

Description: The integral of a strictly positive function is positive. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Hypotheses itggt0.1 
|- ( ph -> 0 < ( vol ` A ) )
itggt0.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itggt0.3 
|- ( ( ph /\ x e. A ) -> B e. RR+ )
Assertion itggt0 
|- ( ph -> 0 < S. A B _d x )

Proof

Step Hyp Ref Expression
1 itggt0.1 
 |-  ( ph -> 0 < ( vol ` A ) )
2 itggt0.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 itggt0.3 
 |-  ( ( ph /\ x e. A ) -> B 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 3 mbfdm2 
 |-  ( ph -> A e. dom vol )
7 3 rpred 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
8 3 rpge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
9 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
10 7 8 9 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> 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 , B , 0 ) e. ( 0 [,) +oo ) )
14 13 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
15 14 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
16 mblss 
 |-  ( A e. dom vol -> A C_ RR )
17 6 16 syl 
 |-  ( ph -> A C_ RR )
18 rembl 
 |-  RR e. dom vol
19 18 a1i 
 |-  ( ph -> RR e. dom vol )
20 13 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
21 eldifn 
 |-  ( x e. ( RR \ A ) -> -. x e. A )
22 21 adantl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> -. x e. A )
23 22 iffalsed 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( x e. A , B , 0 ) = 0 )
24 iftrue 
 |-  ( x e. A -> if ( x e. A , B , 0 ) = B )
25 24 mpteq2ia 
 |-  ( x e. A |-> if ( x e. A , B , 0 ) ) = ( x e. A |-> B )
26 25 5 eqeltrid 
 |-  ( ph -> ( x e. A |-> if ( x e. A , B , 0 ) ) e. MblFn )
27 17 19 20 23 26 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) e. MblFn )
28 3 rpgt0d 
 |-  ( ( ph /\ x e. A ) -> 0 < B )
29 17 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
30 24 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , B , 0 ) = B )
31 30 3 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , B , 0 ) e. RR+ )
32 eqid 
 |-  ( x e. RR |-> if ( x e. A , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) )
33 32 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. A , B , 0 ) e. RR+ ) -> ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x ) = if ( x e. A , B , 0 ) )
34 29 31 33 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x ) = if ( x e. A , B , 0 ) )
35 34 30 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x ) = B )
36 28 35 breqtrrd 
 |-  ( ( ph /\ x e. A ) -> 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x ) )
37 36 ralrimiva 
 |-  ( ph -> A. x e. A 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x ) )
38 nfcv 
 |-  F/_ x 0
39 nfcv 
 |-  F/_ x <
40 nffvmpt1 
 |-  F/_ x ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` y )
41 38 39 40 nfbr 
 |-  F/ x 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` y )
42 nfv 
 |-  F/ y 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x )
43 fveq2 
 |-  ( y = x -> ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` y ) = ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x ) )
44 43 breq2d 
 |-  ( y = x -> ( 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` y ) <-> 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x ) ) )
45 41 42 44 cbvralw 
 |-  ( A. y e. A 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` y ) <-> A. x e. A 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` x ) )
46 37 45 sylibr 
 |-  ( ph -> A. y e. A 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` y ) )
47 46 r19.21bi 
 |-  ( ( ph /\ y e. A ) -> 0 < ( ( x e. RR |-> if ( x e. A , B , 0 ) ) ` y ) )
48 6 1 15 27 47 itg2gt0 
 |-  ( ph -> 0 < ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
49 7 2 8 itgposval 
 |-  ( ph -> S. A B _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
50 48 49 breqtrrd 
 |-  ( ph -> 0 < S. A B _d x )