Metamath Proof Explorer

Theorem isibl2

Description: The predicate " F is integrable" when F is a mapping operation. (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 isibl.1 ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
2 isibl.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
3 isibl2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
5 nfcv ⊢ Ⅎ 𝑥 0
6 nfcv ⊢ Ⅎ 𝑥 ≤
7 nfcv ⊢ Ⅎ 𝑥 ℜ
8 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
9 nfcv ⊢ Ⅎ 𝑥 /
10 nfcv ⊢ Ⅎ 𝑥 ( i ↑ 𝑘 )
11 8 9 10 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) )
12 7 11 nffv ⊢ Ⅎ 𝑥 ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) )
13 5 6 12 nfbr ⊢ Ⅎ 𝑥 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) )
14 4 13 nfan ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) )
15 14 12 5 nfif ⊢ Ⅎ 𝑥 if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) , 0 )
16 nfcv ⊢ Ⅎ 𝑦 if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 )
17 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
18 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
19 18 fvoveq1d ⊢ ( 𝑦 = 𝑥 → ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) )
20 19 breq2d ⊢ ( 𝑦 = 𝑥 → ( 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) ↔ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) )
21 17 20 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) ) )
22 21 19 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
23 15 16 22 cbvmpt ⊢ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
25 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
26 25 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
27 24 3 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
28 27 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
29 28 2 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) = 𝑇 )
30 29 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) )
31 30 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
32 23 31 syl5eq ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
33 1 32 eqtr4d ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
34 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) / ( i ↑ 𝑘 ) ) ) )
35 25 3 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
36 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
37 33 34 35 36 isibl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ 𝐺 ) ∈ ℝ ) ) )