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 ‘ ( ◡ 𝐹 “ 𝐴 ) ) ∈ ℝ )