Metamath Proof Explorer

Theorem iblabsnclem

Description: Lemma for iblabsnc ; cf. iblabslem . (Contributed by Brendan Leahy, 7-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 iblabsnc.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 iblabsnc.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 iblabsnclem.1 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
4 iblabsnclem.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ 𝐿1 )
5 iblabsnclem.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
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 5 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
15 14 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ )
16 0re ⊢ 0 ∈ ℝ
17 ifcl ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ∈ ℝ )
18 15 16 17 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ∈ ℝ )
19 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
21 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) = 0 )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) = 0 )
23 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) = ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
24 23 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
25 15 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) : 𝐴 ⟶ ℝ )
26 15 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ )
27 26 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 𝑦 < ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )
28 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
29 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
30 28 29 absled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ≤ 𝑦 ↔ ( - 𝑦 ≤ ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ≤ 𝑦 ) ) )
31 30 notbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ≤ 𝑦 ↔ ¬ ( - 𝑦 ≤ ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ≤ 𝑦 ) ) )
32 29 26 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ↔ ¬ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ≤ 𝑦 ) )
33 renegcl ⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
34 33 rexrd ⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ* )
35 34 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → - 𝑦 ∈ ℝ* )
36 elioomnf ⊢ ( - 𝑦 ∈ ℝ* → ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐵 ) < - 𝑦 ) ) )
37 35 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐵 ) < - 𝑦 ) ) )
38 28 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) < - 𝑦 ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐵 ) < - 𝑦 ) ) )
39 29 renegcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → - 𝑦 ∈ ℝ )
40 28 39 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) < - 𝑦 ↔ ¬ - 𝑦 ≤ ( 𝐹 ‘ 𝐵 ) ) )
41 37 38 40 3bitr2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ↔ ¬ - 𝑦 ≤ ( 𝐹 ‘ 𝐵 ) ) )
42 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
43 42 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
44 elioopnf ⊢ ( 𝑦 ∈ ℝ* → ( ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 𝑦 < ( 𝐹 ‘ 𝐵 ) ) ) )
45 43 44 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 𝑦 < ( 𝐹 ‘ 𝐵 ) ) ) )
46 28 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < ( 𝐹 ‘ 𝐵 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 𝑦 < ( 𝐹 ‘ 𝐵 ) ) ) )
47 29 28 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < ( 𝐹 ‘ 𝐵 ) ↔ ¬ ( 𝐹 ‘ 𝐵 ) ≤ 𝑦 ) )
48 45 46 47 3bitr2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ↔ ¬ ( 𝐹 ‘ 𝐵 ) ≤ 𝑦 ) )
49 41 48 orbi12d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ( ¬ - 𝑦 ≤ ( 𝐹 ‘ 𝐵 ) ∨ ¬ ( 𝐹 ‘ 𝐵 ) ≤ 𝑦 ) ) )
50 ianor ⊢ ( ¬ ( - 𝑦 ≤ ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ≤ 𝑦 ) ↔ ( ¬ - 𝑦 ≤ ( 𝐹 ‘ 𝐵 ) ∨ ¬ ( 𝐹 ‘ 𝐵 ) ≤ 𝑦 ) )
51 49 50 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ¬ ( - 𝑦 ≤ ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ≤ 𝑦 ) ) )
52 31 32 51 3bitr4rd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ 𝑦 < ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
53 elioopnf ⊢ ( 𝑦 ∈ ℝ* → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 𝑦 < ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )
54 43 53 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 𝑦 < ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )
55 27 52 54 3bitr4rd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
56 55 rabbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝑦 (,) +∞ ) } = { 𝑥 ∈ 𝐴 ∣ ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ) } )
57 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
58 57 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) “ ( 𝑦 (,) +∞ ) ) = { 𝑥 ∈ 𝐴 ∣ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝑦 (,) +∞ ) }
59 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) )
60 59 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) }
61 59 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) }
62 60 61 uneq12i ⊢ ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∪ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ) = ( { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) } ∪ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) } )
63 unrab ⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) } ∪ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) } ) = { 𝑥 ∈ 𝐴 ∣ ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ) }
64 62 63 eqtri ⊢ ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∪ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ) = { 𝑥 ∈ 𝐴 ∣ ( ( 𝐹 ‘ 𝐵 ) ∈ ( -∞ (,) - 𝑦 ) ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝑦 (,) +∞ ) ) }
65 56 58 64 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) “ ( 𝑦 (,) +∞ ) ) = ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∪ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ) )
66 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn )
67 4 66 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn )
68 5 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℝ )
69 mbfima ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∈ dom vol )
70 mbfima ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
71 unmbl ⊢ ( ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∈ dom vol ∧ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol ) → ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∪ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ) ∈ dom vol )
72 69 70 71 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℝ ) → ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∪ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ) ∈ dom vol )
73 67 68 72 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∪ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ) ∈ dom vol )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( -∞ (,) - 𝑦 ) ) ∪ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( 𝑦 (,) +∞ ) ) ) ∈ dom vol )
75 65 74 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
76 elioomnf ⊢ ( 𝑦 ∈ ℝ* → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) < 𝑦 ) ) )
77 43 76 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) < 𝑦 ) ) )
78 26 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) < 𝑦 ↔ ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) < 𝑦 ) ) )
79 28 29 absltd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) < 𝑦 ↔ ( - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) )
80 77 78 79 3bitr2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) )
81 28 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ ( - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) ) )
82 80 81 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ ( - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) ) )
83 3anass ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ ( - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) )
84 82 83 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) )
85 elioo2 ⊢ ( ( - 𝑦 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( - 𝑦 (,) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) )
86 34 42 85 syl2anc ⊢ ( 𝑦 ∈ ℝ → ( ( 𝐹 ‘ 𝐵 ) ∈ ( - 𝑦 (,) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) )
87 86 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( - 𝑦 (,) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ - 𝑦 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) < 𝑦 ) ) )
88 84 87 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( - 𝑦 (,) 𝑦 ) ) )
89 88 rabbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( -∞ (,) 𝑦 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝐵 ) ∈ ( - 𝑦 (,) 𝑦 ) } )
90 57 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) “ ( -∞ (,) 𝑦 ) ) = { 𝑥 ∈ 𝐴 ∣ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ( -∞ (,) 𝑦 ) }
91 59 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( - 𝑦 (,) 𝑦 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝐵 ) ∈ ( - 𝑦 (,) 𝑦 ) }
92 89 90 91 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) “ ( -∞ (,) 𝑦 ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( - 𝑦 (,) 𝑦 ) ) )
93 mbfima ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( - 𝑦 (,) 𝑦 ) ) ∈ dom vol )
94 67 68 93 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( - 𝑦 (,) 𝑦 ) ) ∈ dom vol )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) “ ( - 𝑦 (,) 𝑦 ) ) ∈ dom vol )
96 92 95 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
97 25 9 75 96 ismbf2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) ) ∈ MblFn )
98 24 97 eqeltrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) ∈ MblFn )
99 11 13 18 22 98 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) ∈ MblFn )
100 3 99 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
101 reex ⊢ ℝ ∈ V
102 101 a1i ⊢ ( 𝜑 → ℝ ∈ V )
103 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 )
104 ifcl ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ )
105 5 16 104 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ )
106 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
107 16 5 106 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
108 elrege0 ⊢ ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
109 105 107 108 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
110 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
111 110 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
112 109 111 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ∈ ( 0 [,) +∞ ) )
113 103 112 eqeltrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
114 113 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
115 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 )
116 5 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
117 ifcl ⊢ ( ( - ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ )
118 116 16 117 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ )
119 max1 ⊢ ( ( 0 ∈ ℝ ∧ - ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
120 16 116 119 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
121 elrege0 ⊢ ( if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
122 118 120 121 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
123 122 111 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ∈ ( 0 [,) +∞ ) )
124 115 123 eqeltrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
125 124 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
126 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
127 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
128 102 114 125 126 127 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) )
129 103 115 oveq12i ⊢ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) )
130 max0add ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ → ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
131 5 130 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
132 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
133 132 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
134 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
135 134 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) )
136 133 135 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = ( if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) )
137 23 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) = ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) )
138 131 136 137 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
139 138 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) )
140 00id ⊢ ( 0 + 0 ) = 0
141 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = 0 )
142 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) = 0 )
143 141 142 oveq12d ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = ( 0 + 0 ) )
144 140 143 21 3eqtr4a ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
145 139 144 pm2.61d1 ⊢ ( 𝜑 → ( if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) + if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - ( 𝐹 ‘ 𝐵 ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
146 129 145 syl5eq ⊢ ( 𝜑 → ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) )
147 146 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) )
148 128 147 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐹 ‘ 𝐵 ) ) , 0 ) ) )
149 3 148 eqtr4id ⊢ ( 𝜑 → 𝐺 = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) )
150 149 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) = ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) )
151 113 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
152 103 141 syl5eq ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) = 0 )
153 20 152 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) = 0 )
154 ibar ⊢ ( 𝑥 ∈ 𝐴 → ( 0 ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) ) )
155 154 ifbid ⊢ ( 𝑥 ∈ 𝐴 → if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
156 155 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) )
157 5 8 mbfpos ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
158 156 157 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
159 11 13 151 153 158 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
160 114 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
161 7 simp2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
162 125 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
163 7 simp3d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
164 159 160 161 162 163 itg2addnc ⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) )
165 150 164 eqtrd ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) )
166 161 163 readdcld ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) , ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( 𝐹 ‘ 𝐵 ) ) , - ( 𝐹 ‘ 𝐵 ) , 0 ) ) ) ) ∈ ℝ )
167 165 166 eqeltrd ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ )
168 100 167 jca ⊢ ( 𝜑 → ( 𝐺 ∈ MblFn ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ ) )