Step | Hyp | Ref
| Expression |
1 | | sinf 14854 |
. . . . . 6
⊢
sin:ℂ⟶ℂ |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
sin:ℂ⟶ℂ) |
3 | | mulcl 10020 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
4 | | eqid 2622 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) |
5 | 3, 4 | fmptd 6385 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) |
6 | | fcompt 6400 |
. . . . 5
⊢
((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) → (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))) |
7 | 2, 5, 6 | syl2anc 693 |
. . . 4
⊢ (𝐴 ∈ ℂ → (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))) |
8 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
9 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
10 | 9 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
11 | | simpr 477 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈
ℂ) |
12 | | mulcl 10020 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 𝑤) ∈ ℂ) |
13 | 8, 10, 11, 12 | fvmptd 6288 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤) = (𝐴 · 𝑤)) |
14 | 13 | fveq2d 6195 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(sin‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤)) = (sin‘(𝐴 · 𝑤))) |
15 | 14 | mpteq2dva 4744 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
(sin‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (sin‘(𝐴 · 𝑤)))) |
16 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝐴 · 𝑤) = (𝐴 · 𝑦)) |
17 | 16 | fveq2d 6195 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (sin‘(𝐴 · 𝑤)) = (sin‘(𝐴 · 𝑦))) |
18 | 17 | cbvmptv 4750 |
. . . . 5
⊢ (𝑤 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) |
20 | 7, 15, 19 | 3eqtrrd 2661 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) = (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) |
21 | 20 | oveq2d 6666 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (ℂ D (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))))) |
22 | | cnelprrecn 10029 |
. . . 4
⊢ ℂ
∈ {ℝ, ℂ} |
23 | 22 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
24 | | dvsin 23745 |
. . . . . 6
⊢ (ℂ
D sin) = cos |
25 | 24 | dmeqi 5325 |
. . . . 5
⊢ dom
(ℂ D sin) = dom cos |
26 | | cosf 14855 |
. . . . . 6
⊢
cos:ℂ⟶ℂ |
27 | 26 | fdmi 6052 |
. . . . 5
⊢ dom cos =
ℂ |
28 | 25, 27 | eqtri 2644 |
. . . 4
⊢ dom
(ℂ D sin) = ℂ |
29 | 28 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → dom
(ℂ D sin) = ℂ) |
30 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) |
31 | 30 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦ 𝑦) = (𝑤 ∈ ℂ ↦ 𝑤) |
32 | 31 | oveq2i 6661 |
. . . . . . . . 9
⊢ ((ℂ
× {𝐴})
∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 ·
(𝑤 ∈ ℂ ↦
𝑤)) |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 ·
(𝑤 ∈ ℂ ↦
𝑤))) |
34 | | cnex 10017 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
35 | 34 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → ℂ
∈ V) |
36 | | snex 4908 |
. . . . . . . . . . 11
⊢ {𝐴} ∈ V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → {𝐴} ∈ V) |
38 | | xpexg 6960 |
. . . . . . . . . 10
⊢ ((ℂ
∈ V ∧ {𝐴} ∈
V) → (ℂ × {𝐴}) ∈ V) |
39 | 35, 37, 38 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}) ∈
V) |
40 | 34 | mptex 6486 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) |
42 | | offval3 7162 |
. . . . . . . . 9
⊢
(((ℂ × {𝐴}) ∈ V ∧ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) → ((ℂ × {𝐴}) ∘𝑓
· (𝑤 ∈ ℂ
↦ 𝑤)) = (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
43 | 39, 41, 42 | syl2anc 693 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘𝑓 · (𝑤 ∈ ℂ ↦ 𝑤)) = (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
44 | | fconst6g 6094 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}):ℂ⟶ℂ) |
45 | | fdm 6051 |
. . . . . . . . . . . . 13
⊢ ((ℂ
× {𝐴}):ℂ⟶ℂ → dom
(ℂ × {𝐴}) =
ℂ) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → dom
(ℂ × {𝐴}) =
ℂ) |
47 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤) |
48 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ → 𝑤 ∈
ℂ) |
49 | 47, 48 | fmpti 6383 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ ↦ 𝑤):ℂ⟶ℂ |
50 | 49 | fdmi 6052 |
. . . . . . . . . . . . 13
⊢ dom
(𝑤 ∈ ℂ ↦
𝑤) =
ℂ |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ ℂ ↦
𝑤) =
ℂ) |
52 | 46, 51 | ineq12d 3815 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (𝑤 ∈ ℂ
↦ 𝑤)) = (ℂ
∩ ℂ)) |
53 | | inidm 3822 |
. . . . . . . . . . . 12
⊢ (ℂ
∩ ℂ) = ℂ |
54 | 53 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (ℂ
∩ ℂ) = ℂ) |
55 | 52, 54 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (𝑤 ∈ ℂ
↦ 𝑤)) =
ℂ) |
56 | 55 | mpteq1d 4738 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
57 | | fvconst2g 6467 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((ℂ × {𝐴})‘𝑦) = 𝐴) |
58 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤)) |
59 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧ 𝑤 = 𝑦) → 𝑤 = 𝑦) |
60 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
61 | 58, 59, 60, 60 | fvmptd 6288 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦) |
62 | 61 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦) |
63 | 57, 62 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)) = (𝐴 · 𝑦)) |
64 | 63 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
65 | 56, 64 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
66 | 33, 43, 65 | 3eqtrrd 2661 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 ·
(𝑦 ∈ ℂ ↦
𝑦))) |
67 | 66 | oveq2d 6666 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (ℂ D ((ℂ
× {𝐴})
∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)))) |
68 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ 𝑦) = (𝑦 ∈ ℂ ↦ 𝑦) |
69 | 68, 60 | fmpti 6383 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ |
70 | 69 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ) |
71 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
72 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
73 | 72 | dvmptid 23720 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
(𝑦 ∈ ℂ ↦
1)) |
74 | 73 | trud 1493 |
. . . . . . . . . 10
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1) |
75 | 74 | dmeqi 5325 |
. . . . . . . . 9
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) = dom
(𝑦 ∈ ℂ ↦
1) |
76 | | ax-1cn 9994 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
77 | 76 | rgenw 2924 |
. . . . . . . . . . 11
⊢
∀𝑦 ∈
ℂ 1 ∈ ℂ |
78 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ ↦ 1) =
(𝑦 ∈ ℂ ↦
1) |
79 | 78 | fmpt 6381 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
ℂ 1 ∈ ℂ ↔ (𝑦 ∈ ℂ ↦
1):ℂ⟶ℂ) |
80 | 77, 79 | mpbi 220 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦
1):ℂ⟶ℂ |
81 | 80 | fdmi 6052 |
. . . . . . . . 9
⊢ dom
(𝑦 ∈ ℂ ↦
1) = ℂ |
82 | 75, 81 | eqtri 2644 |
. . . . . . . 8
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
ℂ |
83 | 82 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
ℂ) |
84 | 23, 70, 71, 83 | dvcmulf 23708 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D ((ℂ × {𝐴})
∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦))) = ((ℂ × {𝐴}) ∘𝑓 ·
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))) |
85 | 67, 84 | eqtrd 2656 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = ((ℂ × {𝐴}) ∘𝑓
· (ℂ D (𝑦
∈ ℂ ↦ 𝑦)))) |
86 | 85 | dmeqd 5326 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) = dom ((ℂ
× {𝐴})
∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)))) |
87 | | ovexd 6680 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) ∈
V) |
88 | | offval3 7162 |
. . . . . 6
⊢
(((ℂ × {𝐴}) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) ∈ V) → ((ℂ
× {𝐴})
∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
89 | 39, 87, 88 | syl2anc 693 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
90 | 89 | dmeqd 5326 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
((ℂ × {𝐴})
∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = dom (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
91 | 46, 83 | ineq12d 3815 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (ℂ D (𝑦 ∈
ℂ ↦ 𝑦))) =
(ℂ ∩ ℂ)) |
92 | 91, 54 | eqtrd 2656 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (ℂ D (𝑦 ∈
ℂ ↦ 𝑦))) =
ℂ) |
93 | 92 | mpteq1d 4738 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (ℂ D
(𝑦 ∈ ℂ ↦
𝑦))) ↦ (((ℂ
× {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
94 | 93 | dmeqd 5326 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ (dom (ℂ
× {𝐴}) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))
↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = dom (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
95 | | eqid 2622 |
. . . . . 6
⊢ (𝑤 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) |
96 | | fvconst2g 6467 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ × {𝐴})‘𝑤) = 𝐴) |
97 | 74 | fveq1i 6192 |
. . . . . . . . . . 11
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤) |
98 | 97 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ → ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤)) |
99 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ → (𝑦 ∈ ℂ ↦ 1) =
(𝑦 ∈ ℂ ↦
1)) |
100 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℂ ∧ 𝑦 = 𝑤) → 1 = 1) |
101 | 76 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ → 1 ∈
ℂ) |
102 | 99, 100, 48, 101 | fvmptd 6288 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ → ((𝑦 ∈ ℂ ↦
1)‘𝑤) =
1) |
103 | 98, 102 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℂ → ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = 1) |
104 | 103 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D (𝑦 ∈
ℂ ↦ 𝑦))‘𝑤) = 1) |
105 | 96, 104 | oveq12d 6668 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) = (𝐴 · 1)) |
106 | | mulcl 10020 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 ·
1) ∈ ℂ) |
107 | 76, 106 | mpan2 707 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) ∈
ℂ) |
108 | 107 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 1) ∈
ℂ) |
109 | 105, 108 | eqeltrd 2701 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) ∈ ℂ) |
110 | 95, 109 | dmmptd 6024 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ) |
111 | 94, 110 | eqtrd 2656 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ (dom (ℂ
× {𝐴}) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))
↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ) |
112 | 86, 90, 111 | 3eqtrd 2660 |
. . 3
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) =
ℂ) |
113 | 23, 23, 2, 5, 29, 112 | dvcof 23711 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (sin ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∘𝑓
· (ℂ D (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))))) |
114 | 24 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D sin) = cos) |
115 | | coscn 24199 |
. . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) |
116 | 115 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → cos
∈ (ℂ–cn→ℂ)) |
117 | 114, 116 | eqeltrd 2701 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D sin) ∈ (ℂ–cn→ℂ)) |
118 | 34 | mptex 6486 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V |
119 | 118 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) |
120 | | coexg 7117 |
. . . . 5
⊢
(((ℂ D sin) ∈ (ℂ–cn→ℂ) ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) → ((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) ∈ V) |
121 | 117, 119,
120 | syl2anc 693 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((ℂ
D sin) ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) ∈
V) |
122 | | ovexd 6680 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) ∈ V) |
123 | | offval3 7162 |
. . . 4
⊢
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V) → (((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∘𝑓
· (ℂ D (𝑦
∈ ℂ ↦ (𝐴
· 𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
124 | 121, 122,
123 | syl2anc 693 |
. . 3
⊢ (𝐴 ∈ ℂ →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘𝑓 ·
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
125 | | frn 6053 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ → ran (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ⊆ ℂ) |
126 | 5, 125 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆
ℂ) |
127 | 126, 29 | sseqtr4d 3642 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆ dom (ℂ D
sin)) |
128 | | dmcosseq 5387 |
. . . . . . . 8
⊢ (ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆ dom (ℂ D sin)
→ dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
129 | 127, 128 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
130 | | ovex 6678 |
. . . . . . . . 9
⊢ (𝐴 · 𝑦) ∈ V |
131 | 130, 4 | dmmpti 6023 |
. . . . . . . 8
⊢ dom
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) = ℂ |
132 | 131 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) = ℂ) |
133 | 129, 132 | eqtrd 2656 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) =
ℂ) |
134 | 133, 112 | ineq12d 3815 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (ℂ ∩
ℂ)) |
135 | 134, 54 | eqtrd 2656 |
. . . 4
⊢ (𝐴 ∈ ℂ → (dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) =
ℂ) |
136 | 135 | mpteq1d 4738 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ (dom ((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
137 | 12 | coscld 14861 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(cos‘(𝐴 ·
𝑤)) ∈
ℂ) |
138 | | simpl 473 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝐴 ∈
ℂ) |
139 | 137, 138 | mulcomd 10061 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((cos‘(𝐴 ·
𝑤)) · 𝐴) = (𝐴 · (cos‘(𝐴 · 𝑤)))) |
140 | 139 | mpteq2dva 4744 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((cos‘(𝐴 ·
𝑤)) · 𝐴)) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))) |
141 | 24 | coeq1i 5281 |
. . . . . . . . 9
⊢ ((ℂ
D sin) ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) = (cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
142 | 141 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) = (cos
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))) |
143 | 142 | fveq1d 6193 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) |
144 | | ffun 6048 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ → Fun (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
145 | 5, 144 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) |
146 | 145 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) |
147 | 11, 131 | syl6eleqr 2712 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
148 | | fvco 6274 |
. . . . . . . 8
⊢ ((Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ∧ 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) → ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) |
149 | 146, 147,
148 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((cos
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) |
150 | 13 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(cos‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤)) = (cos‘(𝐴 · 𝑤))) |
151 | 143, 149,
150 | 3eqtrd 2660 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘(𝐴 · 𝑤))) |
152 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
153 | | 0cnd 10033 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 0 ∈
ℂ) |
154 | 23, 71 | dvmptc 23721 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝐴)) = (𝑦 ∈ ℂ ↦ 0)) |
155 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
156 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 1 ∈
ℂ) |
157 | 74 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1)) |
158 | 23, 152, 153, 154, 155, 156, 157 | dvmptmul 23724 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ ((0 · 𝑦) + (1 · 𝐴)))) |
159 | 155 | mul02d 10234 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0
· 𝑦) =
0) |
160 | 152 | mulid2d 10058 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1
· 𝐴) = 𝐴) |
161 | 159, 160 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = (0 + 𝐴)) |
162 | 152 | addid2d 10237 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 +
𝐴) = 𝐴) |
163 | 161, 162 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = 𝐴) |
164 | 163 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ ((0
· 𝑦) + (1 ·
𝐴))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
165 | 158, 164 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
166 | 165 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
167 | | eqidd 2623 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐴) |
168 | 166, 167,
11, 138 | fvmptd 6288 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))‘𝑤) = 𝐴) |
169 | 151, 168 | oveq12d 6668 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) = ((cos‘(𝐴 · 𝑤)) · 𝐴)) |
170 | 169 | mpteq2dva 4744 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((cos‘(𝐴 · 𝑤)) · 𝐴))) |
171 | 9 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑤))) |
172 | 171 | oveq2d 6666 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝐴 · (cos‘(𝐴 · 𝑦))) = (𝐴 · (cos‘(𝐴 · 𝑤)))) |
173 | 172 | cbvmptv 4750 |
. . . . 5
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤)))) |
174 | 173 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))) |
175 | 140, 170,
174 | 3eqtr4d 2666 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
176 | 124, 136,
175 | 3eqtrd 2660 |
. 2
⊢ (𝐴 ∈ ℂ →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘𝑓 ·
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
177 | 21, 113, 176 | 3eqtrd 2660 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |