Metamath Proof Explorer

Theorem isibl

Description: The predicate " F is integrable". The "integrable" predicate corresponds roughly to the range of validity of S. A Bd x , which is to say that the expression S. A B d x doesn't make sense unless ( x e. A |-> B ) e. L^1 . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses isibl.1 ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
isibl.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
isibl.3 ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
isibl.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
Assertion isibl ( 𝜑 → ( 𝐹 ∈ 𝐿1 ↔ ( 𝐹 ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ 𝐺 ) ∈ ℝ ) ) )

Proof

Step Hyp Ref Expression
1 isibl.1 ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
2 isibl.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
3 isibl.3 ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
4 isibl.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
5 fvex ⊢ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ∈ V
6 breq2 ⊢ ( 𝑦 = ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) → ( 0 ≤ 𝑦 ↔ 0 ≤ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) )
7 6 anbi2d ⊢ ( 𝑦 = ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) → ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) ↔ ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) ) )
8 id ⊢ ( 𝑦 = ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) → 𝑦 = ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) )
9 7 8 ifbieq1d ⊢ ( 𝑦 = ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) → if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
10 5 9 csbie ⊢ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 )
11 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
12 11 eleq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ dom 𝑓 ↔ 𝑥 ∈ dom 𝐹 ) )
13 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14 13 fvoveq1d ⊢ ( 𝑓 = 𝐹 → ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) )
15 14 breq2d ⊢ ( 𝑓 = 𝐹 → ( 0 ≤ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ↔ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) )
16 12 15 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) ) )
17 16 14 ifbieq1d ⊢ ( 𝑓 = 𝐹 → if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
18 10 17 syl5eq ⊢ ( 𝑓 = 𝐹 → ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
19 18 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
20 19 fveq2d ⊢ ( 𝑓 = 𝐹 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
21 20 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
22 21 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ ↔ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
23 df-ibl ⊢ 𝐿1 = { 𝑓 ∈ MblFn ∣ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ }
24 22 23 elrab2 ⊢ ( 𝐹 ∈ 𝐿1 ↔ ( 𝐹 ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
25 3 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
26 25 anbi1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) ) )
27 26 ifbid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
28 4 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
29 28 2 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) = 𝑇 )
30 29 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) )
31 27 30 eqtrd ⊢ ( 𝜑 → if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) )
32 31 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
33 32 1 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = 𝐺 )
34 33 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ 𝐺 ) )
35 34 eleq1d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∫2 ‘ 𝐺 ) ∈ ℝ ) )
36 35 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ 𝐺 ) ∈ ℝ ) )
37 36 anbi2d ⊢ ( 𝜑 → ( ( 𝐹 ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ dom 𝐹 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ↔ ( 𝐹 ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ 𝐺 ) ∈ ℝ ) ) )
38 24 37 syl5bb ⊢ ( 𝜑 → ( 𝐹 ∈ 𝐿1 ↔ ( 𝐹 ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ 𝐺 ) ∈ ℝ ) ) )