Metamath Proof Explorer

Theorem itg1ge0

Description: Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014)

Ref Expression
Assertion itg1ge0 
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> 0 <_ ( S.1 ` F ) )

Proof

Step Hyp Ref Expression
1 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
2 difss 
 |-  ( ran F \ { 0 } ) C_ ran F
3 ssfi 
 |-  ( ( ran F e. Fin /\ ( ran F \ { 0 } ) C_ ran F ) -> ( ran F \ { 0 } ) e. Fin )
4 1 2 3 sylancl 
 |-  ( F e. dom S.1 -> ( ran F \ { 0 } ) e. Fin )
5 4 adantr 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( ran F \ { 0 } ) e. Fin )
6 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
7 6 adantr 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> F : RR --> RR )
8 7 frnd 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ran F C_ RR )
9 8 ssdifssd 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( ran F \ { 0 } ) C_ RR )
10 9 sselda 
 |-  ( ( ( F e. dom S.1 /\ 0p oR <_ F ) /\ x e. ( ran F \ { 0 } ) ) -> x e. RR )
11 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ x e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )
12 11 adantlr 
 |-  ( ( ( F e. dom S.1 /\ 0p oR <_ F ) /\ x e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )
13 10 12 remulcld 
 |-  ( ( ( F e. dom S.1 /\ 0p oR <_ F ) /\ x e. ( ran F \ { 0 } ) ) -> ( x x. ( vol ` ( `' F " { x } ) ) ) e. RR )
14 eldifi 
 |-  ( x e. ( ran F \ { 0 } ) -> x e. ran F )
15 0cn 
 |-  0 e. CC
16 fnconstg 
 |-  ( 0 e. CC -> ( CC X. { 0 } ) Fn CC )
17 15 16 ax-mp 
 |-  ( CC X. { 0 } ) Fn CC
18 df-0p 
 |-  0p = ( CC X. { 0 } )
19 18 fneq1i 
 |-  ( 0p Fn CC <-> ( CC X. { 0 } ) Fn CC )
20 17 19 mpbir 
 |-  0p Fn CC
21 20 a1i 
 |-  ( F e. dom S.1 -> 0p Fn CC )
22 6 ffnd 
 |-  ( F e. dom S.1 -> F Fn RR )
23 cnex 
 |-  CC e. _V
24 23 a1i 
 |-  ( F e. dom S.1 -> CC e. _V )
25 reex 
 |-  RR e. _V
26 25 a1i 
 |-  ( F e. dom S.1 -> RR e. _V )
27 ax-resscn 
 |-  RR C_ CC
28 sseqin2 
 |-  ( RR C_ CC <-> ( CC i^i RR ) = RR )
29 27 28 mpbi 
 |-  ( CC i^i RR ) = RR
30 0pval 
 |-  ( y e. CC -> ( 0p ` y ) = 0 )
31 30 adantl 
 |-  ( ( F e. dom S.1 /\ y e. CC ) -> ( 0p ` y ) = 0 )
32 eqidd 
 |-  ( ( F e. dom S.1 /\ y e. RR ) -> ( F ` y ) = ( F ` y ) )
33 21 22 24 26 29 31 32 ofrfval 
 |-  ( F e. dom S.1 -> ( 0p oR <_ F <-> A. y e. RR 0 <_ ( F ` y ) ) )
34 33 biimpa 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> A. y e. RR 0 <_ ( F ` y ) )
35 22 adantr 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> F Fn RR )
36 breq2 
 |-  ( x = ( F ` y ) -> ( 0 <_ x <-> 0 <_ ( F ` y ) ) )
37 36 ralrn 
 |-  ( F Fn RR -> ( A. x e. ran F 0 <_ x <-> A. y e. RR 0 <_ ( F ` y ) ) )
38 35 37 syl 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( A. x e. ran F 0 <_ x <-> A. y e. RR 0 <_ ( F ` y ) ) )
39 34 38 mpbird 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> A. x e. ran F 0 <_ x )
40 39 r19.21bi 
 |-  ( ( ( F e. dom S.1 /\ 0p oR <_ F ) /\ x e. ran F ) -> 0 <_ x )
41 14 40 sylan2 
 |-  ( ( ( F e. dom S.1 /\ 0p oR <_ F ) /\ x e. ( ran F \ { 0 } ) ) -> 0 <_ x )
42 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " { x } ) e. dom vol )
43 42 ad2antrr 
 |-  ( ( ( F e. dom S.1 /\ 0p oR <_ F ) /\ x e. ( ran F \ { 0 } ) ) -> ( `' F " { x } ) e. dom vol )
44 mblss 
 |-  ( ( `' F " { x } ) e. dom vol -> ( `' F " { x } ) C_ RR )
45 ovolge0 
 |-  ( ( `' F " { x } ) C_ RR -> 0 <_ ( vol* ` ( `' F " { x } ) ) )
46 44 45 syl 
 |-  ( ( `' F " { x } ) e. dom vol -> 0 <_ ( vol* ` ( `' F " { x } ) ) )
47 mblvol 
 |-  ( ( `' F " { x } ) e. dom vol -> ( vol ` ( `' F " { x } ) ) = ( vol* ` ( `' F " { x } ) ) )
48 46 47 breqtrrd 
 |-  ( ( `' F " { x } ) e. dom vol -> 0 <_ ( vol ` ( `' F " { x } ) ) )
49 43 48 syl 
 |-  ( ( ( F e. dom S.1 /\ 0p oR <_ F ) /\ x e. ( ran F \ { 0 } ) ) -> 0 <_ ( vol ` ( `' F " { x } ) ) )
50 10 12 41 49 mulge0d 
 |-  ( ( ( F e. dom S.1 /\ 0p oR <_ F ) /\ x e. ( ran F \ { 0 } ) ) -> 0 <_ ( x x. ( vol ` ( `' F " { x } ) ) ) )
51 5 13 50 fsumge0 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> 0 <_ sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) )
52 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) )
53 52 adantr 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.1 ` F ) = sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) )
54 51 53 breqtrrd 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> 0 <_ ( S.1 ` F ) )