Step | Hyp | Ref
| Expression |
1 | | mbff 23394 |
. . . . . . 7
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
2 | 1 | ad2antrr 762 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ) |
3 | | ffn 6045 |
. . . . . 6
⊢ (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹 Fn dom 𝐹) |
5 | | iblmbf 23534 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝐿1
→ 𝐺 ∈
MblFn) |
6 | 5 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺 ∈ MblFn) |
7 | | mbff 23394 |
. . . . . . 7
⊢ (𝐺 ∈ MblFn → 𝐺:dom 𝐺⟶ℂ) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺:dom 𝐺⟶ℂ) |
9 | | ffn 6045 |
. . . . . 6
⊢ (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺 Fn dom 𝐺) |
11 | | mbfdm 23395 |
. . . . . 6
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
12 | 11 | ad2antrr 762 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol) |
13 | | mbfdm 23395 |
. . . . . 6
⊢ (𝐺 ∈ MblFn → dom 𝐺 ∈ dom
vol) |
14 | 6, 13 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐺 ∈ dom vol) |
15 | | eqid 2622 |
. . . . 5
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
16 | | eqidd 2623 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
17 | | eqidd 2623 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
18 | 4, 10, 12, 14, 15, 16, 17 | offval 6904 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝐹 ∘𝑓 · 𝐺) = (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) |
19 | | ovexd 6680 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ V) |
20 | | simpll 790 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹 ∈ MblFn) |
21 | 20, 6 | mbfmul 23493 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn) |
22 | 18, 21 | eqeltrrd 2702 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ MblFn) |
23 | 22, 19 | mbfmptcl 23404 |
. . . . . . . 8
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ) |
24 | | eqidd 2623 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) = (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) |
25 | | absf 14077 |
. . . . . . . . . 10
⊢
abs:ℂ⟶ℝ |
26 | 25 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) →
abs:ℂ⟶ℝ) |
27 | 26 | feqmptd 6249 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → abs = (𝑦 ∈ ℂ ↦ (abs‘𝑦))) |
28 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = ((𝐹‘𝑧) · (𝐺‘𝑧)) → (abs‘𝑦) = (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) |
29 | 23, 24, 27, 28 | fmptco 6396 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (abs ∘ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) = (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))))) |
30 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) = (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) |
31 | 23, 30 | fmptd 6385 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))):(dom 𝐹 ∩ dom 𝐺)⟶ℂ) |
32 | | ax-resscn 9993 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
33 | | ssid 3624 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
34 | | cncfss 22702 |
. . . . . . . . . . 11
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)) |
35 | 32, 33, 34 | mp2an 708 |
. . . . . . . . . 10
⊢
(ℂ–cn→ℝ)
⊆ (ℂ–cn→ℂ) |
36 | | abscncf 22704 |
. . . . . . . . . 10
⊢ abs
∈ (ℂ–cn→ℝ) |
37 | 35, 36 | sselii 3600 |
. . . . . . . . 9
⊢ abs
∈ (ℂ–cn→ℂ) |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → abs ∈ (ℂ–cn→ℂ)) |
39 | | cncombf 23425 |
. . . . . . . 8
⊢ (((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ MblFn ∧ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ abs ∈
(ℂ–cn→ℂ)) →
(abs ∘ (𝑧 ∈ (dom
𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ MblFn) |
40 | 22, 31, 38, 39 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (abs ∘ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ MblFn) |
41 | 29, 40 | eqeltrrd 2702 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ MblFn) |
42 | 23 | abscld 14175 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ ℝ) |
43 | 42 | rexrd 10089 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈
ℝ*) |
44 | 23 | absge0d 14183 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) |
45 | | elxrge0 12281 |
. . . . . . . . . . 11
⊢
((abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ (0[,]+∞) ↔
((abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ ℝ* ∧ 0 ≤
(abs‘((𝐹‘𝑧) · (𝐺‘𝑧))))) |
46 | 43, 44, 45 | sylanbrc 698 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ (0[,]+∞)) |
47 | | 0e0iccpnf 12283 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,]+∞) |
48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ∈
(0[,]+∞)) |
49 | 46, 48 | ifclda 4120 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ∈
(0[,]+∞)) |
50 | 49 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ∈
(0[,]+∞)) |
51 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) |
52 | 50, 51 | fmptd 6385 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))),
0)):ℝ⟶(0[,]+∞)) |
53 | | reex 10027 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → ℝ ∈
V) |
55 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ) |
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ 𝐺 ∈
𝐿1) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ ℝ) |
57 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↔ (𝑧 ∈ dom 𝐹 ∧ 𝑧 ∈ dom 𝐺)) |
58 | 57 | simprbi 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺) |
59 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ) |
60 | 8, 58, 59 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑧) ∈ ℂ) |
61 | 60 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘(𝐺‘𝑧)) ∈ ℝ) |
62 | 60 | absge0d 14183 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ (abs‘(𝐺‘𝑧))) |
63 | | elrege0 12278 |
. . . . . . . . . . . . . . . . 17
⊢
((abs‘(𝐺‘𝑧)) ∈ (0[,)+∞) ↔
((abs‘(𝐺‘𝑧)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑧)))) |
64 | 61, 62, 63 | sylanbrc 698 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘(𝐺‘𝑧)) ∈ (0[,)+∞)) |
65 | | 0e0icopnf 12282 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
(0[,)+∞) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ∈
(0[,)+∞)) |
67 | 64, 66 | ifclda 4120 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0) ∈
(0[,)+∞)) |
68 | 67 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ 𝐺 ∈
𝐿1) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0) ∈
(0[,)+∞)) |
69 | | fconstmpt 5163 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
× {𝑥}) = (𝑧 ∈ ℝ ↦ 𝑥) |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (ℝ × {𝑥}) = (𝑧 ∈ ℝ ↦ 𝑥)) |
71 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) |
72 | 54, 56, 68, 70, 71 | offval2 6914 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((ℝ × {𝑥}) ∘𝑓
· (𝑧 ∈ ℝ
↦ if(𝑧 ∈ (dom
𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) = (𝑧 ∈ ℝ ↦ (𝑥 · if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)))) |
73 | | ovif2 6738 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 · if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) = if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), (𝑥 · 0)) |
74 | 55 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℂ) |
75 | 74 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → 𝑥 ∈ ℂ) |
76 | 75 | mul01d 10235 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑥 · 0) = 0) |
77 | 76 | ifeq2d 4105 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), (𝑥 · 0)) = if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
78 | 73, 77 | syl5eq 2668 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑥 · if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) = if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
79 | 78 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑧 ∈ ℝ ↦ (𝑥 · if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
80 | 72, 79 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((ℝ × {𝑥}) ∘𝑓
· (𝑧 ∈ ℝ
↦ if(𝑧 ∈ (dom
𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘((ℝ × {𝑥}) ∘𝑓 ·
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)))) = (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)))) |
82 | 67 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0) ∈
(0[,)+∞)) |
83 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) |
84 | 82, 83 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)),
0)):ℝ⟶(0[,)+∞)) |
85 | 84 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)),
0)):ℝ⟶(0[,)+∞)) |
86 | | inss2 3834 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺) |
88 | 22, 19 | mbfdm2 23405 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) |
89 | 8 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ) |
90 | 8 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺 = (𝑧 ∈ dom 𝐺 ↦ (𝐺‘𝑧))) |
91 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺 ∈
𝐿1) |
92 | 90, 91 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐺 ↦ (𝐺‘𝑧)) ∈
𝐿1) |
93 | 87, 88, 89, 92 | iblss 23571 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑧)) ∈
𝐿1) |
94 | 60, 93 | iblabs 23595 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘(𝐺‘𝑧))) ∈
𝐿1) |
95 | 61, 62 | iblpos 23559 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘(𝐺‘𝑧))) ∈ 𝐿1 ↔
((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘(𝐺‘𝑧))) ∈ MblFn ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘(𝐺‘𝑧)), 0))) ∈ ℝ))) |
96 | 94, 95 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘(𝐺‘𝑧))) ∈ MblFn ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘(𝐺‘𝑧)), 0))) ∈ ℝ)) |
97 | 96 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) ∈ ℝ) |
98 | 97 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘(𝐺‘𝑧)), 0))) ∈ ℝ) |
99 | | simplrl 800 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → 𝑥 ∈ ℝ) |
100 | | neq0 3930 |
. . . . . . . . . . . . . . 15
⊢ (¬
(dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∃𝑧 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) |
101 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
102 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ∈ ℝ) |
103 | 57 | simplbi 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹) |
104 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
105 | 2, 103, 104 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑧) ∈ ℂ) |
106 | 105 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
107 | | simplrl 800 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑥 ∈ ℝ) |
108 | 105 | absge0d 14183 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ (abs‘(𝐹‘𝑧))) |
109 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) |
110 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
111 | 110 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑧 → (abs‘(𝐹‘𝑦)) = (abs‘(𝐹‘𝑧))) |
112 | 111 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑧 → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑥)) |
113 | 112 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑦 ∈
dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
114 | 109, 103,
113 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
115 | 102, 106,
107, 108, 114 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ 𝑥) |
116 | 115 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 0 ≤ 𝑥)) |
117 | 116 | exlimdv 1861 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∃𝑧 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 0 ≤ 𝑥)) |
118 | 100, 117 | syl5bi 232 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (¬ (dom 𝐹 ∩ dom 𝐺) = ∅ → 0 ≤ 𝑥)) |
119 | 118 | imp 445 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → 0 ≤ 𝑥) |
120 | | elrege0 12278 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
121 | 99, 119, 120 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → 𝑥 ∈ (0[,)+∞)) |
122 | 85, 98, 121 | itg2mulc 23514 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘((ℝ × {𝑥}) ∘𝑓 ·
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)))) = (𝑥 · (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))))) |
123 | 81, 122 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) = (𝑥 · (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))))) |
124 | 99, 98 | remulcld 10070 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑥 · (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)))) ∈ ℝ) |
125 | 123, 124 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ) |
126 | 125 | ex 450 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (¬ (dom 𝐹 ∩ dom 𝐺) = ∅ →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ)) |
127 | | noel 3919 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑧 ∈
∅ |
128 | | eleq2 2690 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↔ 𝑧 ∈ ∅)) |
129 | 127, 128 | mtbiri 317 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) |
130 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) = 0) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . 12
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) = 0) |
132 | 131 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ 0)) |
133 | | fconstmpt 5163 |
. . . . . . . . . . 11
⊢ (ℝ
× {0}) = (𝑧 ∈
ℝ ↦ 0) |
134 | 132, 133 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) = (ℝ ×
{0})) |
135 | 134 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) = (∫2‘(ℝ
× {0}))) |
136 | | itg20 23504 |
. . . . . . . . . 10
⊢
(∫2‘(ℝ × {0})) = 0 |
137 | 136, 101 | eqeltri 2697 |
. . . . . . . . 9
⊢
(∫2‘(ℝ × {0})) ∈
ℝ |
138 | 135, 137 | syl6eqel 2709 |
. . . . . . . 8
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ) |
139 | 126, 138 | pm2.61d2 172 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ) |
140 | 107, 61 | remulcld 10070 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝑥 · (abs‘(𝐺‘𝑧))) ∈ ℝ) |
141 | 140 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝑥 · (abs‘(𝐺‘𝑧))) ∈
ℝ*) |
142 | 107, 61, 115, 62 | mulge0d 10604 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ (𝑥 · (abs‘(𝐺‘𝑧)))) |
143 | | elxrge0 12281 |
. . . . . . . . . . . 12
⊢ ((𝑥 · (abs‘(𝐺‘𝑧))) ∈ (0[,]+∞) ↔ ((𝑥 · (abs‘(𝐺‘𝑧))) ∈ ℝ* ∧ 0 ≤
(𝑥 ·
(abs‘(𝐺‘𝑧))))) |
144 | 141, 142,
143 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝑥 · (abs‘(𝐺‘𝑧))) ∈ (0[,]+∞)) |
145 | 144, 48 | ifclda 4120 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) ∈
(0[,]+∞)) |
146 | 145 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) ∈
(0[,]+∞)) |
147 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
148 | 146, 147 | fmptd 6385 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))),
0)):ℝ⟶(0[,]+∞)) |
149 | 105, 60 | absmuld 14193 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) = ((abs‘(𝐹‘𝑧)) · (abs‘(𝐺‘𝑧)))) |
150 | | abscl 14018 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧) ∈ ℂ → (abs‘(𝐺‘𝑧)) ∈ ℝ) |
151 | | absge0 14027 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧) ∈ ℂ → 0 ≤
(abs‘(𝐺‘𝑧))) |
152 | 150, 151 | jca 554 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑧) ∈ ℂ → ((abs‘(𝐺‘𝑧)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑧)))) |
153 | 60, 152 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((abs‘(𝐺‘𝑧)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑧)))) |
154 | | lemul1a 10877 |
. . . . . . . . . . . . . 14
⊢
((((abs‘(𝐹‘𝑧)) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ((abs‘(𝐺‘𝑧)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑧)))) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑥) → ((abs‘(𝐹‘𝑧)) · (abs‘(𝐺‘𝑧))) ≤ (𝑥 · (abs‘(𝐺‘𝑧)))) |
155 | 106, 107,
153, 114, 154 | syl31anc 1329 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((abs‘(𝐹‘𝑧)) · (abs‘(𝐺‘𝑧))) ≤ (𝑥 · (abs‘(𝐺‘𝑧)))) |
156 | 149, 155 | eqbrtrd 4675 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ≤ (𝑥 · (abs‘(𝐺‘𝑧)))) |
157 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) = (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) |
158 | 157 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) = (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) |
159 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) = (𝑥 · (abs‘(𝐺‘𝑧)))) |
160 | 159 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) = (𝑥 · (abs‘(𝐺‘𝑧)))) |
161 | 156, 158,
160 | 3brtr4d 4685 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
162 | | 0le0 11110 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
0 |
163 | 162 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (¬
𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 0 ≤ 0) |
164 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) = 0) |
165 | 163, 164,
130 | 3brtr4d 4685 |
. . . . . . . . . . . 12
⊢ (¬
𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
166 | 165 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
167 | 161, 166 | pm2.61dan 832 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
168 | 167 | ralrimivw 2967 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
169 | 53 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ℝ ∈ V) |
170 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) |
171 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
172 | 169, 50, 146, 170, 171 | ofrfval2 6915 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) ↔ ∀𝑧 ∈ ℝ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
173 | 168, 172 | mpbird 247 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
174 | | itg2le 23506 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)):ℝ⟶(0[,]+∞) ∧
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ≤
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)))) |
175 | 52, 148, 173, 174 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ≤
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)))) |
176 | | itg2lecl 23505 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ≤
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)))) →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ∈ ℝ) |
177 | 52, 139, 175, 176 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ∈ ℝ) |
178 | 42, 44 | iblpos 23559 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ 𝐿1 ↔
((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ MblFn ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ∈ ℝ))) |
179 | 41, 177, 178 | mpbir2and 957 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈
𝐿1) |
180 | 19, 22, 179 | iblabsr 23596 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) ∈
𝐿1) |
181 | 18, 180 | eqeltrd 2701 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝐹 ∘𝑓 · 𝐺) ∈
𝐿1) |
182 | 181 | rexlimdvaa 3032 |
. 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
→ (∃𝑥 ∈
ℝ ∀𝑦 ∈
dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝐹 ∘𝑓 · 𝐺) ∈
𝐿1)) |
183 | 182 | 3impia 1261 |
1
⊢ ((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1
∧ ∃𝑥 ∈
ℝ ∀𝑦 ∈
dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝐹 ∘𝑓 · 𝐺) ∈
𝐿1) |