| Step | Hyp | Ref
| Expression |
| 1 | | ffvelcdm 7101 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → (𝐹‘𝑡) ∈ ℝ) |
| 2 | 1 | recnd 11289 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → (𝐹‘𝑡) ∈ ℂ) |
| 3 | | id 22 |
. . . . 5
⊢ (𝐹:𝐴⟶ℝ → 𝐹:𝐴⟶ℝ) |
| 4 | 3 | feqmptd 6977 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → 𝐹 = (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡))) |
| 5 | | absf 15376 |
. . . . . 6
⊢
abs:ℂ⟶ℝ |
| 6 | 5 | a1i 11 |
. . . . 5
⊢ (𝐹:𝐴⟶ℝ →
abs:ℂ⟶ℝ) |
| 7 | 6 | feqmptd 6977 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → abs = (𝑥 ∈ ℂ ↦
(abs‘𝑥))) |
| 8 | | fveq2 6906 |
. . . 4
⊢ (𝑥 = (𝐹‘𝑡) → (abs‘𝑥) = (abs‘(𝐹‘𝑡))) |
| 9 | 2, 4, 7, 8 | fmptco 7149 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → (abs ∘ 𝐹) = (𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡)))) |
| 10 | 9 | adantr 480 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (abs ∘ 𝐹) = (𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡)))) |
| 11 | 2 | abscld 15475 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → (abs‘(𝐹‘𝑡)) ∈ ℝ) |
| 12 | 11 | fmpttd 7135 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → (𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))):𝐴⟶ℝ) |
| 13 | 12 | adantr 480 |
. . 3
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))):𝐴⟶ℝ) |
| 14 | | fdm 6745 |
. . . . 5
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
| 15 | 14 | adantr 480 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → dom 𝐹 = 𝐴) |
| 16 | | mbfdm 25661 |
. . . . 5
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
| 17 | 16 | adantl 481 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → dom 𝐹 ∈ dom vol) |
| 18 | 15, 17 | eqeltrrd 2842 |
. . 3
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → 𝐴 ∈ dom vol) |
| 19 | | rexr 11307 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
| 20 | | elioopnf 13483 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ*
→ ((abs‘(𝐹‘𝑡)) ∈ (𝑥(,)+∞) ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ 𝑥 < (abs‘(𝐹‘𝑡))))) |
| 21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
((abs‘(𝐹‘𝑡)) ∈ (𝑥(,)+∞) ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ 𝑥 < (abs‘(𝐹‘𝑡))))) |
| 22 | 11 | biantrurd 532 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → (𝑥 < (abs‘(𝐹‘𝑡)) ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ 𝑥 < (abs‘(𝐹‘𝑡))))) |
| 23 | 22 | bicomd 223 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → (((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ 𝑥 < (abs‘(𝐹‘𝑡))) ↔ 𝑥 < (abs‘(𝐹‘𝑡)))) |
| 24 | 21, 23 | sylan9bbr 510 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) ∈ (𝑥(,)+∞) ↔ 𝑥 < (abs‘(𝐹‘𝑡)))) |
| 25 | | ltnle 11340 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧
(abs‘(𝐹‘𝑡)) ∈ ℝ) → (𝑥 < (abs‘(𝐹‘𝑡)) ↔ ¬ (abs‘(𝐹‘𝑡)) ≤ 𝑥)) |
| 26 | 25 | ancoms 458 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 < (abs‘(𝐹‘𝑡)) ↔ ¬ (abs‘(𝐹‘𝑡)) ≤ 𝑥)) |
| 27 | 11, 26 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 < (abs‘(𝐹‘𝑡)) ↔ ¬ (abs‘(𝐹‘𝑡)) ≤ 𝑥)) |
| 28 | | absle 15354 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑡) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) ≤ 𝑥 ↔ (-𝑥 ≤ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ 𝑥))) |
| 29 | 1, 28 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) ≤ 𝑥 ↔ (-𝑥 ≤ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ 𝑥))) |
| 30 | | renegcl 11572 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → -𝑥 ∈
ℝ) |
| 31 | | lenlt 11339 |
. . . . . . . . . . . . . . . . 17
⊢ ((-𝑥 ∈ ℝ ∧ (𝐹‘𝑡) ∈ ℝ) → (-𝑥 ≤ (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) < -𝑥)) |
| 32 | 30, 1, 31 | syl2anr 597 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (-𝑥 ≤ (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) < -𝑥)) |
| 33 | 1 | biantrurd 532 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → ((𝐹‘𝑡) < -𝑥 ↔ ((𝐹‘𝑡) ∈ ℝ ∧ (𝐹‘𝑡) < -𝑥))) |
| 34 | 30 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ → -𝑥 ∈
ℝ*) |
| 35 | | elioomnf 13484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (-𝑥 ∈ ℝ*
→ ((𝐹‘𝑡) ∈ (-∞(,)-𝑥) ↔ ((𝐹‘𝑡) ∈ ℝ ∧ (𝐹‘𝑡) < -𝑥))) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → ((𝐹‘𝑡) ∈ (-∞(,)-𝑥) ↔ ((𝐹‘𝑡) ∈ ℝ ∧ (𝐹‘𝑡) < -𝑥))) |
| 37 | 36 | bicomd 223 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (((𝐹‘𝑡) ∈ ℝ ∧ (𝐹‘𝑡) < -𝑥) ↔ (𝐹‘𝑡) ∈ (-∞(,)-𝑥))) |
| 38 | 33, 37 | sylan9bb 509 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑡) < -𝑥 ↔ (𝐹‘𝑡) ∈ (-∞(,)-𝑥))) |
| 39 | 38 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (¬ (𝐹‘𝑡) < -𝑥 ↔ ¬ (𝐹‘𝑡) ∈ (-∞(,)-𝑥))) |
| 40 | 32, 39 | bitrd 279 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (-𝑥 ≤ (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ∈ (-∞(,)-𝑥))) |
| 41 | | lenlt 11339 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑡) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑡) ≤ 𝑥 ↔ ¬ 𝑥 < (𝐹‘𝑡))) |
| 42 | 1, 41 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑡) ≤ 𝑥 ↔ ¬ 𝑥 < (𝐹‘𝑡))) |
| 43 | 1 | biantrurd 532 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → (𝑥 < (𝐹‘𝑡) ↔ ((𝐹‘𝑡) ∈ ℝ ∧ 𝑥 < (𝐹‘𝑡)))) |
| 44 | | elioopnf 13483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ((𝐹‘𝑡) ∈ (𝑥(,)+∞) ↔ ((𝐹‘𝑡) ∈ ℝ ∧ 𝑥 < (𝐹‘𝑡)))) |
| 45 | 19, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → ((𝐹‘𝑡) ∈ (𝑥(,)+∞) ↔ ((𝐹‘𝑡) ∈ ℝ ∧ 𝑥 < (𝐹‘𝑡)))) |
| 46 | 45 | bicomd 223 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (((𝐹‘𝑡) ∈ ℝ ∧ 𝑥 < (𝐹‘𝑡)) ↔ (𝐹‘𝑡) ∈ (𝑥(,)+∞))) |
| 47 | 43, 46 | sylan9bb 509 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 < (𝐹‘𝑡) ↔ (𝐹‘𝑡) ∈ (𝑥(,)+∞))) |
| 48 | 47 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ∈ (𝑥(,)+∞))) |
| 49 | 42, 48 | bitrd 279 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑡) ≤ 𝑥 ↔ ¬ (𝐹‘𝑡) ∈ (𝑥(,)+∞))) |
| 50 | 40, 49 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((-𝑥 ≤ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ 𝑥) ↔ (¬ (𝐹‘𝑡) ∈ (-∞(,)-𝑥) ∧ ¬ (𝐹‘𝑡) ∈ (𝑥(,)+∞)))) |
| 51 | 29, 50 | bitrd 279 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) ≤ 𝑥 ↔ (¬ (𝐹‘𝑡) ∈ (-∞(,)-𝑥) ∧ ¬ (𝐹‘𝑡) ∈ (𝑥(,)+∞)))) |
| 52 | 51 | notbid 318 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (¬
(abs‘(𝐹‘𝑡)) ≤ 𝑥 ↔ ¬ (¬ (𝐹‘𝑡) ∈ (-∞(,)-𝑥) ∧ ¬ (𝐹‘𝑡) ∈ (𝑥(,)+∞)))) |
| 53 | | elun 4153 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑡) ∈ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞)) ↔ ((𝐹‘𝑡) ∈ (-∞(,)-𝑥) ∨ (𝐹‘𝑡) ∈ (𝑥(,)+∞))) |
| 54 | | oran 992 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑡) ∈ (-∞(,)-𝑥) ∨ (𝐹‘𝑡) ∈ (𝑥(,)+∞)) ↔ ¬ (¬ (𝐹‘𝑡) ∈ (-∞(,)-𝑥) ∧ ¬ (𝐹‘𝑡) ∈ (𝑥(,)+∞))) |
| 55 | 53, 54 | bitri 275 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑡) ∈ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞)) ↔ ¬ (¬ (𝐹‘𝑡) ∈ (-∞(,)-𝑥) ∧ ¬ (𝐹‘𝑡) ∈ (𝑥(,)+∞))) |
| 56 | 52, 55 | bitr4di 289 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (¬
(abs‘(𝐹‘𝑡)) ≤ 𝑥 ↔ (𝐹‘𝑡) ∈ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞)))) |
| 57 | 24, 27, 56 | 3bitrd 305 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) ∈ (𝑥(,)+∞) ↔ (𝐹‘𝑡) ∈ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞)))) |
| 58 | 57 | an32s 652 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑡 ∈ 𝐴) → ((abs‘(𝐹‘𝑡)) ∈ (𝑥(,)+∞) ↔ (𝐹‘𝑡) ∈ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞)))) |
| 59 | 58 | rabbidva 3443 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → {𝑡 ∈ 𝐴 ∣ (abs‘(𝐹‘𝑡)) ∈ (𝑥(,)+∞)} = {𝑡 ∈ 𝐴 ∣ (𝐹‘𝑡) ∈ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞))}) |
| 60 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) = (𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) |
| 61 | 60 | mptpreima 6258 |
. . . . . . . 8
⊢ (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (𝑥(,)+∞)) = {𝑡 ∈ 𝐴 ∣ (abs‘(𝐹‘𝑡)) ∈ (𝑥(,)+∞)} |
| 62 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) = (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) |
| 63 | 62 | mptpreima 6258 |
. . . . . . . 8
⊢ (◡(𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) “ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞))) = {𝑡 ∈ 𝐴 ∣ (𝐹‘𝑡) ∈ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞))} |
| 64 | 59, 61, 63 | 3eqtr4g 2802 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (𝑥(,)+∞)) = (◡(𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) “ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞)))) |
| 65 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → 𝐹:𝐴⟶ℝ) |
| 66 | 65 | feqmptd 6977 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → 𝐹 = (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡))) |
| 67 | 66 | cnveqd 5886 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → ◡𝐹 = ◡(𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡))) |
| 68 | 67 | imaeq1d 6077 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞))) = (◡(𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) “ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞)))) |
| 69 | 64, 68 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (𝑥(,)+∞)) = (◡𝐹 “ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞)))) |
| 70 | | imaundi 6169 |
. . . . . 6
⊢ (◡𝐹 “ ((-∞(,)-𝑥) ∪ (𝑥(,)+∞))) = ((◡𝐹 “ (-∞(,)-𝑥)) ∪ (◡𝐹 “ (𝑥(,)+∞))) |
| 71 | 69, 70 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (𝑥(,)+∞)) = ((◡𝐹 “ (-∞(,)-𝑥)) ∪ (◡𝐹 “ (𝑥(,)+∞)))) |
| 72 | 71 | adantlr 715 |
. . . 4
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (𝑥(,)+∞)) = ((◡𝐹 “ (-∞(,)-𝑥)) ∪ (◡𝐹 “ (𝑥(,)+∞)))) |
| 73 | | mbfima 25665 |
. . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (-∞(,)-𝑥)) ∈ dom vol) |
| 74 | | mbfima 25665 |
. . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom
vol) |
| 75 | | unmbl 25572 |
. . . . . . 7
⊢ (((◡𝐹 “ (-∞(,)-𝑥)) ∈ dom vol ∧ (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) → ((◡𝐹 “ (-∞(,)-𝑥)) ∪ (◡𝐹 “ (𝑥(,)+∞))) ∈ dom
vol) |
| 76 | 73, 74, 75 | syl2anc 584 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → ((◡𝐹 “ (-∞(,)-𝑥)) ∪ (◡𝐹 “ (𝑥(,)+∞))) ∈ dom
vol) |
| 77 | 76 | ancoms 458 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → ((◡𝐹 “ (-∞(,)-𝑥)) ∪ (◡𝐹 “ (𝑥(,)+∞))) ∈ dom
vol) |
| 78 | 77 | adantr 480 |
. . . 4
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) ∧ 𝑥 ∈ ℝ) → ((◡𝐹 “ (-∞(,)-𝑥)) ∪ (◡𝐹 “ (𝑥(,)+∞))) ∈ dom
vol) |
| 79 | 72, 78 | eqeltrd 2841 |
. . 3
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (𝑥(,)+∞)) ∈ dom
vol) |
| 80 | | abslt 15353 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑡) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) < 𝑥 ↔ (-𝑥 < (𝐹‘𝑡) ∧ (𝐹‘𝑡) < 𝑥))) |
| 81 | 1, 80 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) < 𝑥 ↔ (-𝑥 < (𝐹‘𝑡) ∧ (𝐹‘𝑡) < 𝑥))) |
| 82 | | elioomnf 13484 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ*
→ ((abs‘(𝐹‘𝑡)) ∈ (-∞(,)𝑥) ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ (abs‘(𝐹‘𝑡)) < 𝑥))) |
| 83 | 19, 82 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
((abs‘(𝐹‘𝑡)) ∈ (-∞(,)𝑥) ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ (abs‘(𝐹‘𝑡)) < 𝑥))) |
| 84 | 11 | biantrurd 532 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → ((abs‘(𝐹‘𝑡)) < 𝑥 ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ (abs‘(𝐹‘𝑡)) < 𝑥))) |
| 85 | 84 | bicomd 223 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → (((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ (abs‘(𝐹‘𝑡)) < 𝑥) ↔ (abs‘(𝐹‘𝑡)) < 𝑥)) |
| 86 | 83, 85 | sylan9bbr 510 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) ∈ (-∞(,)𝑥) ↔ (abs‘(𝐹‘𝑡)) < 𝑥)) |
| 87 | 34, 19 | jca 511 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (-𝑥 ∈ ℝ*
∧ 𝑥 ∈
ℝ*)) |
| 88 | 1 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) → (𝐹‘𝑡) ∈
ℝ*) |
| 89 | | elioo5 13444 |
. . . . . . . . . . . 12
⊢ ((-𝑥 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ (𝐹‘𝑡) ∈ ℝ*) → ((𝐹‘𝑡) ∈ (-𝑥(,)𝑥) ↔ (-𝑥 < (𝐹‘𝑡) ∧ (𝐹‘𝑡) < 𝑥))) |
| 90 | 89 | 3expa 1119 |
. . . . . . . . . . 11
⊢ (((-𝑥 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) ∧ (𝐹‘𝑡) ∈ ℝ*) → ((𝐹‘𝑡) ∈ (-𝑥(,)𝑥) ↔ (-𝑥 < (𝐹‘𝑡) ∧ (𝐹‘𝑡) < 𝑥))) |
| 91 | 87, 88, 90 | syl2anr 597 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑡) ∈ (-𝑥(,)𝑥) ↔ (-𝑥 < (𝐹‘𝑡) ∧ (𝐹‘𝑡) < 𝑥))) |
| 92 | 81, 86, 91 | 3bitr4d 311 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑡 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑡)) ∈ (-∞(,)𝑥) ↔ (𝐹‘𝑡) ∈ (-𝑥(,)𝑥))) |
| 93 | 92 | an32s 652 |
. . . . . . . 8
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑡 ∈ 𝐴) → ((abs‘(𝐹‘𝑡)) ∈ (-∞(,)𝑥) ↔ (𝐹‘𝑡) ∈ (-𝑥(,)𝑥))) |
| 94 | 93 | rabbidva 3443 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → {𝑡 ∈ 𝐴 ∣ (abs‘(𝐹‘𝑡)) ∈ (-∞(,)𝑥)} = {𝑡 ∈ 𝐴 ∣ (𝐹‘𝑡) ∈ (-𝑥(,)𝑥)}) |
| 95 | 60 | mptpreima 6258 |
. . . . . . 7
⊢ (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (-∞(,)𝑥)) = {𝑡 ∈ 𝐴 ∣ (abs‘(𝐹‘𝑡)) ∈ (-∞(,)𝑥)} |
| 96 | 62 | mptpreima 6258 |
. . . . . . 7
⊢ (◡(𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) “ (-𝑥(,)𝑥)) = {𝑡 ∈ 𝐴 ∣ (𝐹‘𝑡) ∈ (-𝑥(,)𝑥)} |
| 97 | 94, 95, 96 | 3eqtr4g 2802 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (-∞(,)𝑥)) = (◡(𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) “ (-𝑥(,)𝑥))) |
| 98 | 67 | imaeq1d 6077 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (-𝑥(,)𝑥)) = (◡(𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) “ (-𝑥(,)𝑥))) |
| 99 | 97, 98 | eqtr4d 2780 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (-∞(,)𝑥)) = (◡𝐹 “ (-𝑥(,)𝑥))) |
| 100 | 99 | adantlr 715 |
. . . 4
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (-∞(,)𝑥)) = (◡𝐹 “ (-𝑥(,)𝑥))) |
| 101 | | mbfima 25665 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (-𝑥(,)𝑥)) ∈ dom vol) |
| 102 | 101 | ancoms 458 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (◡𝐹 “ (-𝑥(,)𝑥)) ∈ dom vol) |
| 103 | 102 | adantr 480 |
. . . 4
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (-𝑥(,)𝑥)) ∈ dom vol) |
| 104 | 100, 103 | eqeltrd 2841 |
. . 3
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) “ (-∞(,)𝑥)) ∈ dom vol) |
| 105 | 13, 18, 79, 104 | ismbf2d 25675 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (𝑡 ∈ 𝐴 ↦ (abs‘(𝐹‘𝑡))) ∈ MblFn) |
| 106 | 10, 105 | eqeltrd 2841 |
1
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (abs ∘ 𝐹) ∈ MblFn) |