Metamath Proof Explorer

Theorem iblcnlem

Description: Expand out the universal quantifier in isibl2 . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses itgcnlem.r ⊢ R = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
itgcnlem.s ⊢ S = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
itgcnlem.t ⊢ T = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
itgcnlem.u ⊢ U = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
itgcnlem.v ⊢ φ ∧ x ∈ A → B ∈ V
Assertion iblcnlem ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ

Proof

Step Hyp Ref Expression
1 itgcnlem.r ⊢ R = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
2 itgcnlem.s ⊢ S = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
3 itgcnlem.t ⊢ T = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
4 itgcnlem.u ⊢ U = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
5 itgcnlem.v ⊢ φ ∧ x ∈ A → B ∈ V
6 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
7 6 a1i ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
8 simp1 ⊢ x ∈ A ⟼ B ∈ MblFn ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ → x ∈ A ⟼ B ∈ MblFn
9 8 a1i ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ → x ∈ A ⟼ B ∈ MblFn
10 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0
11 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0
12 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0
13 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0
14 0cn ⊢ 0 ∈ ℂ
15 14 elimel ⊢ if B ∈ ℂ B 0 ∈ ℂ
16 15 a1i ⊢ φ ∧ x ∈ A → if B ∈ ℂ B 0 ∈ ℂ
17 10 11 12 13 16 iblcnlem1 ⊢ φ → x ∈ A ⟼ if B ∈ ℂ B 0 ∈ 𝐿 1 ↔ x ∈ A ⟼ if B ∈ ℂ B 0 ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ
18 17 adantr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ if B ∈ ℂ B 0 ∈ 𝐿 1 ↔ x ∈ A ⟼ if B ∈ ℂ B 0 ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ
19 eqid ⊢ A = A
20 mbff ⊢ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℂ
21 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
22 21 5 dmmptd ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
23 22 feq2d ⊢ φ → x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℂ ↔ x ∈ A ⟼ B : A ⟶ ℂ
24 23 biimpa ⊢ φ ∧ x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℂ → x ∈ A ⟼ B : A ⟶ ℂ
25 20 24 sylan2 ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ B : A ⟶ ℂ
26 21 fmpt ⊢ ∀ x ∈ A B ∈ ℂ ↔ x ∈ A ⟼ B : A ⟶ ℂ
27 25 26 sylibr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∀ x ∈ A B ∈ ℂ
28 iftrue ⊢ B ∈ ℂ → if B ∈ ℂ B 0 = B
29 28 ralimi ⊢ ∀ x ∈ A B ∈ ℂ → ∀ x ∈ A if B ∈ ℂ B 0 = B
30 27 29 syl ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∀ x ∈ A if B ∈ ℂ B 0 = B
31 mpteq12 ⊢ A = A ∧ ∀ x ∈ A if B ∈ ℂ B 0 = B → x ∈ A ⟼ if B ∈ ℂ B 0 = x ∈ A ⟼ B
32 19 30 31 sylancr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ if B ∈ ℂ B 0 = x ∈ A ⟼ B
33 32 eleq1d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ if B ∈ ℂ B 0 ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ 𝐿 1
34 32 eleq1d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ if B ∈ ℂ B 0 ∈ MblFn ↔ x ∈ A ⟼ B ∈ MblFn
35 eqid ⊢ ℝ = ℝ
36 28 imim2i ⊢ x ∈ A → B ∈ ℂ → x ∈ A → if B ∈ ℂ B 0 = B
37 36 imp ⊢ x ∈ A → B ∈ ℂ ∧ x ∈ A → if B ∈ ℂ B 0 = B
38 37 fveq2d ⊢ x ∈ A → B ∈ ℂ ∧ x ∈ A → ℜ ⁡ if B ∈ ℂ B 0 = ℜ ⁡ B
39 38 ibllem ⊢ x ∈ A → B ∈ ℂ → if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
40 39 a1d ⊢ x ∈ A → B ∈ ℂ → x ∈ ℝ → if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
41 40 ralimi2 ⊢ ∀ x ∈ A B ∈ ℂ → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
42 27 41 syl ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
43 mpteq12 ⊢ ℝ = ℝ ∧ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
44 35 42 43 sylancr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
45 44 fveq2d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
46 45 1 eqtr4di ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 = R
47 46 eleq1d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ↔ R ∈ ℝ
48 38 negeqd ⊢ x ∈ A → B ∈ ℂ ∧ x ∈ A → − ℜ ⁡ if B ∈ ℂ B 0 = − ℜ ⁡ B
49 48 ibllem ⊢ x ∈ A → B ∈ ℂ → if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
50 49 a1d ⊢ x ∈ A → B ∈ ℂ → x ∈ ℝ → if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
51 50 ralimi2 ⊢ ∀ x ∈ A B ∈ ℂ → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
52 27 51 syl ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
53 mpteq12 ⊢ ℝ = ℝ ∧ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
54 35 52 53 sylancr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
55 54 fveq2d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
56 55 2 eqtr4di ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 = S
57 56 eleq1d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ↔ S ∈ ℝ
58 47 57 anbi12d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ↔ R ∈ ℝ ∧ S ∈ ℝ
59 37 fveq2d ⊢ x ∈ A → B ∈ ℂ ∧ x ∈ A → ℑ ⁡ if B ∈ ℂ B 0 = ℑ ⁡ B
60 59 ibllem ⊢ x ∈ A → B ∈ ℂ → if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
61 60 a1d ⊢ x ∈ A → B ∈ ℂ → x ∈ ℝ → if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
62 61 ralimi2 ⊢ ∀ x ∈ A B ∈ ℂ → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
63 27 62 syl ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
64 mpteq12 ⊢ ℝ = ℝ ∧ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
65 35 63 64 sylancr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
66 65 fveq2d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
67 66 3 eqtr4di ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 = T
68 67 eleq1d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ↔ T ∈ ℝ
69 59 negeqd ⊢ x ∈ A → B ∈ ℂ ∧ x ∈ A → − ℑ ⁡ if B ∈ ℂ B 0 = − ℑ ⁡ B
70 69 ibllem ⊢ x ∈ A → B ∈ ℂ → if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
71 70 a1d ⊢ x ∈ A → B ∈ ℂ → x ∈ ℝ → if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
72 71 ralimi2 ⊢ ∀ x ∈ A B ∈ ℂ → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
73 27 72 syl ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
74 mpteq12 ⊢ ℝ = ℝ ∧ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
75 35 73 74 sylancr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
76 75 fveq2d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
77 76 4 eqtr4di ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 = U
78 77 eleq1d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ↔ U ∈ ℝ
79 68 78 anbi12d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ↔ T ∈ ℝ ∧ U ∈ ℝ
80 34 58 79 3anbi123d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ if B ∈ ℂ B 0 ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ if B ∈ ℂ B 0 ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ if B ∈ ℂ B 0 − ℜ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ if B ∈ ℂ B 0 ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ if B ∈ ℂ B 0 − ℑ ⁡ if B ∈ ℂ B 0 0 ∈ ℝ ↔ x ∈ A ⟼ B ∈ MblFn ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ
81 18 33 80 3bitr3d ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ
82 81 ex ⊢ φ → x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ
83 7 9 82 pm5.21ndd ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ