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 ⊢ 𝑅 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.s ⊢ 𝑆 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.t ⊢ 𝑇 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.u ⊢ 𝑈 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion iblcnlem ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) )

Proof

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