This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem i1fres

Description: The "restriction" of a simple function to a measurable subset is simple. (It's not actually a restriction because it is zero instead of undefined outside A .) (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Hypothesis i1fres.1 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
Assertion i1fres ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → 𝐺 ∈ dom ∫1 )

Proof

Step Hyp Ref Expression
1 i1fres.1 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
2 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
3 2 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → 𝐹 : ℝ ⟶ ℝ )
4 3 ffnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → 𝐹 Fn ℝ )
5 fnfvelrn ⊢ ( ( 𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
6 4 5 sylan ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
7 i1f0rn ⊢ ( 𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹 )
8 7 ad2antrr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ran 𝐹 )
9 6 8 ifcld ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ran 𝐹 )
10 9 1 fmptd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → 𝐺 : ℝ ⟶ ran 𝐹 )
11 3 frnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → ran 𝐹 ⊆ ℝ )
12 10 11 fssd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → 𝐺 : ℝ ⟶ ℝ )
13 i1frn ⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
14 13 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → ran 𝐹 ∈ Fin )
15 10 frnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → ran 𝐺 ⊆ ran 𝐹 )
16 14 15 ssfid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → ran 𝐺 ∈ Fin )
17 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
18 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
19 17 18 ifbieq1d ⊢ ( 𝑥 = 𝑧 → if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) )
20 fvex ⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
21 c0ex ⊢ 0 ∈ V
22 20 21 ifex ⊢ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) ∈ V
23 19 1 22 fvmpt ⊢ ( 𝑧 ∈ ℝ → ( 𝐺 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) )
24 23 adantl ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) )
25 24 eqeq1d ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑧 ) = 𝑦 ↔ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ) )
26 eldifsni ⊢ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) → 𝑦 ≠ 0 )
27 26 ad2antlr ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → 𝑦 ≠ 0 )
28 27 necomd ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → 0 ≠ 𝑦 )
29 iffalse ⊢ ( ¬ 𝑧 ∈ 𝐴 → if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 0 )
30 29 neeq1d ⊢ ( ¬ 𝑧 ∈ 𝐴 → ( if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) ≠ 𝑦 ↔ 0 ≠ 𝑦 ) )
31 28 30 syl5ibrcom ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ¬ 𝑧 ∈ 𝐴 → if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) ≠ 𝑦 ) )
32 31 necon4bd ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 → 𝑧 ∈ 𝐴 ) )
33 32 pm4.71rd ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ↔ ( 𝑧 ∈ 𝐴 ∧ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ) ) )
34 25 33 bitrd ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑧 ) = 𝑦 ↔ ( 𝑧 ∈ 𝐴 ∧ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ) ) )
35 iftrue ⊢ ( 𝑧 ∈ 𝐴 → if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = ( 𝐹 ‘ 𝑧 ) )
36 35 eqeq1d ⊢ ( 𝑧 ∈ 𝐴 → ( if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
37 36 pm5.32i ⊢ ( ( 𝑧 ∈ 𝐴 ∧ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
38 34 37 bitrdi ⊢ ( ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑧 ) = 𝑦 ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
39 38 pm5.32da ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ) )
40 an12 ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
41 39 40 bitrdi ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ) )
42 10 ffnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → 𝐺 Fn ℝ )
43 42 adantr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝐺 Fn ℝ )
44 fniniseg ⊢ ( 𝐺 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
45 43 44 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
46 4 adantr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝐹 Fn ℝ )
47 fniniseg ⊢ ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
48 46 47 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
49 48 anbi2d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ) )
50 41 45 49 3bitr4d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) )
51 elin ⊢ ( 𝑧 ∈ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) )
52 50 51 bitr4di ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ↔ 𝑧 ∈ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) )
53 52 eqrdv ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑦 } ) = ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) )
54 simplr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝐴 ∈ dom vol )
55 i1fima ⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
56 55 ad2antrr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
57 inmbl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ) → ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ dom vol )
58 54 56 57 syl2anc ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ dom vol )
59 53 58 eqeltrd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑦 } ) ∈ dom vol )
60 53 fveq2d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑦 } ) ) = ( vol ‘ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) )
61 mblvol ⊢ ( ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) )
62 58 61 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) )
63 60 62 eqtrd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑦 } ) ) = ( vol* ‘ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) )
64 inss2 ⊢ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑦 } )
65 mblss ⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ )
66 56 65 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ )
67 mblvol ⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) )
68 56 67 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) )
69 i1fima2sn ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
70 69 adantlr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
71 68 70 eqeltrrd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol* ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
72 ovolsscl ⊢ ( ( ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑦 } ) ∧ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∈ ℝ )
73 64 66 71 72 mp3an2i ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol* ‘ ( 𝐴 ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∈ ℝ )
74 63 73 eqeltrd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑦 } ) ) ∈ ℝ )
75 12 16 59 74 i1fd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol ) → 𝐺 ∈ dom ∫1 )