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 ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( vol ‘ ( 𝐹𝐴 ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 i1fima ( 𝐹 ∈ dom ∫1 → ( 𝐹𝐴 ) ∈ dom vol )
2 1 adantr ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐹𝐴 ) ∈ dom vol )
3 mblvol ( ( 𝐹𝐴 ) ∈ dom vol → ( vol ‘ ( 𝐹𝐴 ) ) = ( vol* ‘ ( 𝐹𝐴 ) ) )
4 2 3 syl ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( vol ‘ ( 𝐹𝐴 ) ) = ( vol* ‘ ( 𝐹𝐴 ) ) )
5 i1ff ( 𝐹 ∈ dom ∫1𝐹 : ℝ ⟶ ℝ )
6 5 adantr ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → 𝐹 : ℝ ⟶ ℝ )
7 ffun ( 𝐹 : ℝ ⟶ ℝ → Fun 𝐹 )
8 inpreima ( Fun 𝐹 → ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) )
9 6 7 8 3syl ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) )
10 cnvimass ( 𝐹𝐴 ) ⊆ dom 𝐹
11 cnvimarndm ( 𝐹 “ ran 𝐹 ) = dom 𝐹
12 10 11 sseqtrri ( 𝐹𝐴 ) ⊆ ( 𝐹 “ ran 𝐹 )
13 df-ss ( ( 𝐹𝐴 ) ⊆ ( 𝐹 “ ran 𝐹 ) ↔ ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) = ( 𝐹𝐴 ) )
14 12 13 mpbi ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) = ( 𝐹𝐴 )
15 9 14 eqtr2di ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐹𝐴 ) = ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )
16 elinel1 ( 0 ∈ ( 𝐴 ∩ ran 𝐹 ) → 0 ∈ 𝐴 )
17 16 con3i ( ¬ 0 ∈ 𝐴 → ¬ 0 ∈ ( 𝐴 ∩ ran 𝐹 ) )
18 17 adantl ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ¬ 0 ∈ ( 𝐴 ∩ ran 𝐹 ) )
19 disjsn ( ( ( 𝐴 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ( 𝐴 ∩ ran 𝐹 ) )
20 18 19 sylibr ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( ( 𝐴 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ )
21 inss2 ( 𝐴 ∩ ran 𝐹 ) ⊆ ran 𝐹
22 5 frnd ( 𝐹 ∈ dom ∫1 → ran 𝐹 ⊆ ℝ )
23 21 22 sstrid ( 𝐹 ∈ dom ∫1 → ( 𝐴 ∩ ran 𝐹 ) ⊆ ℝ )
24 23 adantr ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐴 ∩ ran 𝐹 ) ⊆ ℝ )
25 reldisj ( ( 𝐴 ∩ ran 𝐹 ) ⊆ ℝ → ( ( ( 𝐴 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ( 𝐴 ∩ ran 𝐹 ) ⊆ ( ℝ ∖ { 0 } ) ) )
26 24 25 syl ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( ( ( 𝐴 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ( 𝐴 ∩ ran 𝐹 ) ⊆ ( ℝ ∖ { 0 } ) ) )
27 20 26 mpbid ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐴 ∩ ran 𝐹 ) ⊆ ( ℝ ∖ { 0 } ) )
28 imass2 ( ( 𝐴 ∩ ran 𝐹 ) ⊆ ( ℝ ∖ { 0 } ) → ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) ⊆ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) )
29 27 28 syl ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) ⊆ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) )
30 15 29 eqsstrd ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐹𝐴 ) ⊆ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) )
31 i1fima ( 𝐹 ∈ dom ∫1 → ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ∈ dom vol )
32 31 adantr ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ∈ dom vol )
33 mblss ( ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ∈ dom vol → ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ⊆ ℝ )
34 32 33 syl ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ⊆ ℝ )
35 mblvol ( ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ∈ dom vol → ( vol ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) = ( vol* ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) )
36 32 35 syl ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( vol ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) = ( vol* ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) )
37 isi1f ( 𝐹 ∈ dom ∫1 ↔ ( 𝐹 ∈ MblFn ∧ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )
38 37 simprbi ( 𝐹 ∈ dom ∫1 → ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
39 38 simp3d ( 𝐹 ∈ dom ∫1 → ( vol ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ )
40 39 adantr ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( vol ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ )
41 36 40 eqeltrrd ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( vol* ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ )
42 ovolsscl ( ( ( 𝐹𝐴 ) ⊆ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ∧ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐹𝐴 ) ) ∈ ℝ )
43 30 34 41 42 syl3anc ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( vol* ‘ ( 𝐹𝐴 ) ) ∈ ℝ )
44 4 43 eqeltrd ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴 ) → ( vol ‘ ( 𝐹𝐴 ) ) ∈ ℝ )