Metamath Proof Explorer

Theorem i1fima2

Description: Any preimage of a simple function not containing zero has finite measure. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion i1fima2 
|- ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( vol ` ( `' F " A ) ) e. RR )

Proof

Step Hyp Ref Expression
1 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " A ) e. dom vol )
2 1 adantr 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( `' F " A ) e. dom vol )
3 mblvol 
 |-  ( ( `' F " A ) e. dom vol -> ( vol ` ( `' F " A ) ) = ( vol* ` ( `' F " A ) ) )
4 2 3 syl 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( vol ` ( `' F " A ) ) = ( vol* ` ( `' F " A ) ) )
5 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
6 5 adantr 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> F : RR --> RR )
7 ffun 
 |-  ( F : RR --> RR -> Fun F )
8 inpreima 
 |-  ( Fun F -> ( `' F " ( A i^i ran F ) ) = ( ( `' F " A ) i^i ( `' F " ran F ) ) )
9 6 7 8 3syl 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( `' F " ( A i^i ran F ) ) = ( ( `' F " A ) i^i ( `' F " ran F ) ) )
10 cnvimass 
 |-  ( `' F " A ) C_ dom F
11 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
12 10 11 sseqtrri 
 |-  ( `' F " A ) C_ ( `' F " ran F )
13 df-ss 
 |-  ( ( `' F " A ) C_ ( `' F " ran F ) <-> ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( `' F " A ) )
14 12 13 mpbi 
 |-  ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( `' F " A )
15 9 14 eqtr2di 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )
16 elinel1 
 |-  ( 0 e. ( A i^i ran F ) -> 0 e. A )
17 16 con3i 
 |-  ( -. 0 e. A -> -. 0 e. ( A i^i ran F ) )
18 17 adantl 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> -. 0 e. ( A i^i ran F ) )
19 disjsn 
 |-  ( ( ( A i^i ran F ) i^i { 0 } ) = (/) <-> -. 0 e. ( A i^i ran F ) )
20 18 19 sylibr 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( ( A i^i ran F ) i^i { 0 } ) = (/) )
21 inss2 
 |-  ( A i^i ran F ) C_ ran F
22 5 frnd 
 |-  ( F e. dom S.1 -> ran F C_ RR )
23 21 22 sstrid 
 |-  ( F e. dom S.1 -> ( A i^i ran F ) C_ RR )
24 23 adantr 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( A i^i ran F ) C_ RR )
25 reldisj 
 |-  ( ( A i^i ran F ) C_ RR -> ( ( ( A i^i ran F ) i^i { 0 } ) = (/) <-> ( A i^i ran F ) C_ ( RR \ { 0 } ) ) )
26 24 25 syl 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( ( ( A i^i ran F ) i^i { 0 } ) = (/) <-> ( A i^i ran F ) C_ ( RR \ { 0 } ) ) )
27 20 26 mpbid 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( A i^i ran F ) C_ ( RR \ { 0 } ) )
28 imass2 
 |-  ( ( A i^i ran F ) C_ ( RR \ { 0 } ) -> ( `' F " ( A i^i ran F ) ) C_ ( `' F " ( RR \ { 0 } ) ) )
29 27 28 syl 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( `' F " ( A i^i ran F ) ) C_ ( `' F " ( RR \ { 0 } ) ) )
30 15 29 eqsstrd 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( `' F " A ) C_ ( `' F " ( RR \ { 0 } ) ) )
31 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " ( RR \ { 0 } ) ) e. dom vol )
32 31 adantr 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( `' F " ( RR \ { 0 } ) ) e. dom vol )
33 mblss 
 |-  ( ( `' F " ( RR \ { 0 } ) ) e. dom vol -> ( `' F " ( RR \ { 0 } ) ) C_ RR )
34 32 33 syl 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( `' F " ( RR \ { 0 } ) ) C_ RR )
35 mblvol 
 |-  ( ( `' F " ( RR \ { 0 } ) ) e. dom vol -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) = ( vol* ` ( `' F " ( RR \ { 0 } ) ) ) )
36 32 35 syl 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) = ( vol* ` ( `' F " ( RR \ { 0 } ) ) ) )
37 isi1f 
 |-  ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )
38 37 simprbi 
 |-  ( F e. dom S.1 -> ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) )
39 38 simp3d 
 |-  ( F e. dom S.1 -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR )
40 39 adantr 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR )
41 36 40 eqeltrrd 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( vol* ` ( `' F " ( RR \ { 0 } ) ) ) e. RR )
42 ovolsscl 
 |-  ( ( ( `' F " A ) C_ ( `' F " ( RR \ { 0 } ) ) /\ ( `' F " ( RR \ { 0 } ) ) C_ RR /\ ( vol* ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) -> ( vol* ` ( `' F " A ) ) e. RR )
43 30 34 41 42 syl3anc 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( vol* ` ( `' F " A ) ) e. RR )
44 4 43 eqeltrd 
 |-  ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( vol ` ( `' F " A ) ) e. RR )