Step | Hyp | Ref
| Expression |
1 | | mbff 23200 |
. . . . . . 7
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
2 | 1 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹:dom 𝐹⟶ℂ) |
3 | | ffn 5958 |
. . . . . 6
⊢ (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹 Fn dom 𝐹) |
5 | | iblmbf 23340 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝐿1
→ 𝐺 ∈
MblFn) |
6 | 5 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺 ∈ MblFn) |
7 | | mbff 23200 |
. . . . . . 7
⊢ (𝐺 ∈ MblFn → 𝐺:dom 𝐺⟶ℂ) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺:dom 𝐺⟶ℂ) |
9 | | ffn 5958 |
. . . . . 6
⊢ (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺 Fn dom 𝐺) |
11 | | mbfdm 23201 |
. . . . . 6
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
12 | 11 | ad2antrr 758 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐹 ∈ dom vol) |
13 | | mbfdm 23201 |
. . . . . 6
⊢ (𝐺 ∈ MblFn → dom 𝐺 ∈ dom
vol) |
14 | 6, 13 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → dom 𝐺 ∈ dom vol) |
15 | | eqid 2610 |
. . . . 5
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
16 | | eqidd 2611 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
17 | | eqidd 2611 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
18 | 4, 10, 12, 14, 15, 16, 17 | offval 6802 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝐹 ∘𝑓 · 𝐺) = (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) |
19 | | ovex 6577 |
. . . . . 6
⊢ ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ V |
20 | 19 | a1i 11 |
. . . . 5
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ V) |
21 | | simpll 786 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐹 ∈ MblFn) |
22 | 21, 6 | mbfmul 23299 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn) |
23 | 18, 22 | eqeltrrd 2689 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ MblFn) |
24 | 23, 20 | mbfmptcl 23210 |
. . . . . . . 8
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ) |
25 | | eqidd 2611 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) = (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) |
26 | | absf 13925 |
. . . . . . . . . 10
⊢
abs:ℂ⟶ℝ |
27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) →
abs:ℂ⟶ℝ) |
28 | 27 | feqmptd 6159 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → abs = (𝑦 ∈ ℂ ↦ (abs‘𝑦))) |
29 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = ((𝐹‘𝑧) · (𝐺‘𝑧)) → (abs‘𝑦) = (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) |
30 | 24, 25, 28, 29 | fmptco 6303 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (abs ∘ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) = (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))))) |
31 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) = (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) |
32 | 24, 31 | fmptd 6292 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))):(dom 𝐹 ∩ dom 𝐺)⟶ℂ) |
33 | | ax-resscn 9872 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
34 | | ssid 3587 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
35 | | cncfss 22510 |
. . . . . . . . . . 11
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)) |
36 | 33, 34, 35 | mp2an 704 |
. . . . . . . . . 10
⊢
(ℂ–cn→ℝ)
⊆ (ℂ–cn→ℂ) |
37 | | abscncf 22512 |
. . . . . . . . . 10
⊢ abs
∈ (ℂ–cn→ℝ) |
38 | 36, 37 | sselii 3565 |
. . . . . . . . 9
⊢ abs
∈ (ℂ–cn→ℂ) |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → abs ∈ (ℂ–cn→ℂ)) |
40 | | cncombf 23231 |
. . . . . . . 8
⊢ (((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ MblFn ∧ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ abs ∈
(ℂ–cn→ℂ)) →
(abs ∘ (𝑧 ∈ (dom
𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ MblFn) |
41 | 23, 32, 39, 40 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (abs ∘ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ MblFn) |
42 | 30, 41 | eqeltrrd 2689 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ MblFn) |
43 | 24 | abscld 14023 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ ℝ) |
44 | 43 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈
ℝ*) |
45 | 24 | absge0d 14031 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) |
46 | | elxrge0 12152 |
. . . . . . . . . . 11
⊢
((abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ (0[,]+∞) ↔
((abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ ℝ* ∧ 0 ≤
(abs‘((𝐹‘𝑧) · (𝐺‘𝑧))))) |
47 | 44, 45, 46 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ∈ (0[,]+∞)) |
48 | | 0e0iccpnf 12154 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,]+∞) |
49 | 48 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ∈
(0[,]+∞)) |
50 | 47, 49 | ifclda 4070 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ∈
(0[,]+∞)) |
51 | 50 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ∈
(0[,]+∞)) |
52 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) |
53 | 51, 52 | fmptd 6292 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))),
0)):ℝ⟶(0[,]+∞)) |
54 | | reex 9906 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → ℝ ∈
V) |
56 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℝ) |
57 | 56 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ 𝐺 ∈
𝐿1) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈ ℝ) |
58 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↔ (𝑧 ∈ dom 𝐹 ∧ 𝑧 ∈ dom 𝐺)) |
59 | 58 | simprbi 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺) |
60 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ) |
61 | 8, 59, 60 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑧) ∈ ℂ) |
62 | 61 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘(𝐺‘𝑧)) ∈ ℝ) |
63 | 61 | absge0d 14031 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ (abs‘(𝐺‘𝑧))) |
64 | | elrege0 12149 |
. . . . . . . . . . . . . . . . 17
⊢
((abs‘(𝐺‘𝑧)) ∈ (0[,)+∞) ↔
((abs‘(𝐺‘𝑧)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑧)))) |
65 | 62, 63, 64 | sylanbrc 695 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘(𝐺‘𝑧)) ∈ (0[,)+∞)) |
66 | | 0e0icopnf 12153 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
(0[,)+∞) |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ∈
(0[,)+∞)) |
68 | 65, 67 | ifclda 4070 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0) ∈
(0[,)+∞)) |
69 | 68 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ MblFn
∧ 𝐺 ∈
𝐿1) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0) ∈
(0[,)+∞)) |
70 | | fconstmpt 5085 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
× {𝑥}) = (𝑧 ∈ ℝ ↦ 𝑥) |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (ℝ × {𝑥}) = (𝑧 ∈ ℝ ↦ 𝑥)) |
72 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) |
73 | 55, 57, 69, 71, 72 | offval2 6812 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((ℝ × {𝑥}) ∘𝑓
· (𝑧 ∈ ℝ
↦ if(𝑧 ∈ (dom
𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) = (𝑧 ∈ ℝ ↦ (𝑥 · if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)))) |
74 | | ovif2 6636 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 · if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) = if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), (𝑥 · 0)) |
75 | 56 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝑥 ∈ ℂ) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → 𝑥 ∈ ℂ) |
77 | 76 | mul01d 10114 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑥 · 0) = 0) |
78 | 77 | ifeq2d 4055 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), (𝑥 · 0)) = if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
79 | 74, 78 | syl5eq 2656 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑥 · if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) = if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
80 | 79 | mpteq2dv 4673 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑧 ∈ ℝ ↦ (𝑥 · if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
81 | 73, 80 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((ℝ × {𝑥}) ∘𝑓
· (𝑧 ∈ ℝ
↦ if(𝑧 ∈ (dom
𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
82 | 81 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘((ℝ × {𝑥}) ∘𝑓 ·
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)))) = (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)))) |
83 | 68 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0) ∈
(0[,)+∞)) |
84 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)) |
85 | 83, 84 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)),
0)):ℝ⟶(0[,)+∞)) |
86 | 85 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)),
0)):ℝ⟶(0[,)+∞)) |
87 | | inss2 3796 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺) |
89 | 23, 20 | mbfdm2 23211 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) |
90 | 8 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ) |
91 | 8 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺 = (𝑧 ∈ dom 𝐺 ↦ (𝐺‘𝑧))) |
92 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → 𝐺 ∈
𝐿1) |
93 | 91, 92 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ dom 𝐺 ↦ (𝐺‘𝑧)) ∈
𝐿1) |
94 | 88, 89, 90, 93 | iblss 23377 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑧)) ∈
𝐿1) |
95 | 61, 94 | iblabs 23401 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘(𝐺‘𝑧))) ∈
𝐿1) |
96 | 62, 63 | iblpos 23365 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘(𝐺‘𝑧))) ∈ 𝐿1 ↔
((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘(𝐺‘𝑧))) ∈ MblFn ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘(𝐺‘𝑧)), 0))) ∈ ℝ))) |
97 | 95, 96 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘(𝐺‘𝑧))) ∈ MblFn ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘(𝐺‘𝑧)), 0))) ∈ ℝ)) |
98 | 97 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))) ∈ ℝ) |
99 | 98 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘(𝐺‘𝑧)), 0))) ∈ ℝ) |
100 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → 𝑥 ∈ ℝ) |
101 | | neq0 3889 |
. . . . . . . . . . . . . . 15
⊢ (¬
(dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∃𝑧 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) |
102 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ∈ ℝ) |
104 | 58 | simplbi 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹) |
105 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
106 | 2, 104, 105 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑧) ∈ ℂ) |
107 | 106 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
108 | | simplrl 796 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑥 ∈ ℝ) |
109 | 106 | absge0d 14031 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ (abs‘(𝐹‘𝑧))) |
110 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) |
111 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
112 | 111 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑧 → (abs‘(𝐹‘𝑦)) = (abs‘(𝐹‘𝑧))) |
113 | 112 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑧 → ((abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑥)) |
114 | 113 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑦 ∈
dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
115 | 110, 104,
114 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘(𝐹‘𝑧)) ≤ 𝑥) |
116 | 103, 107,
108, 109, 115 | letrd 10073 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ 𝑥) |
117 | 116 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 0 ≤ 𝑥)) |
118 | 117 | exlimdv 1848 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∃𝑧 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 0 ≤ 𝑥)) |
119 | 101, 118 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (¬ (dom 𝐹 ∩ dom 𝐺) = ∅ → 0 ≤ 𝑥)) |
120 | 119 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → 0 ≤ 𝑥) |
121 | | elrege0 12149 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
122 | 100, 120,
121 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → 𝑥 ∈ (0[,)+∞)) |
123 | 86, 99, 122 | itg2mulc 23320 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘((ℝ × {𝑥}) ∘𝑓 ·
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)))) = (𝑥 · (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))))) |
124 | 82, 123 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) = (𝑥 · (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0))))) |
125 | 100, 99 | remulcld 9949 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) → (𝑥 · (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘(𝐺‘𝑧)), 0)))) ∈ ℝ) |
126 | 124, 125 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ (dom 𝐹 ∩ dom 𝐺) = ∅) →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ) |
127 | 126 | ex 449 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (¬ (dom 𝐹 ∩ dom 𝐺) = ∅ →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ)) |
128 | | noel 3878 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑧 ∈
∅ |
129 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↔ 𝑧 ∈ ∅)) |
130 | 128, 129 | mtbiri 316 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) |
131 | | iffalse 4045 |
. . . . . . . . . . . . 13
⊢ (¬
𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) = 0) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . 12
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) = 0) |
133 | 132 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ 0)) |
134 | | fconstmpt 5085 |
. . . . . . . . . . 11
⊢ (ℝ
× {0}) = (𝑧 ∈
ℝ ↦ 0) |
135 | 133, 134 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) = (ℝ ×
{0})) |
136 | 135 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) = (∫2‘(ℝ
× {0}))) |
137 | | itg20 23310 |
. . . . . . . . . 10
⊢
(∫2‘(ℝ × {0})) = 0 |
138 | 137, 102 | eqeltri 2684 |
. . . . . . . . 9
⊢
(∫2‘(ℝ × {0})) ∈
ℝ |
139 | 136, 138 | syl6eqel 2696 |
. . . . . . . 8
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ) |
140 | 127, 139 | pm2.61d2 171 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) ∈ ℝ) |
141 | 108, 62 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝑥 · (abs‘(𝐺‘𝑧))) ∈ ℝ) |
142 | 141 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝑥 · (abs‘(𝐺‘𝑧))) ∈
ℝ*) |
143 | 108, 62, 116, 63 | mulge0d 10483 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 0 ≤ (𝑥 · (abs‘(𝐺‘𝑧)))) |
144 | | elxrge0 12152 |
. . . . . . . . . . . 12
⊢ ((𝑥 · (abs‘(𝐺‘𝑧))) ∈ (0[,]+∞) ↔ ((𝑥 · (abs‘(𝐺‘𝑧))) ∈ ℝ* ∧ 0 ≤
(𝑥 ·
(abs‘(𝐺‘𝑧))))) |
145 | 142, 143,
144 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝑥 · (abs‘(𝐺‘𝑧))) ∈ (0[,]+∞)) |
146 | 145, 49 | ifclda 4070 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) ∈
(0[,]+∞)) |
147 | 146 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ ℝ) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) ∈
(0[,]+∞)) |
148 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
149 | 147, 148 | fmptd 6292 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))),
0)):ℝ⟶(0[,]+∞)) |
150 | 106, 61 | absmuld 14041 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) = ((abs‘(𝐹‘𝑧)) · (abs‘(𝐺‘𝑧)))) |
151 | | abscl 13866 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧) ∈ ℂ → (abs‘(𝐺‘𝑧)) ∈ ℝ) |
152 | | absge0 13875 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧) ∈ ℂ → 0 ≤
(abs‘(𝐺‘𝑧))) |
153 | 151, 152 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑧) ∈ ℂ → ((abs‘(𝐺‘𝑧)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑧)))) |
154 | 61, 153 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((abs‘(𝐺‘𝑧)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑧)))) |
155 | | lemul1a 10756 |
. . . . . . . . . . . . . 14
⊢
((((abs‘(𝐹‘𝑧)) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ((abs‘(𝐺‘𝑧)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑧)))) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑥) → ((abs‘(𝐹‘𝑧)) · (abs‘(𝐺‘𝑧))) ≤ (𝑥 · (abs‘(𝐺‘𝑧)))) |
156 | 107, 108,
154, 115, 155 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((abs‘(𝐹‘𝑧)) · (abs‘(𝐺‘𝑧))) ≤ (𝑥 · (abs‘(𝐺‘𝑧)))) |
157 | 150, 156 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))) ≤ (𝑥 · (abs‘(𝐺‘𝑧)))) |
158 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) = (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) |
159 | 158 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) = (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) |
160 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) = (𝑥 · (abs‘(𝐺‘𝑧)))) |
161 | 160 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0) = (𝑥 · (abs‘(𝐺‘𝑧)))) |
162 | 157, 159,
161 | 3brtr4d 4615 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
163 | | 0le0 10987 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
0 |
164 | 163 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (¬
𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 0 ≤ 0) |
165 | | iffalse 4045 |
. . . . . . . . . . . . 13
⊢ (¬
𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) = 0) |
166 | 164, 165,
131 | 3brtr4d 4615 |
. . . . . . . . . . . 12
⊢ (¬
𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
167 | 166 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) ∧ ¬ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
168 | 162, 167 | pm2.61dan 828 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
169 | 168 | ralrimivw 2950 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ∀𝑧 ∈ ℝ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0) ≤ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) |
170 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ℝ ∈ V) |
171 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) |
172 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)) = (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
173 | 170, 51, 147, 171, 172 | ofrfval2 6813 |
. . . . . . . . 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))) |
174 | 169, 173 | mpbird 246 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0)) ∘𝑟 ≤
(𝑧 ∈ ℝ ↦
if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0))) |
175 | | itg2le 23312 |
. . . . . . . 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)))) |
176 | 53, 149, 174, 175 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ≤
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (𝑥 · (abs‘(𝐺‘𝑧))), 0)))) |
177 | | itg2lecl 23311 |
. . . . . . 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))) ∈ ℝ) |
178 | 53, 140, 176, 177 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (∫2‘(𝑧 ∈ ℝ ↦ if(𝑧 ∈ (dom 𝐹 ∩ dom 𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ∈ ℝ) |
179 | 43, 45 | iblpos 23365 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → ((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ 𝐿1 ↔
((𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈ MblFn ∧
(∫2‘(𝑧
∈ ℝ ↦ if(𝑧
∈ (dom 𝐹 ∩ dom
𝐺), (abs‘((𝐹‘𝑧) · (𝐺‘𝑧))), 0))) ∈ ℝ))) |
180 | 42, 178, 179 | mpbir2and 959 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (abs‘((𝐹‘𝑧) · (𝐺‘𝑧)))) ∈
𝐿1) |
181 | 20, 23, 180 | iblabsr 23402 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑧) · (𝐺‘𝑧))) ∈
𝐿1) |
182 | 18, 181 | eqeltrd 2688 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
∧ (𝑥 ∈ ℝ
∧ ∀𝑦 ∈ dom
𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)) → (𝐹 ∘𝑓 · 𝐺) ∈
𝐿1) |
183 | 182 | rexlimdvaa 3014 |
. 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1)
→ (∃𝑥 ∈
ℝ ∀𝑦 ∈
dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 → (𝐹 ∘𝑓 · 𝐺) ∈
𝐿1)) |
184 | 183 | 3impia 1253 |
1
⊢ ((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1
∧ ∃𝑥 ∈
ℝ ∀𝑦 ∈
dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝐹 ∘𝑓 · 𝐺) ∈
𝐿1) |