Step | Hyp | Ref
| Expression |
1 | | i1ff 24597 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
2 | 1 | ffvelrnda 6923 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℝ) |
3 | | i1ff 24597 |
. . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
4 | 3 | ffvelrnda 6923 |
. . . . . . 7
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐺‘𝑥) ∈
ℝ) |
5 | | absreim 14882 |
. . . . . . 7
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (𝐺‘𝑥) ∈ ℝ) → (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))) = (√‘(((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2)))) |
6 | 2, 4, 5 | syl2an 599 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
∧ (𝐺 ∈ dom
∫1 ∧ 𝑥
∈ ℝ)) → (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))) = (√‘(((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2)))) |
7 | 6 | anandirs 679 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))) = (√‘(((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2)))) |
8 | 2 | recnd 10886 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℂ) |
9 | 8 | sqvald 13738 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ ((𝐹‘𝑥)↑2) = ((𝐹‘𝑥) · (𝐹‘𝑥))) |
10 | 4 | recnd 10886 |
. . . . . . . . 9
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐺‘𝑥) ∈
ℂ) |
11 | 10 | sqvald 13738 |
. . . . . . . 8
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ ((𝐺‘𝑥)↑2) = ((𝐺‘𝑥) · (𝐺‘𝑥))) |
12 | 9, 11 | oveqan12d 7251 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
∧ (𝐺 ∈ dom
∫1 ∧ 𝑥
∈ ℝ)) → (((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2)) = (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥)))) |
13 | 12 | anandirs 679 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2)) = (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥)))) |
14 | 13 | fveq2d 6740 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (√‘(((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2))) = (√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))))) |
15 | 7, 14 | eqtrd 2778 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))) = (√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))))) |
16 | 15 | mpteq2dva 5165 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝑥 ∈ ℝ ↦ (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥))))) = (𝑥 ∈ ℝ ↦
(√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥)))))) |
17 | | ax-icn 10813 |
. . . . . . 7
⊢ i ∈
ℂ |
18 | | mulcl 10838 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ) → (i · (𝐺‘𝑥)) ∈ ℂ) |
19 | 17, 10, 18 | sylancr 590 |
. . . . . 6
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (i · (𝐺‘𝑥)) ∈ ℂ) |
20 | | addcl 10836 |
. . . . . 6
⊢ (((𝐹‘𝑥) ∈ ℂ ∧ (i · (𝐺‘𝑥)) ∈ ℂ) → ((𝐹‘𝑥) + (i · (𝐺‘𝑥))) ∈ ℂ) |
21 | 8, 19, 20 | syl2an 599 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
∧ (𝐺 ∈ dom
∫1 ∧ 𝑥
∈ ℝ)) → ((𝐹‘𝑥) + (i · (𝐺‘𝑥))) ∈ ℂ) |
22 | 21 | anandirs 679 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → ((𝐹‘𝑥) + (i · (𝐺‘𝑥))) ∈ ℂ) |
23 | | reex 10845 |
. . . . . 6
⊢ ℝ
∈ V |
24 | 23 | a1i 11 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ℝ ∈ V) |
25 | 2 | adantlr 715 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
26 | | ovexd 7267 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (i · (𝐺‘𝑥)) ∈ V) |
27 | 1 | feqmptd 6799 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
28 | 27 | adantr 484 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → 𝐹
= (𝑥 ∈ ℝ ↦
(𝐹‘𝑥))) |
29 | 23 | a1i 11 |
. . . . . . 7
⊢ (𝐺 ∈ dom ∫1
→ ℝ ∈ V) |
30 | 17 | a1i 11 |
. . . . . . 7
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ i ∈ ℂ) |
31 | | fconstmpt 5626 |
. . . . . . . 8
⊢ (ℝ
× {i}) = (𝑥 ∈
ℝ ↦ i) |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ (𝐺 ∈ dom ∫1
→ (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i)) |
33 | 3 | feqmptd 6799 |
. . . . . . 7
⊢ (𝐺 ∈ dom ∫1
→ 𝐺 = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) |
34 | 29, 30, 4, 32, 33 | offval2 7507 |
. . . . . 6
⊢ (𝐺 ∈ dom ∫1
→ ((ℝ × {i}) ∘f · 𝐺) = (𝑥 ∈ ℝ ↦ (i · (𝐺‘𝑥)))) |
35 | 34 | adantl 485 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ((ℝ × {i}) ∘f ·
𝐺) = (𝑥 ∈ ℝ ↦ (i · (𝐺‘𝑥)))) |
36 | 24, 25, 26, 28, 35 | offval2 7507 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐹 ∘f + ((ℝ ×
{i}) ∘f · 𝐺)) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑥) + (i · (𝐺‘𝑥))))) |
37 | | absf 14926 |
. . . . . 6
⊢
abs:ℂ⟶ℝ |
38 | 37 | a1i 11 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → abs:ℂ⟶ℝ) |
39 | 38 | feqmptd 6799 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → abs = (𝑦 ∈ ℂ ↦ (abs‘𝑦))) |
40 | | fveq2 6736 |
. . . 4
⊢ (𝑦 = ((𝐹‘𝑥) + (i · (𝐺‘𝑥))) → (abs‘𝑦) = (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥))))) |
41 | 22, 36, 39, 40 | fmptco 6963 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (abs ∘ (𝐹 ∘f + ((ℝ ×
{i}) ∘f · 𝐺))) = (𝑥 ∈ ℝ ↦ (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))))) |
42 | 8, 8 | mulcld 10878 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ ((𝐹‘𝑥) · (𝐹‘𝑥)) ∈ ℂ) |
43 | 10, 10 | mulcld 10878 |
. . . . . 6
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ ((𝐺‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
44 | | addcl 10836 |
. . . . . 6
⊢ ((((𝐹‘𝑥) · (𝐹‘𝑥)) ∈ ℂ ∧ ((𝐺‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) → (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))) ∈ ℂ) |
45 | 42, 43, 44 | syl2an 599 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
∧ (𝐺 ∈ dom
∫1 ∧ 𝑥
∈ ℝ)) → (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))) ∈ ℂ) |
46 | 45 | anandirs 679 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))) ∈ ℂ) |
47 | 42 | adantlr 715 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → ((𝐹‘𝑥) · (𝐹‘𝑥)) ∈ ℂ) |
48 | 43 | adantll 714 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → ((𝐺‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
49 | 23 | a1i 11 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ ℝ ∈ V) |
50 | 49, 2, 2, 27, 27 | offval2 7507 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝐹
∘f · 𝐹) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑥) · (𝐹‘𝑥)))) |
51 | 50 | adantr 484 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐹 ∘f · 𝐹) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑥) · (𝐹‘𝑥)))) |
52 | 29, 4, 4, 33, 33 | offval2 7507 |
. . . . . 6
⊢ (𝐺 ∈ dom ∫1
→ (𝐺
∘f · 𝐺) = (𝑥 ∈ ℝ ↦ ((𝐺‘𝑥) · (𝐺‘𝑥)))) |
53 | 52 | adantl 485 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐺 ∘f · 𝐺) = (𝑥 ∈ ℝ ↦ ((𝐺‘𝑥) · (𝐺‘𝑥)))) |
54 | 24, 47, 48, 51, 53 | offval2 7507 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) = (𝑥 ∈ ℝ ↦ (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))))) |
55 | | sqrtf 14952 |
. . . . . 6
⊢
√:ℂ⟶ℂ |
56 | 55 | a1i 11 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → √:ℂ⟶ℂ) |
57 | 56 | feqmptd 6799 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → √ = (𝑦 ∈ ℂ ↦ (√‘𝑦))) |
58 | | fveq2 6736 |
. . . 4
⊢ (𝑦 = (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))) → (√‘𝑦) = (√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))))) |
59 | 46, 54, 57, 58 | fmptco 6963 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) = (𝑥 ∈ ℝ ↦
(√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥)))))) |
60 | 16, 41, 59 | 3eqtr4d 2788 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (abs ∘ (𝐹 ∘f + ((ℝ ×
{i}) ∘f · 𝐺))) = (√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)))) |
61 | | elrege0 13067 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
62 | | resqrtcl 14842 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(√‘𝑥) ∈
ℝ) |
63 | 61, 62 | sylbi 220 |
. . . . . 6
⊢ (𝑥 ∈ (0[,)+∞) →
(√‘𝑥) ∈
ℝ) |
64 | 63 | adantl 485 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ (0[,)+∞)) → (√‘𝑥) ∈ ℝ) |
65 | | id 22 |
. . . . . . . . 9
⊢
(√:ℂ⟶ℂ →
√:ℂ⟶ℂ) |
66 | 65 | feqmptd 6799 |
. . . . . . . 8
⊢
(√:ℂ⟶ℂ → √ = (𝑥 ∈ ℂ ↦ (√‘𝑥))) |
67 | 55, 66 | ax-mp 5 |
. . . . . . 7
⊢ √ =
(𝑥 ∈ ℂ ↦
(√‘𝑥)) |
68 | 67 | reseq1i 5862 |
. . . . . 6
⊢ (√
↾ (0[,)+∞)) = ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾
(0[,)+∞)) |
69 | | rge0ssre 13069 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
70 | | ax-resscn 10811 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
71 | 69, 70 | sstri 3925 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℂ |
72 | | resmpt 5920 |
. . . . . . 7
⊢
((0[,)+∞) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾ (0[,)+∞)) =
(𝑥 ∈ (0[,)+∞)
↦ (√‘𝑥))) |
73 | 71, 72 | ax-mp 5 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ↦
(√‘𝑥)) ↾
(0[,)+∞)) = (𝑥 ∈
(0[,)+∞) ↦ (√‘𝑥)) |
74 | 68, 73 | eqtri 2766 |
. . . . 5
⊢ (√
↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) |
75 | 64, 74 | fmptd 6950 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (√ ↾
(0[,)+∞)):(0[,)+∞)⟶ℝ) |
76 | | ge0addcl 13073 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,)+∞)) |
77 | 76 | adantl 485 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ (𝑥
∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞)) |
78 | | oveq12 7241 |
. . . . . . . . 9
⊢ ((𝑧 = 𝐹 ∧ 𝑧 = 𝐹) → (𝑧 ∘f · 𝑧) = (𝐹 ∘f · 𝐹)) |
79 | 78 | anidms 570 |
. . . . . . . 8
⊢ (𝑧 = 𝐹 → (𝑧 ∘f · 𝑧) = (𝐹 ∘f · 𝐹)) |
80 | 79 | feq1d 6549 |
. . . . . . 7
⊢ (𝑧 = 𝐹 → ((𝑧 ∘f · 𝑧):ℝ⟶(0[,)+∞)
↔ (𝐹
∘f · 𝐹):ℝ⟶(0[,)+∞))) |
81 | | i1ff 24597 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ dom ∫1
→ 𝑧:ℝ⟶ℝ) |
82 | 81 | ffvelrnda 6923 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑧‘𝑥) ∈
ℝ) |
83 | 82, 82 | remulcld 10888 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ ((𝑧‘𝑥) · (𝑧‘𝑥)) ∈ ℝ) |
84 | 82 | msqge0d 11425 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ ((𝑧‘𝑥) · (𝑧‘𝑥))) |
85 | | elrege0 13067 |
. . . . . . . . . 10
⊢ (((𝑧‘𝑥) · (𝑧‘𝑥)) ∈ (0[,)+∞) ↔ (((𝑧‘𝑥) · (𝑧‘𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑧‘𝑥) · (𝑧‘𝑥)))) |
86 | 83, 84, 85 | sylanbrc 586 |
. . . . . . . . 9
⊢ ((𝑧 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ ((𝑧‘𝑥) · (𝑧‘𝑥)) ∈ (0[,)+∞)) |
87 | 86 | fmpttd 6951 |
. . . . . . . 8
⊢ (𝑧 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ ((𝑧‘𝑥) · (𝑧‘𝑥))):ℝ⟶(0[,)+∞)) |
88 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑧 ∈ dom ∫1
→ ℝ ∈ V) |
89 | 81 | feqmptd 6799 |
. . . . . . . . . 10
⊢ (𝑧 ∈ dom ∫1
→ 𝑧 = (𝑥 ∈ ℝ ↦ (𝑧‘𝑥))) |
90 | 88, 82, 82, 89, 89 | offval2 7507 |
. . . . . . . . 9
⊢ (𝑧 ∈ dom ∫1
→ (𝑧
∘f · 𝑧) = (𝑥 ∈ ℝ ↦ ((𝑧‘𝑥) · (𝑧‘𝑥)))) |
91 | 90 | feq1d 6549 |
. . . . . . . 8
⊢ (𝑧 ∈ dom ∫1
→ ((𝑧
∘f · 𝑧):ℝ⟶(0[,)+∞) ↔ (𝑥 ∈ ℝ ↦ ((𝑧‘𝑥) · (𝑧‘𝑥))):ℝ⟶(0[,)+∞))) |
92 | 87, 91 | mpbird 260 |
. . . . . . 7
⊢ (𝑧 ∈ dom ∫1
→ (𝑧
∘f · 𝑧):ℝ⟶(0[,)+∞)) |
93 | 80, 92 | vtoclga 3502 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝐹
∘f · 𝐹):ℝ⟶(0[,)+∞)) |
94 | 93 | adantr 484 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐹 ∘f · 𝐹):ℝ⟶(0[,)+∞)) |
95 | | oveq12 7241 |
. . . . . . . . 9
⊢ ((𝑧 = 𝐺 ∧ 𝑧 = 𝐺) → (𝑧 ∘f · 𝑧) = (𝐺 ∘f · 𝐺)) |
96 | 95 | anidms 570 |
. . . . . . . 8
⊢ (𝑧 = 𝐺 → (𝑧 ∘f · 𝑧) = (𝐺 ∘f · 𝐺)) |
97 | 96 | feq1d 6549 |
. . . . . . 7
⊢ (𝑧 = 𝐺 → ((𝑧 ∘f · 𝑧):ℝ⟶(0[,)+∞)
↔ (𝐺
∘f · 𝐺):ℝ⟶(0[,)+∞))) |
98 | 97, 92 | vtoclga 3502 |
. . . . . 6
⊢ (𝐺 ∈ dom ∫1
→ (𝐺
∘f · 𝐺):ℝ⟶(0[,)+∞)) |
99 | 98 | adantl 485 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐺 ∘f · 𝐺):ℝ⟶(0[,)+∞)) |
100 | | inidm 4148 |
. . . . 5
⊢ (ℝ
∩ ℝ) = ℝ |
101 | 77, 94, 99, 24, 24, 100 | off 7505 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)):ℝ⟶(0[,)+∞)) |
102 | | fco2 6591 |
. . . 4
⊢
(((√ ↾ (0[,)+∞)):(0[,)+∞)⟶ℝ ∧
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺)):ℝ⟶(0[,)+∞)) →
(√ ∘ ((𝐹
∘f · 𝐹) ∘f + (𝐺 ∘f · 𝐺))):ℝ⟶ℝ) |
103 | 75, 101, 102 | syl2anc 587 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))):ℝ⟶ℝ) |
104 | | rnco 6131 |
. . . 4
⊢ ran
(√ ∘ ((𝐹
∘f · 𝐹) ∘f + (𝐺 ∘f · 𝐺))) = ran (√ ↾ ran
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺))) |
105 | | ffn 6564 |
. . . . . . . 8
⊢
(√:ℂ⟶ℂ → √ Fn
ℂ) |
106 | 55, 105 | ax-mp 5 |
. . . . . . 7
⊢ √
Fn ℂ |
107 | | readdcl 10837 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
108 | 107 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ (𝑥
∈ ℝ ∧ 𝑦
∈ ℝ)) → (𝑥
+ 𝑦) ∈
ℝ) |
109 | | remulcl 10839 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
110 | 109 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ (𝑥 ∈ ℝ
∧ 𝑦 ∈ ℝ))
→ (𝑥 · 𝑦) ∈
ℝ) |
111 | 110, 1, 1, 49, 49, 100 | off 7505 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (𝐹
∘f · 𝐹):ℝ⟶ℝ) |
112 | 111 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐹 ∘f · 𝐹):ℝ⟶ℝ) |
113 | 109 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ dom ∫1
∧ (𝑥 ∈ ℝ
∧ 𝑦 ∈ ℝ))
→ (𝑥 · 𝑦) ∈
ℝ) |
114 | 113, 3, 3, 29, 29, 100 | off 7505 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ dom ∫1
→ (𝐺
∘f · 𝐺):ℝ⟶ℝ) |
115 | 114 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐺 ∘f · 𝐺):ℝ⟶ℝ) |
116 | 108, 112,
115, 24, 24, 100 | off 7505 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)):ℝ⟶ℝ) |
117 | 116 | frnd 6572 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) ⊆
ℝ) |
118 | 117, 70 | sstrdi 3928 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) ⊆
ℂ) |
119 | | fnssres 6519 |
. . . . . . 7
⊢ ((√
Fn ℂ ∧ ran ((𝐹
∘f · 𝐹) ∘f + (𝐺 ∘f · 𝐺)) ⊆ ℂ) →
(√ ↾ ran ((𝐹
∘f · 𝐹) ∘f + (𝐺 ∘f · 𝐺))) Fn ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) |
120 | 106, 118,
119 | sylancr 590 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (√ ↾ ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) Fn ran ((𝐹 ∘f ·
𝐹) ∘f +
(𝐺 ∘f
· 𝐺))) |
121 | | id 22 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈ dom
∫1) |
122 | 121, 121 | i1fmul 24617 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝐹
∘f · 𝐹) ∈ dom
∫1) |
123 | 122 | adantr 484 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐹 ∘f · 𝐹) ∈ dom
∫1) |
124 | | id 22 |
. . . . . . . . . 10
⊢ (𝐺 ∈ dom ∫1
→ 𝐺 ∈ dom
∫1) |
125 | 124, 124 | i1fmul 24617 |
. . . . . . . . 9
⊢ (𝐺 ∈ dom ∫1
→ (𝐺
∘f · 𝐺) ∈ dom
∫1) |
126 | 125 | adantl 485 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (𝐺 ∘f · 𝐺) ∈ dom
∫1) |
127 | 123, 126 | i1fadd 24616 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) ∈ dom
∫1) |
128 | | i1frn 24598 |
. . . . . . 7
⊢ (((𝐹 ∘f ·
𝐹) ∘f +
(𝐺 ∘f
· 𝐺)) ∈ dom
∫1 → ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) ∈
Fin) |
129 | 127, 128 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) ∈
Fin) |
130 | | fnfi 8881 |
. . . . . 6
⊢
(((√ ↾ ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) Fn ran ((𝐹 ∘f ·
𝐹) ∘f +
(𝐺 ∘f
· 𝐺)) ∧ ran
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺)) ∈ Fin) → (√ ↾ ran
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺))) ∈ Fin) |
131 | 120, 129,
130 | syl2anc 587 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (√ ↾ ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) ∈
Fin) |
132 | | rnfi 8984 |
. . . . 5
⊢ ((√
↾ ran ((𝐹
∘f · 𝐹) ∘f + (𝐺 ∘f · 𝐺))) ∈ Fin → ran
(√ ↾ ran ((𝐹
∘f · 𝐹) ∘f + (𝐺 ∘f · 𝐺))) ∈ Fin) |
133 | 131, 132 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ran (√ ↾ ran ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) ∈
Fin) |
134 | 104, 133 | eqeltrid 2843 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → ran (√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) ∈
Fin) |
135 | | cnvco 5769 |
. . . . . . 7
⊢ ◡(√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) = (◡((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) ∘ ◡√) |
136 | 135 | imaeq1i 5941 |
. . . . . 6
⊢ (◡(√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) “ {𝑥}) = ((◡((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) ∘ ◡√) “ {𝑥}) |
137 | | imaco 6130 |
. . . . . 6
⊢ ((◡((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) ∘ ◡√) “ {𝑥}) = (◡((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) “ (◡√ “ {𝑥})) |
138 | 136, 137 | eqtri 2766 |
. . . . 5
⊢ (◡(√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) “ {𝑥}) = (◡((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) “ (◡√ “ {𝑥})) |
139 | | i1fima 24599 |
. . . . . 6
⊢ (((𝐹 ∘f ·
𝐹) ∘f +
(𝐺 ∘f
· 𝐺)) ∈ dom
∫1 → (◡((𝐹 ∘f ·
𝐹) ∘f +
(𝐺 ∘f
· 𝐺)) “ (◡√ “ {𝑥})) ∈ dom vol) |
140 | 127, 139 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (◡((𝐹 ∘f ·
𝐹) ∘f +
(𝐺 ∘f
· 𝐺)) “ (◡√ “ {𝑥})) ∈ dom vol) |
141 | 138, 140 | eqeltrid 2843 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (◡(√
∘ ((𝐹
∘f · 𝐹) ∘f + (𝐺 ∘f · 𝐺))) “ {𝑥}) ∈ dom vol) |
142 | 141 | adantr 484 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ (ran (√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) ∖ {0})) →
(◡(√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) “ {𝑥}) ∈ dom
vol) |
143 | 138 | fveq2i 6739 |
. . . 4
⊢
(vol‘(◡(√ ∘
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺))) “ {𝑥})) = (vol‘(◡((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) “ (◡√ “ {𝑥}))) |
144 | | eldifsni 4718 |
. . . . . . . 8
⊢ (𝑥 ∈ (ran (√ ∘
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺))) ∖ {0}) → 𝑥 ≠ 0) |
145 | | c0ex 10852 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
146 | 145 | elsn 4571 |
. . . . . . . . . . 11
⊢ (0 ∈
{𝑥} ↔ 0 = 𝑥) |
147 | | eqcom 2745 |
. . . . . . . . . . 11
⊢ (0 =
𝑥 ↔ 𝑥 = 0) |
148 | 146, 147 | bitri 278 |
. . . . . . . . . 10
⊢ (0 ∈
{𝑥} ↔ 𝑥 = 0) |
149 | 148 | necon3bbii 2989 |
. . . . . . . . 9
⊢ (¬ 0
∈ {𝑥} ↔ 𝑥 ≠ 0) |
150 | | sqrt0 14830 |
. . . . . . . . . 10
⊢
(√‘0) = 0 |
151 | 150 | eleq1i 2829 |
. . . . . . . . 9
⊢
((√‘0) ∈ {𝑥} ↔ 0 ∈ {𝑥}) |
152 | 149, 151 | xchnxbir 336 |
. . . . . . . 8
⊢ (¬
(√‘0) ∈ {𝑥} ↔ 𝑥 ≠ 0) |
153 | 144, 152 | sylibr 237 |
. . . . . . 7
⊢ (𝑥 ∈ (ran (√ ∘
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺))) ∖ {0}) → ¬
(√‘0) ∈ {𝑥}) |
154 | 153 | olcd 874 |
. . . . . 6
⊢ (𝑥 ∈ (ran (√ ∘
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺))) ∖ {0}) → (¬ 0 ∈
ℂ ∨ ¬ (√‘0) ∈ {𝑥})) |
155 | | ianor 982 |
. . . . . . 7
⊢ (¬ (0
∈ ℂ ∧ (√‘0) ∈ {𝑥}) ↔ (¬ 0 ∈ ℂ ∨ ¬
(√‘0) ∈ {𝑥})) |
156 | | elpreima 6897 |
. . . . . . . 8
⊢ (√
Fn ℂ → (0 ∈ (◡√
“ {𝑥}) ↔ (0
∈ ℂ ∧ (√‘0) ∈ {𝑥}))) |
157 | 55, 105, 156 | mp2b 10 |
. . . . . . 7
⊢ (0 ∈
(◡√ “ {𝑥}) ↔ (0 ∈ ℂ ∧
(√‘0) ∈ {𝑥})) |
158 | 155, 157 | xchnxbir 336 |
. . . . . 6
⊢ (¬ 0
∈ (◡√ “ {𝑥}) ↔ (¬ 0 ∈
ℂ ∨ ¬ (√‘0) ∈ {𝑥})) |
159 | 154, 158 | sylibr 237 |
. . . . 5
⊢ (𝑥 ∈ (ran (√ ∘
((𝐹 ∘f
· 𝐹)
∘f + (𝐺
∘f · 𝐺))) ∖ {0}) → ¬ 0 ∈
(◡√ “ {𝑥})) |
160 | | i1fima2 24600 |
. . . . 5
⊢ ((((𝐹 ∘f ·
𝐹) ∘f +
(𝐺 ∘f
· 𝐺)) ∈ dom
∫1 ∧ ¬ 0 ∈ (◡√ “ {𝑥})) → (vol‘(◡((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) “ (◡√ “ {𝑥}))) ∈ ℝ) |
161 | 127, 159,
160 | syl2an 599 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ (ran (√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) ∖ {0})) →
(vol‘(◡((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺)) “ (◡√ “ {𝑥}))) ∈ ℝ) |
162 | 143, 161 | eqeltrid 2843 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) ∧ 𝑥
∈ (ran (√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) ∖ {0})) →
(vol‘(◡(√ ∘ ((𝐹 ∘f ·
𝐹) ∘f +
(𝐺 ∘f
· 𝐺))) “
{𝑥})) ∈
ℝ) |
163 | 103, 134,
142, 162 | i1fd 24602 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (√ ∘ ((𝐹 ∘f · 𝐹) ∘f + (𝐺 ∘f ·
𝐺))) ∈ dom
∫1) |
164 | 60, 163 | eqeltrd 2839 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈ dom
∫1) → (abs ∘ (𝐹 ∘f + ((ℝ ×
{i}) ∘f · 𝐺))) ∈ dom
∫1) |