Metamath Proof Explorer

Theorem iblabslem

Description: Lemma for iblabs . (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses iblabs.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
iblabs.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
iblabs.3 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
iblabs.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ 𝐿1 )
iblabs.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
Assertion iblabslem ( 𝜑 → ( 𝐺 ∈ MblFn ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ ) )

Proof

Step Hyp Ref Expression
1 iblabs.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 iblabs.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 iblabs.3 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
4 iblabs.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ 𝐿1 )
5 iblabs.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
6 5 iblrelem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
7 4 6 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) )
8 7 simp1d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn )
9 8 5 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
10 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
11 9 10 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
12 rembl ⊢ ℝ ∈ dom vol
13 12 a1i ⊢ ( 𝜑 → ℝ ∈ dom vol )
14 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) = ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) = ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
16 5 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
17 16 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ )
18 15 17 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ∈ ℝ )
19 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
21 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) = 0 )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) = 0 )
23 14 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
24 absf ⊢ abs : ℂ ⟶ ℝ
25 24 a1i ⊢ ( 𝜑 → abs : ℂ ⟶ ℝ )
26 25 16 cofmpt ⊢ ( 𝜑 → ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
27 23 26 eqtr4id ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) = ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ) )
28 16 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
29 ax-resscn ⊢ ℝ ⊆ ℂ
30 ssid ⊢ ℂ ⊆ ℂ
31 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ ) )
32 29 30 31 mp2an ⊢ ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ )
33 abscncf ⊢ abs ∈ ( ℂ –cn→ ℝ )
34 32 33 sselii ⊢ abs ∈ ( ℂ –cn→ ℂ )
35 34 a1i ⊢ ( 𝜑 → abs ∈ ( ℂ –cn→ ℂ ) )
36 cncombf ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ ∧ abs ∈ ( ℂ –cn→ ℂ ) ) → ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ) ∈ MblFn )
37 8 28 35 36 syl3anc ⊢ ( 𝜑 → ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ) ∈ MblFn )
38 27 37 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) ∈ MblFn )
39 11 13 18 22 38 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) ∈ MblFn )
40 3 39 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
41 reex ⊢ ℝ ∈ V
42 41 a1i ⊢ ( 𝜑 → ℝ ∈ V )
43 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 )
44 0re ⊢ 0 ∈ ℝ
45 ifcl ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ )
46 5 44 45 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ )
47 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
48 44 5 47 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
49 elrege0 ⊢ ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
50 46 48 49 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
51 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
52 51 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
53 50 52 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ∈ ( 0 [,) +∞ ) )
54 43 53 eqeltrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
56 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 )
57 5 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
58 ifcl ⊢ ( ( - ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ )
59 57 44 58 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ )
60 max1 ⊢ ( ( 0 ∈ ℝ ∧ - ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
61 44 57 60 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
62 elrege0 ⊢ ( if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
63 59 61 62 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
64 63 52 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ∈ ( 0 [,) +∞ ) )
65 56 64 eqeltrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
67 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
68 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
69 42 55 66 67 68 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) )
70 43 56 oveq12i ⊢ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) )
71 max0add ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ → ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
72 5 71 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
73 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
75 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
76 75 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
77 74 76 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
78 72 77 15 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
79 78 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) )
80 00id ⊢ ( 0 + 0 ) = 0
81 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = 0 )
82 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = 0 )
83 81 82 oveq12d ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = ( 0 + 0 ) )
84 80 83 21 3eqtr4a ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
85 79 84 pm2.61d1 ⊢ ( 𝜑 → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
86 70 85 syl5eq ⊢ ( 𝜑 → ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
87 86 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) )
88 69 87 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) )
89 3 88 eqtr4id ⊢ ( 𝜑 → 𝐺 = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) )
90 89 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) = ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) )
91 54 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
92 43 81 syl5eq ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) = 0 )
93 20 92 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) = 0 )
94 ibar ⊢ ( 𝑥 ∈ 𝐴 → ( 0 ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) ) )
95 94 ifbid ⊢ ( 𝑥 ∈ 𝐴 → if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
96 95 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
97 5 8 mbfpos ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
98 96 97 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
99 11 13 91 93 98 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
100 55 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
101 7 simp2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
102 65 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
103 56 82 syl5eq ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) = 0 )
104 20 103 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) = 0 )
105 ibar ⊢ ( 𝑥 ∈ 𝐴 → ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) ) )
106 105 ifbid ⊢ ( 𝑥 ∈ 𝐴 → if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
107 106 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
108 5 8 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn )
109 57 108 mbfpos ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
110 107 109 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
111 11 13 102 104 110 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
112 66 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
113 7 simp3d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
114 99 100 101 111 112 113 itg2add ⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) )
115 90 114 eqtrd ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) )
116 101 113 readdcld ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) ∈ ℝ )
117 115 116 eqeltrd ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ )
118 40 117 jca ⊢ ( 𝜑 → ( 𝐺 ∈ MblFn ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ ) )