Metamath Proof Explorer

Theorem ftc1anclem1

Description: Lemma for ftc1anc - the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf , but this proof avoids ax-cc . (Contributed by Brendan Leahy, 18-Jun-2018)

Ref Expression
Assertion ftc1anclem1 ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → ( abs ∘ 𝐹 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
2 1 recnd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
3 id ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 : 𝐴 ⟶ ℝ )
4 3 feqmptd ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 = ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) )
5 absf ⊢ abs : ℂ ⟶ ℝ
6 5 a1i ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → abs : ℂ ⟶ ℝ )
7 6 feqmptd ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) ) )
8 fveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑡 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
9 2 4 7 8 fmptco ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( abs ∘ 𝐹 ) = ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
10 9 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → ( abs ∘ 𝐹 ) = ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
11 2 abscld ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
12 11 fmpttd ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) : 𝐴 ⟶ ℝ )
13 12 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) : 𝐴 ⟶ ℝ )
14 fdm ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → dom 𝐹 = 𝐴 )
15 14 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → dom 𝐹 = 𝐴 )
16 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
17 16 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → dom 𝐹 ∈ dom vol )
18 15 17 eqeltrrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → 𝐴 ∈ dom vol )
19 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
20 elioopnf ⊢ ( 𝑥 ∈ ℝ* → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
21 19 20 syl ⊢ ( 𝑥 ∈ ℝ → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
22 11 biantrurd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
23 22 bicomd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ↔ 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
24 21 23 sylan9bbr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
25 ltnle ⊢ ( ( 𝑥 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ) → ( 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ↔ ¬ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑥 ) )
26 25 ancoms ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ↔ ¬ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑥 ) )
27 11 26 sylan ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ↔ ¬ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑥 ) )
28 absle ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑥 ↔ ( - 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 𝑥 ) ) )
29 1 28 sylan ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑥 ↔ ( - 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 𝑥 ) ) )
30 renegcl ⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
31 lenlt ⊢ ( ( - 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) → ( - 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) < - 𝑥 ) )
32 30 1 31 syl2anr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( - 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) < - 𝑥 ) )
33 1 biantrurd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑡 ) < - 𝑥 ↔ ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑡 ) < - 𝑥 ) ) )
34 30 rexrd ⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ* )
35 elioomnf ⊢ ( - 𝑥 ∈ ℝ* → ( ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑡 ) < - 𝑥 ) ) )
36 34 35 syl ⊢ ( 𝑥 ∈ ℝ → ( ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑡 ) < - 𝑥 ) ) )
37 36 bicomd ⊢ ( 𝑥 ∈ ℝ → ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑡 ) < - 𝑥 ) ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ) )
38 33 37 sylan9bb ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑡 ) < - 𝑥 ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ) )
39 38 notbid ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ¬ ( 𝐹 ‘ 𝑡 ) < - 𝑥 ↔ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ) )
40 32 39 bitrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( - 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ) )
41 lenlt ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑡 ) ≤ 𝑥 ↔ ¬ 𝑥 < ( 𝐹 ‘ 𝑡 ) ) )
42 1 41 sylan ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑡 ) ≤ 𝑥 ↔ ¬ 𝑥 < ( 𝐹 ‘ 𝑡 ) ) )
43 1 biantrurd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( 𝑥 < ( 𝐹 ‘ 𝑡 ) ↔ ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ 𝑥 < ( 𝐹 ‘ 𝑡 ) ) ) )
44 elioopnf ⊢ ( 𝑥 ∈ ℝ* → ( ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ 𝑥 < ( 𝐹 ‘ 𝑡 ) ) ) )
45 19 44 syl ⊢ ( 𝑥 ∈ ℝ → ( ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ 𝑥 < ( 𝐹 ‘ 𝑡 ) ) ) )
46 45 bicomd ⊢ ( 𝑥 ∈ ℝ → ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ 𝑥 < ( 𝐹 ‘ 𝑡 ) ) ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) )
47 43 46 sylan9bb ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < ( 𝐹 ‘ 𝑡 ) ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) )
48 47 notbid ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 < ( 𝐹 ‘ 𝑡 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) )
49 42 48 bitrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑡 ) ≤ 𝑥 ↔ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) )
50 40 49 anbi12d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( - 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ 𝑥 ) ↔ ( ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) ) )
51 29 50 bitrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑥 ↔ ( ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) ) )
52 51 notbid ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ¬ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑥 ↔ ¬ ( ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) ) )
53 elun ⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ↔ ( ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ∨ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) )
54 oran ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ∨ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) ↔ ¬ ( ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) )
55 53 54 bitri ⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ↔ ¬ ( ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( -∞ (,) - 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑥 (,) +∞ ) ) )
56 52 55 bitr4di ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ¬ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) )
57 24 27 56 3bitrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) )
58 57 an32s ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑡 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) )
59 58 rabbidva ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → { 𝑡 ∈ 𝐴 ∣ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) } = { 𝑡 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑡 ) ∈ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) } )
60 eqid ⊢ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
61 60 mptpreima ⊢ ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = { 𝑡 ∈ 𝐴 ∣ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) }
62 eqid ⊢ ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) )
63 62 mptpreima ⊢ ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) “ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) = { 𝑡 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑡 ) ∈ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) }
64 59 61 63 3eqtr4g ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) “ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) )
65 simpl ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ )
66 65 feqmptd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → 𝐹 = ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) )
67 66 cnveqd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ◡ 𝐹 = ◡ ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) )
68 67 imaeq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) = ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) “ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) )
69 64 68 eqtr4d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = ( ◡ 𝐹 “ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) )
70 imaundi ⊢ ( ◡ 𝐹 “ ( ( -∞ (,) - 𝑥 ) ∪ ( 𝑥 (,) +∞ ) ) ) = ( ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∪ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) )
71 69 70 eqtrdi ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = ( ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∪ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ) )
72 71 adantlr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = ( ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∪ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ) )
73 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∈ dom vol )
74 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
75 unmbl ⊢ ( ( ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∈ dom vol ∧ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ) → ( ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∪ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ) ∈ dom vol )
76 73 74 75 syl2anc ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∪ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ) ∈ dom vol )
77 76 ancoms ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → ( ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∪ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ) ∈ dom vol )
78 77 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) ∧ 𝑥 ∈ ℝ ) → ( ( ◡ 𝐹 “ ( -∞ (,) - 𝑥 ) ) ∪ ( ◡ 𝐹 “ ( 𝑥 (,) +∞ ) ) ) ∈ dom vol )
79 72 78 eqeltrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
80 abslt ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ↔ ( - 𝑥 < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) < 𝑥 ) ) )
81 1 80 sylan ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ↔ ( - 𝑥 < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) < 𝑥 ) ) )
82 elioomnf ⊢ ( 𝑥 ∈ ℝ* → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ) ) )
83 19 82 syl ⊢ ( 𝑥 ∈ ℝ → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ) ) )
84 11 biantrurd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ) ) )
85 84 bicomd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ) )
86 83 85 sylan9bbr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) < 𝑥 ) )
87 34 19 jca ⊢ ( 𝑥 ∈ ℝ → ( - 𝑥 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) )
88 1 rexrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ* )
89 elioo5 ⊢ ( ( - 𝑥 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑡 ) ∈ ( - 𝑥 (,) 𝑥 ) ↔ ( - 𝑥 < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) < 𝑥 ) ) )
90 89 3expa ⊢ ( ( ( - 𝑥 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑡 ) ∈ ( - 𝑥 (,) 𝑥 ) ↔ ( - 𝑥 < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) < 𝑥 ) ) )
91 87 88 90 syl2anr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑡 ) ∈ ( - 𝑥 (,) 𝑥 ) ↔ ( - 𝑥 < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) < 𝑥 ) ) )
92 81 86 91 3bitr4d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( - 𝑥 (,) 𝑥 ) ) )
93 92 an32s ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑡 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( 𝐹 ‘ 𝑡 ) ∈ ( - 𝑥 (,) 𝑥 ) ) )
94 93 rabbidva ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → { 𝑡 ∈ 𝐴 ∣ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) } = { 𝑡 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑡 ) ∈ ( - 𝑥 (,) 𝑥 ) } )
95 60 mptpreima ⊢ ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) = { 𝑡 ∈ 𝐴 ∣ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) }
96 62 mptpreima ⊢ ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) “ ( - 𝑥 (,) 𝑥 ) ) = { 𝑡 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑡 ) ∈ ( - 𝑥 (,) 𝑥 ) }
97 94 95 96 3eqtr4g ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) = ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) “ ( - 𝑥 (,) 𝑥 ) ) )
98 67 imaeq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( - 𝑥 (,) 𝑥 ) ) = ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑡 ) ) “ ( - 𝑥 (,) 𝑥 ) ) )
99 97 98 eqtr4d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) = ( ◡ 𝐹 “ ( - 𝑥 (,) 𝑥 ) ) )
100 99 adantlr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) = ( ◡ 𝐹 “ ( - 𝑥 (,) 𝑥 ) ) )
101 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( ◡ 𝐹 “ ( - 𝑥 (,) 𝑥 ) ) ∈ dom vol )
102 101 ancoms ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → ( ◡ 𝐹 “ ( - 𝑥 (,) 𝑥 ) ) ∈ dom vol )
103 102 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) ∧ 𝑥 ∈ ℝ ) → ( ◡ 𝐹 “ ( - 𝑥 (,) 𝑥 ) ) ∈ dom vol )
104 100 103 eqeltrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
105 13 18 79 104 ismbf2d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → ( 𝑡 ∈ 𝐴 ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn )
106 10 105 eqeltrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → ( abs ∘ 𝐹 ) ∈ MblFn )