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 ⊢ φ → G = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0
isibl.2 ⊢ φ ∧ x ∈ A → T = ℜ ⁡ B i k
isibl.3 ⊢ φ → dom ⁡ F = A
isibl.4 ⊢ φ ∧ x ∈ A → F ⁡ x = B
Assertion isibl ⊢ φ → F ∈ 𝐿 1 ↔ F ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ G ∈ ℝ

Proof

Step Hyp Ref Expression
1 isibl.1 ⊢ φ → G = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0
2 isibl.2 ⊢ φ ∧ x ∈ A → T = ℜ ⁡ B i k
3 isibl.3 ⊢ φ → dom ⁡ F = A
4 isibl.4 ⊢ φ ∧ x ∈ A → F ⁡ x = B
5 fvex ⊢ ℜ ⁡ f ⁡ x i k ∈ V
6 breq2 ⊢ y = ℜ ⁡ f ⁡ x i k → 0 ≤ y ↔ 0 ≤ ℜ ⁡ f ⁡ x i k
7 6 anbi2d ⊢ y = ℜ ⁡ f ⁡ x i k → x ∈ dom ⁡ f ∧ 0 ≤ y ↔ x ∈ dom ⁡ f ∧ 0 ≤ ℜ ⁡ f ⁡ x i k
8 id ⊢ y = ℜ ⁡ f ⁡ x i k → y = ℜ ⁡ f ⁡ x i k
9 7 8 ifbieq1d ⊢ y = ℜ ⁡ f ⁡ x i k → if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 = if x ∈ dom ⁡ f ∧ 0 ≤ ℜ ⁡ f ⁡ x i k ℜ ⁡ f ⁡ x i k 0
10 5 9 csbie ⊢ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 = if x ∈ dom ⁡ f ∧ 0 ≤ ℜ ⁡ f ⁡ x i k ℜ ⁡ f ⁡ x i k 0
11 dmeq ⊢ f = F → dom ⁡ f = dom ⁡ F
12 11 eleq2d ⊢ f = F → x ∈ dom ⁡ f ↔ x ∈ dom ⁡ F
13 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
14 13 fvoveq1d ⊢ f = F → ℜ ⁡ f ⁡ x i k = ℜ ⁡ F ⁡ x i k
15 14 breq2d ⊢ f = F → 0 ≤ ℜ ⁡ f ⁡ x i k ↔ 0 ≤ ℜ ⁡ F ⁡ x i k
16 12 15 anbi12d ⊢ f = F → x ∈ dom ⁡ f ∧ 0 ≤ ℜ ⁡ f ⁡ x i k ↔ x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k
17 16 14 ifbieq1d ⊢ f = F → if x ∈ dom ⁡ f ∧ 0 ≤ ℜ ⁡ f ⁡ x i k ℜ ⁡ f ⁡ x i k 0 = if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0
18 10 17 eqtrid ⊢ f = F → ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 = if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0
19 18 mpteq2dv ⊢ f = F → x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 = x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0
20 19 fveq2d ⊢ f = F → ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0
21 20 eleq1d ⊢ f = F → ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 ∈ ℝ ↔ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 ∈ ℝ
22 21 ralbidv ⊢ f = F → ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 ∈ ℝ ↔ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 ∈ ℝ
23 df-ibl ⊢ 𝐿 1 = f ∈ MblFn | ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 ∈ ℝ
24 22 23 elrab2 ⊢ F ∈ 𝐿 1 ↔ F ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 ∈ ℝ
25 3 eleq2d ⊢ φ → x ∈ dom ⁡ F ↔ x ∈ A
26 25 anbi1d ⊢ φ → x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ↔ x ∈ A ∧ 0 ≤ ℜ ⁡ F ⁡ x i k
27 26 ifbid ⊢ φ → if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 = if x ∈ A ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0
28 4 fvoveq1d ⊢ φ ∧ x ∈ A → ℜ ⁡ F ⁡ x i k = ℜ ⁡ B i k
29 28 2 eqtr4d ⊢ φ ∧ x ∈ A → ℜ ⁡ F ⁡ x i k = T
30 29 ibllem ⊢ φ → if x ∈ A ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 = if x ∈ A ∧ 0 ≤ T T 0
31 27 30 eqtrd ⊢ φ → if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 = if x ∈ A ∧ 0 ≤ T T 0
32 31 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0
33 32 1 eqtr4d ⊢ φ → x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 = G
34 33 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 = ∫ 2 ⁡ G
35 34 eleq1d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 ∈ ℝ ↔ ∫ 2 ⁡ G ∈ ℝ
36 35 ralbidv ⊢ φ → ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 ∈ ℝ ↔ ∀ k ∈ 0 … 3 ∫ 2 ⁡ G ∈ ℝ
37 36 anbi2d ⊢ φ → F ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ dom ⁡ F ∧ 0 ≤ ℜ ⁡ F ⁡ x i k ℜ ⁡ F ⁡ x i k 0 ∈ ℝ ↔ F ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ G ∈ ℝ
38 24 37 bitrid ⊢ φ → F ∈ 𝐿 1 ↔ F ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ G ∈ ℝ