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∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
itgcnlem.s ⊢S=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
itgcnlem.t ⊢T=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
itgcnlem.u ⊢U=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
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∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
2 itgcnlem.s ⊢S=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
3 itgcnlem.t ⊢T=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
4 itgcnlem.u ⊢U=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
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∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00
11 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00
12 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00
13 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00
14 0cn ⊢0∈ℂ
15 14 elimel ⊢ifB∈ℂB0∈ℂ
16 15 a1i ⊢φ∧x∈A→ifB∈ℂB0∈ℂ
17 10 11 12 13 16 iblcnlem1 ⊢φ→x∈A⟼ifB∈ℂB0∈𝐿1↔x∈A⟼ifB∈ℂB0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00∈ℝ
18 17 adantr ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼ifB∈ℂB0∈𝐿1↔x∈A⟼ifB∈ℂB0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00∈ℝ
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∈AB∈ℂ↔x∈A⟼B:A⟶ℂ
27 25 26 sylibr ⊢φ∧x∈A⟼B∈MblFn→∀x∈AB∈ℂ
28 iftrue ⊢B∈ℂ→ifB∈ℂB0=B
29 28 ralimi ⊢∀x∈AB∈ℂ→∀x∈AifB∈ℂB0=B
30 27 29 syl ⊢φ∧x∈A⟼B∈MblFn→∀x∈AifB∈ℂB0=B
31 mpteq12 ⊢A=A∧∀x∈AifB∈ℂB0=B→x∈A⟼ifB∈ℂB0=x∈A⟼B
32 19 30 31 sylancr ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼ifB∈ℂB0=x∈A⟼B
33 32 eleq1d ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼ifB∈ℂB0∈𝐿1↔x∈A⟼B∈𝐿1
34 32 eleq1d ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼ifB∈ℂB0∈MblFn↔x∈A⟼B∈MblFn
35 eqid ⊢ℝ=ℝ
36 28 imim2i ⊢x∈A→B∈ℂ→x∈A→ifB∈ℂB0=B
37 36 imp ⊢x∈A→B∈ℂ∧x∈A→ifB∈ℂB0=B
38 37 fveq2d ⊢x∈A→B∈ℂ∧x∈A→ℜ⁡ifB∈ℂB0=ℜ⁡B
39 38 ibllem ⊢x∈A→B∈ℂ→ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=ifx∈A∧0≤ℜ⁡Bℜ⁡B0
40 39 a1d ⊢x∈A→B∈ℂ→x∈ℝ→ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=ifx∈A∧0≤ℜ⁡Bℜ⁡B0
41 40 ralimi2 ⊢∀x∈AB∈ℂ→∀x∈ℝifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=ifx∈A∧0≤ℜ⁡Bℜ⁡B0
42 27 41 syl ⊢φ∧x∈A⟼B∈MblFn→∀x∈ℝifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=ifx∈A∧0≤ℜ⁡Bℜ⁡B0
43 mpteq12 ⊢ℝ=ℝ∧∀x∈ℝifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=ifx∈A∧0≤ℜ⁡Bℜ⁡B0→x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
44 35 42 43 sylancr ⊢φ∧x∈A⟼B∈MblFn→x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
45 44 fveq2d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
46 45 1 eqtr4di ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00=R
47 46 eleq1d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00∈ℝ↔R∈ℝ
48 38 negeqd ⊢x∈A→B∈ℂ∧x∈A→−ℜ⁡ifB∈ℂB0=−ℜ⁡B
49 48 ibllem ⊢x∈A→B∈ℂ→ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
50 49 a1d ⊢x∈A→B∈ℂ→x∈ℝ→ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
51 50 ralimi2 ⊢∀x∈AB∈ℂ→∀x∈ℝifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
52 27 51 syl ⊢φ∧x∈A⟼B∈MblFn→∀x∈ℝifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
53 mpteq12 ⊢ℝ=ℝ∧∀x∈ℝifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0→x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
54 35 52 53 sylancr ⊢φ∧x∈A⟼B∈MblFn→x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
55 54 fveq2d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
56 55 2 eqtr4di ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00=S
57 56 eleq1d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00∈ℝ↔S∈ℝ
58 47 57 anbi12d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00∈ℝ↔R∈ℝ∧S∈ℝ
59 37 fveq2d ⊢x∈A→B∈ℂ∧x∈A→ℑ⁡ifB∈ℂB0=ℑ⁡B
60 59 ibllem ⊢x∈A→B∈ℂ→ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=ifx∈A∧0≤ℑ⁡Bℑ⁡B0
61 60 a1d ⊢x∈A→B∈ℂ→x∈ℝ→ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=ifx∈A∧0≤ℑ⁡Bℑ⁡B0
62 61 ralimi2 ⊢∀x∈AB∈ℂ→∀x∈ℝifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=ifx∈A∧0≤ℑ⁡Bℑ⁡B0
63 27 62 syl ⊢φ∧x∈A⟼B∈MblFn→∀x∈ℝifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=ifx∈A∧0≤ℑ⁡Bℑ⁡B0
64 mpteq12 ⊢ℝ=ℝ∧∀x∈ℝifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=ifx∈A∧0≤ℑ⁡Bℑ⁡B0→x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
65 35 63 64 sylancr ⊢φ∧x∈A⟼B∈MblFn→x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
66 65 fveq2d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
67 66 3 eqtr4di ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00=T
68 67 eleq1d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00∈ℝ↔T∈ℝ
69 59 negeqd ⊢x∈A→B∈ℂ∧x∈A→−ℑ⁡ifB∈ℂB0=−ℑ⁡B
70 69 ibllem ⊢x∈A→B∈ℂ→ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
71 70 a1d ⊢x∈A→B∈ℂ→x∈ℝ→ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
72 71 ralimi2 ⊢∀x∈AB∈ℂ→∀x∈ℝifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
73 27 72 syl ⊢φ∧x∈A⟼B∈MblFn→∀x∈ℝifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
74 mpteq12 ⊢ℝ=ℝ∧∀x∈ℝifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0→x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
75 35 73 74 sylancr ⊢φ∧x∈A⟼B∈MblFn→x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
76 75 fveq2d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
77 76 4 eqtr4di ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00=U
78 77 eleq1d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00∈ℝ↔U∈ℝ
79 68 78 anbi12d ⊢φ∧x∈A⟼B∈MblFn→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00∈ℝ↔T∈ℝ∧U∈ℝ
80 34 58 79 3anbi123d ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼ifB∈ℂB0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡ifB∈ℂB0ℜ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡ifB∈ℂB0−ℜ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡ifB∈ℂB0ℑ⁡ifB∈ℂB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡ifB∈ℂB0−ℑ⁡ifB∈ℂB00∈ℝ↔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∈ℝ