Step | Hyp | Ref
| Expression |
1 | | iblabs.3 |
. . 3
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
2 | | iblabs.4 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈
𝐿1) |
3 | | iblabs.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ) |
4 | 3 | iblrelem 23557 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ))) |
5 | 2, 4 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ)) |
6 | 5 | simp1d 1073 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn) |
7 | 6, 3 | mbfdm2 23405 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ dom vol) |
8 | | mblss 23299 |
. . . . 5
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
10 | | rembl 23308 |
. . . . 5
⊢ ℝ
∈ dom vol |
11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈ dom
vol) |
12 | | iftrue 4092 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = (abs‘(𝐹‘𝐵))) |
13 | 12 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = (abs‘(𝐹‘𝐵))) |
14 | 3 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℂ) |
15 | 14 | abscld 14175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐹‘𝐵)) ∈ ℝ) |
16 | 13, 15 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) ∈ ℝ) |
17 | | eldifn 3733 |
. . . . . 6
⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴) |
18 | 17 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴) |
19 | | iffalse 4095 |
. . . . 5
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = 0) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = 0) |
21 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) |
22 | | absf 14077 |
. . . . . . . . 9
⊢
abs:ℂ⟶ℝ |
23 | 22 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
24 | 23 | feqmptd 6249 |
. . . . . . 7
⊢ (𝜑 → abs = (𝑦 ∈ ℂ ↦ (abs‘𝑦))) |
25 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐵) → (abs‘𝑦) = (abs‘(𝐹‘𝐵))) |
26 | 14, 21, 24, 25 | fmptco 6396 |
. . . . . 6
⊢ (𝜑 → (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (abs‘(𝐹‘𝐵)))) |
27 | 12 | mpteq2ia 4740 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) = (𝑥 ∈ 𝐴 ↦ (abs‘(𝐹‘𝐵))) |
28 | 26, 27 | syl6reqr 2675 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) = (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)))) |
29 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) |
30 | 14, 29 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)):𝐴⟶ℂ) |
31 | | ax-resscn 9993 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
32 | | ssid 3624 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
33 | | cncfss 22702 |
. . . . . . . . 9
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)) |
34 | 31, 32, 33 | mp2an 708 |
. . . . . . . 8
⊢
(ℂ–cn→ℝ)
⊆ (ℂ–cn→ℂ) |
35 | | abscncf 22704 |
. . . . . . . 8
⊢ abs
∈ (ℂ–cn→ℝ) |
36 | 34, 35 | sselii 3600 |
. . . . . . 7
⊢ abs
∈ (ℂ–cn→ℂ) |
37 | 36 | a1i 11 |
. . . . . 6
⊢ (𝜑 → abs ∈
(ℂ–cn→ℂ)) |
38 | | cncombf 23425 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)):𝐴⟶ℂ ∧ abs ∈
(ℂ–cn→ℂ)) →
(abs ∘ (𝑥 ∈
𝐴 ↦ (𝐹‘𝐵))) ∈ MblFn) |
39 | 6, 30, 37, 38 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) ∈ MblFn) |
40 | 28, 39 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) ∈ MblFn) |
41 | 9, 11, 16, 20, 40 | mbfss 23413 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) ∈ MblFn) |
42 | 1, 41 | syl5eqel 2705 |
. 2
⊢ (𝜑 → 𝐺 ∈ MblFn) |
43 | | reex 10027 |
. . . . . . . . 9
⊢ ℝ
∈ V |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
V) |
45 | | ifan 4134 |
. . . . . . . . . 10
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) |
46 | | 0re 10040 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
47 | | ifcl 4130 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝐵) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ) |
48 | 3, 46, 47 | sylancl 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ) |
49 | | max1 12016 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝐵), (𝐹‘𝐵), 0)) |
50 | 46, 3, 49 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) |
51 | | elrege0 12278 |
. . . . . . . . . . . 12
⊢ (if(0
≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ (0[,)+∞) ↔ (if(0
≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
(𝐹‘𝐵), (𝐹‘𝐵), 0))) |
52 | 48, 50, 51 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
53 | | 0e0icopnf 12282 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,)+∞) |
54 | 53 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
55 | 52, 54 | ifclda 4120 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) ∈
(0[,)+∞)) |
56 | 45, 55 | syl5eqel 2705 |
. . . . . . . . 9
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
57 | 56 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
58 | | ifan 4134 |
. . . . . . . . . 10
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) |
59 | 3 | renegcld 10457 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐹‘𝐵) ∈ ℝ) |
60 | | ifcl 4130 |
. . . . . . . . . . . . 13
⊢ ((-(𝐹‘𝐵) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ) |
61 | 59, 46, 60 | sylancl 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ) |
62 | | max1 12016 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ -(𝐹‘𝐵) ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝐵), -(𝐹‘𝐵), 0)) |
63 | 46, 59, 62 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) |
64 | | elrege0 12278 |
. . . . . . . . . . . 12
⊢ (if(0
≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ (0[,)+∞) ↔ (if(0
≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
-(𝐹‘𝐵), -(𝐹‘𝐵), 0))) |
65 | 61, 63, 64 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
66 | 65, 54 | ifclda 4120 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) ∈
(0[,)+∞)) |
67 | 58, 66 | syl5eqel 2705 |
. . . . . . . . 9
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
68 | 67 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
69 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) |
70 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) |
71 | 44, 57, 68, 69, 70 | offval2 6914 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) |
72 | 45, 58 | oveq12i 6662 |
. . . . . . . . 9
⊢
(if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) |
73 | | max0add 14050 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝐵) ∈ ℝ → (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (abs‘(𝐹‘𝐵))) |
74 | 3, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (abs‘(𝐹‘𝐵))) |
75 | | iftrue 4092 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) |
76 | 75 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) |
77 | | iftrue 4092 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) |
78 | 77 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) |
79 | 76, 78 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0))) |
80 | 74, 79, 13 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
81 | 80 | ex 450 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))) |
82 | | 00id 10211 |
. . . . . . . . . . 11
⊢ (0 + 0) =
0 |
83 | | iffalse 4095 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = 0) |
84 | | iffalse 4095 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = 0) |
85 | 83, 84 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = (0 + 0)) |
86 | 82, 85, 19 | 3eqtr4a 2682 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
87 | 81, 86 | pm2.61d1 171 |
. . . . . . . . 9
⊢ (𝜑 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
88 | 72, 87 | syl5eq 2668 |
. . . . . . . 8
⊢ (𝜑 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) |
89 | 88 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))) |
90 | 71, 89 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))) |
91 | 90, 1 | syl6reqr 2675 |
. . . . 5
⊢ (𝜑 → 𝐺 = ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) |
92 | 91 | fveq2d 6195 |
. . . 4
⊢ (𝜑 →
(∫2‘𝐺)
= (∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))))) |
93 | 56 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
94 | 45, 83 | syl5eq 2668 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = 0) |
95 | 18, 94 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = 0) |
96 | | ibar 525 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (0 ≤ (𝐹‘𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)))) |
97 | 96 | ifbid 4108 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) |
98 | 97 | mpteq2ia 4740 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) |
99 | 3, 6 | mbfpos 23418 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) ∈ MblFn) |
100 | 98, 99 | syl5eqelr 2706 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∈ MblFn) |
101 | 9, 11, 93, 95, 100 | mbfss 23413 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∈ MblFn) |
102 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) |
103 | 57, 102 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵),
0)):ℝ⟶(0[,)+∞)) |
104 | 5 | simp2d 1074 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ) |
105 | 67 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈
(0[,)+∞)) |
106 | 58, 84 | syl5eq 2668 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = 0) |
107 | 18, 106 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = 0) |
108 | | ibar 525 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (0 ≤ -(𝐹‘𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)))) |
109 | 108 | ifbid 4108 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) |
110 | 109 | mpteq2ia 4740 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) |
111 | 3, 6 | mbfneg 23417 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐹‘𝐵)) ∈ MblFn) |
112 | 59, 111 | mbfpos 23418 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) ∈ MblFn) |
113 | 110, 112 | syl5eqelr 2706 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) ∈ MblFn) |
114 | 9, 11, 105, 107, 113 | mbfss 23413 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) ∈ MblFn) |
115 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) |
116 | 68, 115 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵),
0)):ℝ⟶(0[,)+∞)) |
117 | 5 | simp3d 1075 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ) |
118 | 101, 103,
104, 114, 116, 117 | itg2add 23526 |
. . . 4
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))))) |
119 | 92, 118 | eqtrd 2656 |
. . 3
⊢ (𝜑 →
(∫2‘𝐺)
= ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))))) |
120 | 104, 117 | readdcld 10069 |
. . 3
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) ∈ ℝ) |
121 | 119, 120 | eqeltrd 2701 |
. 2
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ) |
122 | 42, 121 | jca 554 |
1
⊢ (𝜑 → (𝐺 ∈ MblFn ∧
(∫2‘𝐺)
∈ ℝ)) |