Proof of Theorem iblabslem
| Step | Hyp | Ref
| Expression |
| 1 | | iblabs.3 |
. . 3
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
| 2 | | iblabs.4 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈
𝐿1) |
| 3 | | iblabs.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ) |
| 4 | 3 | iblrelem 25826 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ))) |
| 5 | 2, 4 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ)) |
| 6 | 5 | simp1d 1143 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn) |
| 7 | 6, 3 | mbfdm2 25672 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ dom vol) |
| 8 | | mblss 25566 |
. . . . 5
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
| 9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 10 | | rembl 25575 |
. . . . 5
⊢ ℝ
∈ dom vol |
| 11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈ dom
vol) |
| 12 | | iftrue 4531 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = (abs‘(𝐹‘𝐵))) |
| 13 | 12 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = (abs‘(𝐹‘𝐵))) |
| 14 | 3 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℂ) |
| 15 | 14 | abscld 15475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐹‘𝐵)) ∈ ℝ) |
| 16 | 13, 15 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) ∈ ℝ) |
| 17 | | eldifn 4132 |
. . . . . 6
⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴) |
| 18 | 17 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴) |
| 19 | | iffalse 4534 |
. . . . 5
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = 0) |
| 20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = 0) |
| 21 | 12 | mpteq2ia 5245 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) = (𝑥 ∈ 𝐴 ↦ (abs‘(𝐹‘𝐵))) |
| 22 | | absf 15376 |
. . . . . . . 8
⊢
abs:ℂ⟶ℝ |
| 23 | 22 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
| 24 | 23, 14 | cofmpt 7152 |
. . . . . 6
⊢ (𝜑 → (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (abs‘(𝐹‘𝐵)))) |
| 25 | 21, 24 | eqtr4id 2796 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) = (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)))) |
| 26 | 14 | fmpttd 7135 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)):𝐴⟶ℂ) |
| 27 | | ax-resscn 11212 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
| 28 | | ssid 4006 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
| 29 | | cncfss 24925 |
. . . . . . . . 9
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)) |
| 30 | 27, 28, 29 | mp2an 692 |
. . . . . . . 8
⊢
(ℂ–cn→ℝ)
⊆ (ℂ–cn→ℂ) |
| 31 | | abscncf 24927 |
. . . . . . . 8
⊢ abs
∈ (ℂ–cn→ℝ) |
| 32 | 30, 31 | sselii 3980 |
. . . . . . 7
⊢ abs
∈ (ℂ–cn→ℂ) |
| 33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝜑 → abs ∈
(ℂ–cn→ℂ)) |
| 34 | | cncombf 25693 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)):𝐴⟶ℂ ∧ abs ∈
(ℂ–cn→ℂ)) →
(abs ∘ (𝑥 ∈
𝐴 ↦ (𝐹‘𝐵))) ∈ MblFn) |
| 35 | 6, 26, 33, 34 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) ∈ MblFn) |
| 36 | 25, 35 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) ∈ MblFn) |
| 37 | 9, 11, 16, 20, 36 | mbfss 25681 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) ∈ MblFn) |
| 38 | 1, 37 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝐺 ∈ MblFn) |
| 39 | | reex 11246 |
. . . . . . . . 9
⊢ ℝ
∈ V |
| 40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
V) |
| 41 | | ifan 4579 |
. . . . . . . . . 10
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) |
| 42 | | 0re 11263 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
| 43 | | ifcl 4571 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝐵) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ) |
| 44 | 3, 42, 43 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ) |
| 45 | | max1 13227 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝐵), (𝐹‘𝐵), 0)) |
| 46 | 42, 3, 45 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) |
| 47 | | elrege0 13494 |
. . . . . . . . . . . 12
⊢ (if(0
≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ (0[,)+∞) ↔ (if(0
≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
(𝐹‘𝐵), (𝐹‘𝐵), 0))) |
| 48 | 44, 46, 47 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
| 49 | | 0e0icopnf 13498 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,)+∞) |
| 50 | 49 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
| 51 | 48, 50 | ifclda 4561 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) ∈
(0[,)+∞)) |
| 52 | 41, 51 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
| 53 | 52 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
| 54 | | ifan 4579 |
. . . . . . . . . 10
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) |
| 55 | 3 | renegcld 11690 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐹‘𝐵) ∈ ℝ) |
| 56 | | ifcl 4571 |
. . . . . . . . . . . . 13
⊢ ((-(𝐹‘𝐵) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ) |
| 57 | 55, 42, 56 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ) |
| 58 | | max1 13227 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ -(𝐹‘𝐵) ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝐵), -(𝐹‘𝐵), 0)) |
| 59 | 42, 55, 58 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) |
| 60 | | elrege0 13494 |
. . . . . . . . . . . 12
⊢ (if(0
≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ (0[,)+∞) ↔ (if(0
≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
-(𝐹‘𝐵), -(𝐹‘𝐵), 0))) |
| 61 | 57, 59, 60 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
| 62 | 61, 50 | ifclda 4561 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) ∈
(0[,)+∞)) |
| 63 | 54, 62 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
| 64 | 63 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
| 65 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) |
| 66 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) |
| 67 | 40, 53, 64, 65, 66 | offval2 7717 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) |
| 68 | 41, 54 | oveq12i 7443 |
. . . . . . . . 9
⊢
(if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) |
| 69 | | max0add 15349 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝐵) ∈ ℝ → (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (abs‘(𝐹‘𝐵))) |
| 70 | 3, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (abs‘(𝐹‘𝐵))) |
| 71 | | iftrue 4531 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) |
| 72 | 71 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) |
| 73 | | iftrue 4531 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) |
| 74 | 73 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) |
| 75 | 72, 74 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0))) |
| 76 | 70, 75, 13 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
| 77 | 76 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))) |
| 78 | | 00id 11436 |
. . . . . . . . . . 11
⊢ (0 + 0) =
0 |
| 79 | | iffalse 4534 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = 0) |
| 80 | | iffalse 4534 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = 0) |
| 81 | 79, 80 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = (0 + 0)) |
| 82 | 78, 81, 19 | 3eqtr4a 2803 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
| 83 | 77, 82 | pm2.61d1 180 |
. . . . . . . . 9
⊢ (𝜑 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
| 84 | 68, 83 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
| 85 | 84 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))) |
| 86 | 67, 85 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))) |
| 87 | 1, 86 | eqtr4id 2796 |
. . . . 5
⊢ (𝜑 → 𝐺 = ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) |
| 88 | 87 | fveq2d 6910 |
. . . 4
⊢ (𝜑 →
(∫2‘𝐺)
= (∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))))) |
| 89 | 52 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
| 90 | 41, 79 | eqtrid 2789 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = 0) |
| 91 | 18, 90 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = 0) |
| 92 | | ibar 528 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (0 ≤ (𝐹‘𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)))) |
| 93 | 92 | ifbid 4549 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) |
| 94 | 93 | mpteq2ia 5245 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) |
| 95 | 3, 6 | mbfpos 25686 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) ∈ MblFn) |
| 96 | 94, 95 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∈ MblFn) |
| 97 | 9, 11, 89, 91, 96 | mbfss 25681 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∈ MblFn) |
| 98 | 53 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵),
0)):ℝ⟶(0[,)+∞)) |
| 99 | 5 | simp2d 1144 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ) |
| 100 | 63 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
| 101 | 54, 80 | eqtrid 2789 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = 0) |
| 102 | 18, 101 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = 0) |
| 103 | | ibar 528 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (0 ≤ -(𝐹‘𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)))) |
| 104 | 103 | ifbid 4549 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) |
| 105 | 104 | mpteq2ia 5245 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) |
| 106 | 3, 6 | mbfneg 25685 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐹‘𝐵)) ∈ MblFn) |
| 107 | 55, 106 | mbfpos 25686 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) ∈ MblFn) |
| 108 | 105, 107 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) ∈ MblFn) |
| 109 | 9, 11, 100, 102, 108 | mbfss 25681 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) ∈ MblFn) |
| 110 | 64 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵),
0)):ℝ⟶(0[,)+∞)) |
| 111 | 5 | simp3d 1145 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ) |
| 112 | 97, 98, 99, 109, 110, 111 | itg2add 25794 |
. . . 4
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))))) |
| 113 | 88, 112 | eqtrd 2777 |
. . 3
⊢ (𝜑 →
(∫2‘𝐺)
= ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))))) |
| 114 | 99, 111 | readdcld 11290 |
. . 3
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) ∈ ℝ) |
| 115 | 113, 114 | eqeltrd 2841 |
. 2
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ) |
| 116 | 38, 115 | jca 511 |
1
⊢ (𝜑 → (𝐺 ∈ MblFn ∧
(∫2‘𝐺)
∈ ℝ)) |