Step | Hyp | Ref
| Expression |
1 | | sinf 15562 |
. . . . . 6
⊢
sin:ℂ⟶ℂ |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
sin:ℂ⟶ℂ) |
3 | | mulcl 10692 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
4 | 3 | fmpttd 6883 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) |
5 | | fcompt 6899 |
. . . . 5
⊢
((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) → (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))) |
6 | 2, 4, 5 | syl2anc 587 |
. . . 4
⊢ (𝐴 ∈ ℂ → (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))) |
7 | | eqidd 2739 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
8 | | oveq2 7172 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
9 | 8 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
10 | | simpr 488 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈
ℂ) |
11 | | mulcl 10692 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 𝑤) ∈ ℂ) |
12 | 7, 9, 10, 11 | fvmptd 6776 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤) = (𝐴 · 𝑤)) |
13 | 12 | fveq2d 6672 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(sin‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤)) = (sin‘(𝐴 · 𝑤))) |
14 | 13 | mpteq2dva 5122 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
(sin‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (sin‘(𝐴 · 𝑤)))) |
15 | | oveq2 7172 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝐴 · 𝑤) = (𝐴 · 𝑦)) |
16 | 15 | fveq2d 6672 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (sin‘(𝐴 · 𝑤)) = (sin‘(𝐴 · 𝑦))) |
17 | 16 | cbvmptv 5130 |
. . . . 5
⊢ (𝑤 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) |
18 | 17 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) |
19 | 6, 14, 18 | 3eqtrrd 2778 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) = (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) |
20 | 19 | oveq2d 7180 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (ℂ D (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))))) |
21 | | cnelprrecn 10701 |
. . . 4
⊢ ℂ
∈ {ℝ, ℂ} |
22 | 21 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
23 | | dvsin 24726 |
. . . . . 6
⊢ (ℂ
D sin) = cos |
24 | 23 | dmeqi 5741 |
. . . . 5
⊢ dom
(ℂ D sin) = dom cos |
25 | | cosf 15563 |
. . . . . 6
⊢
cos:ℂ⟶ℂ |
26 | 25 | fdmi 6510 |
. . . . 5
⊢ dom cos =
ℂ |
27 | 24, 26 | eqtri 2761 |
. . . 4
⊢ dom
(ℂ D sin) = ℂ |
28 | 27 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → dom
(ℂ D sin) = ℂ) |
29 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) |
30 | 29 | cbvmptv 5130 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦ 𝑦) = (𝑤 ∈ ℂ ↦ 𝑤) |
31 | 30 | oveq2i 7175 |
. . . . . . . . 9
⊢ ((ℂ
× {𝐴})
∘f · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘f · (𝑤 ∈ ℂ ↦ 𝑤)) |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘f · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘f · (𝑤 ∈ ℂ ↦ 𝑤))) |
33 | | cnex 10689 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → ℂ
∈ V) |
35 | | snex 5295 |
. . . . . . . . . . 11
⊢ {𝐴} ∈ V |
36 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → {𝐴} ∈ V) |
37 | 34, 36 | xpexd 7486 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}) ∈
V) |
38 | 33 | mptex 6990 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V |
39 | 38 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) |
40 | | offval3 7701 |
. . . . . . . . 9
⊢
(((ℂ × {𝐴}) ∈ V ∧ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) → ((ℂ × {𝐴}) ∘f ·
(𝑤 ∈ ℂ ↦
𝑤)) = (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
41 | 37, 39, 40 | syl2anc 587 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘f · (𝑤 ∈ ℂ ↦ 𝑤)) = (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
42 | | fconst6g 6561 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}):ℂ⟶ℂ) |
43 | 42 | fdmd 6509 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → dom
(ℂ × {𝐴}) =
ℂ) |
44 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤) |
45 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ → 𝑤 ∈
ℂ) |
46 | 44, 45 | fmpti 6880 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ ↦ 𝑤):ℂ⟶ℂ |
47 | 46 | fdmi 6510 |
. . . . . . . . . . . . 13
⊢ dom
(𝑤 ∈ ℂ ↦
𝑤) =
ℂ |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ ℂ ↦
𝑤) =
ℂ) |
49 | 43, 48 | ineq12d 4102 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (𝑤 ∈ ℂ
↦ 𝑤)) = (ℂ
∩ ℂ)) |
50 | | inidm 4107 |
. . . . . . . . . . . 12
⊢ (ℂ
∩ ℂ) = ℂ |
51 | 50 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (ℂ
∩ ℂ) = ℂ) |
52 | 49, 51 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (𝑤 ∈ ℂ
↦ 𝑤)) =
ℂ) |
53 | 52 | mpteq1d 5116 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
54 | | fvconst2g 6968 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((ℂ × {𝐴})‘𝑦) = 𝐴) |
55 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤)) |
56 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧ 𝑤 = 𝑦) → 𝑤 = 𝑦) |
57 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
58 | 55, 56, 57, 57 | fvmptd 6776 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦) |
59 | 58 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦) |
60 | 54, 59 | oveq12d 7182 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)) = (𝐴 · 𝑦)) |
61 | 60 | mpteq2dva 5122 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
62 | 53, 61 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
63 | 32, 41, 62 | 3eqtrrd 2778 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = ((ℂ × {𝐴}) ∘f · (𝑦 ∈ ℂ ↦ 𝑦))) |
64 | 63 | oveq2d 7180 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (ℂ D ((ℂ
× {𝐴})
∘f · (𝑦 ∈ ℂ ↦ 𝑦)))) |
65 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ 𝑦) = (𝑦 ∈ ℂ ↦ 𝑦) |
66 | 65, 57 | fmpti 6880 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ |
67 | 66 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ) |
68 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
69 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
70 | 69 | dvmptid 24701 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
(𝑦 ∈ ℂ ↦
1)) |
71 | 70 | mptru 1549 |
. . . . . . . . . 10
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1) |
72 | 71 | dmeqi 5741 |
. . . . . . . . 9
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) = dom
(𝑦 ∈ ℂ ↦
1) |
73 | | ax-1cn 10666 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
74 | 73 | rgenw 3065 |
. . . . . . . . . . 11
⊢
∀𝑦 ∈
ℂ 1 ∈ ℂ |
75 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ ↦ 1) =
(𝑦 ∈ ℂ ↦
1) |
76 | 75 | fmpt 6878 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
ℂ 1 ∈ ℂ ↔ (𝑦 ∈ ℂ ↦
1):ℂ⟶ℂ) |
77 | 74, 76 | mpbi 233 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦
1):ℂ⟶ℂ |
78 | 77 | fdmi 6510 |
. . . . . . . . 9
⊢ dom
(𝑦 ∈ ℂ ↦
1) = ℂ |
79 | 72, 78 | eqtri 2761 |
. . . . . . . 8
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
ℂ |
80 | 79 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
ℂ) |
81 | 22, 67, 68, 80 | dvcmulf 24689 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D ((ℂ × {𝐴})
∘f · (𝑦 ∈ ℂ ↦ 𝑦))) = ((ℂ × {𝐴}) ∘f · (ℂ D
(𝑦 ∈ ℂ ↦
𝑦)))) |
82 | 64, 81 | eqtrd 2773 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = ((ℂ × {𝐴}) ∘f ·
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))) |
83 | 82 | dmeqd 5742 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) = dom ((ℂ
× {𝐴})
∘f · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)))) |
84 | | ovexd 7199 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) ∈
V) |
85 | | offval3 7701 |
. . . . . 6
⊢
(((ℂ × {𝐴}) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) ∈ V) → ((ℂ
× {𝐴})
∘f · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
86 | 37, 84, 85 | syl2anc 587 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘f · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
87 | 86 | dmeqd 5742 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
((ℂ × {𝐴})
∘f · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = dom (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
88 | 43, 80 | ineq12d 4102 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (ℂ D (𝑦 ∈
ℂ ↦ 𝑦))) =
(ℂ ∩ ℂ)) |
89 | 88, 51 | eqtrd 2773 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (ℂ D (𝑦 ∈
ℂ ↦ 𝑦))) =
ℂ) |
90 | 89 | mpteq1d 5116 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (ℂ D
(𝑦 ∈ ℂ ↦
𝑦))) ↦ (((ℂ
× {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
91 | 90 | dmeqd 5742 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ (dom (ℂ
× {𝐴}) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))
↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = dom (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
92 | | eqid 2738 |
. . . . . 6
⊢ (𝑤 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) |
93 | | fvconst2g 6968 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ × {𝐴})‘𝑤) = 𝐴) |
94 | 71 | fveq1i 6669 |
. . . . . . . . . . 11
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤) |
95 | 94 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ → ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤)) |
96 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ → (𝑦 ∈ ℂ ↦ 1) =
(𝑦 ∈ ℂ ↦
1)) |
97 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℂ ∧ 𝑦 = 𝑤) → 1 = 1) |
98 | 73 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ → 1 ∈
ℂ) |
99 | 96, 97, 45, 98 | fvmptd 6776 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ → ((𝑦 ∈ ℂ ↦
1)‘𝑤) =
1) |
100 | 95, 99 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℂ → ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = 1) |
101 | 100 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D (𝑦 ∈
ℂ ↦ 𝑦))‘𝑤) = 1) |
102 | 93, 101 | oveq12d 7182 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) = (𝐴 · 1)) |
103 | | mulcl 10692 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 ·
1) ∈ ℂ) |
104 | 73, 103 | mpan2 691 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) ∈
ℂ) |
105 | 104 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 1) ∈
ℂ) |
106 | 102, 105 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) ∈ ℂ) |
107 | 92, 106 | dmmptd 6476 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ) |
108 | 91, 107 | eqtrd 2773 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ (dom (ℂ
× {𝐴}) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))
↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ) |
109 | 83, 87, 108 | 3eqtrd 2777 |
. . 3
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) =
ℂ) |
110 | 22, 22, 2, 4, 28, 109 | dvcof 24692 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (sin ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∘f ·
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))))) |
111 | 23 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D sin) = cos) |
112 | | coscn 25184 |
. . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) |
113 | 112 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → cos
∈ (ℂ–cn→ℂ)) |
114 | 111, 113 | eqeltrd 2833 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D sin) ∈ (ℂ–cn→ℂ)) |
115 | 33 | mptex 6990 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V |
116 | 115 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) |
117 | | coexg 7653 |
. . . . 5
⊢
(((ℂ D sin) ∈ (ℂ–cn→ℂ) ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) → ((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) ∈ V) |
118 | 114, 116,
117 | syl2anc 587 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((ℂ
D sin) ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) ∈
V) |
119 | | ovexd 7199 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) ∈ V) |
120 | | offval3 7701 |
. . . 4
⊢
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V) → (((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∘f ·
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
121 | 118, 119,
120 | syl2anc 587 |
. . 3
⊢ (𝐴 ∈ ℂ →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘f · (ℂ D
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
122 | 4 | frnd 6506 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆
ℂ) |
123 | 122, 28 | sseqtrrd 3916 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆ dom (ℂ D
sin)) |
124 | | dmcosseq 5810 |
. . . . . . . 8
⊢ (ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆ dom (ℂ D sin)
→ dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
125 | 123, 124 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
126 | | ovex 7197 |
. . . . . . . . 9
⊢ (𝐴 · 𝑦) ∈ V |
127 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) |
128 | 126, 127 | dmmpti 6475 |
. . . . . . . 8
⊢ dom
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) = ℂ |
129 | 128 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) = ℂ) |
130 | 125, 129 | eqtrd 2773 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) =
ℂ) |
131 | 130, 109 | ineq12d 4102 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (ℂ ∩
ℂ)) |
132 | 131, 51 | eqtrd 2773 |
. . . 4
⊢ (𝐴 ∈ ℂ → (dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) =
ℂ) |
133 | 132 | mpteq1d 5116 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ (dom ((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
134 | 11 | coscld 15569 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(cos‘(𝐴 ·
𝑤)) ∈
ℂ) |
135 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝐴 ∈
ℂ) |
136 | 134, 135 | mulcomd 10733 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((cos‘(𝐴 ·
𝑤)) · 𝐴) = (𝐴 · (cos‘(𝐴 · 𝑤)))) |
137 | 136 | mpteq2dva 5122 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((cos‘(𝐴 ·
𝑤)) · 𝐴)) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))) |
138 | 23 | coeq1i 5696 |
. . . . . . . . 9
⊢ ((ℂ
D sin) ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) = (cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
139 | 138 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) = (cos
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))) |
140 | 139 | fveq1d 6670 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) |
141 | 4 | ffund 6502 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) |
142 | 141 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) |
143 | 10, 128 | eleqtrrdi 2844 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
144 | | fvco 6760 |
. . . . . . . 8
⊢ ((Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ∧ 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) → ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) |
145 | 142, 143,
144 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((cos
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) |
146 | 12 | fveq2d 6672 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(cos‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤)) = (cos‘(𝐴 · 𝑤))) |
147 | 140, 145,
146 | 3eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘(𝐴 · 𝑤))) |
148 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
149 | | 0cnd 10705 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 0 ∈
ℂ) |
150 | 22, 68 | dvmptc 24702 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝐴)) = (𝑦 ∈ ℂ ↦ 0)) |
151 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
152 | 73 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 1 ∈
ℂ) |
153 | 71 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1)) |
154 | 22, 148, 149, 150, 151, 152, 153 | dvmptmul 24705 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ ((0 · 𝑦) + (1 · 𝐴)))) |
155 | 151 | mul02d 10909 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0
· 𝑦) =
0) |
156 | 148 | mulid2d 10730 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1
· 𝐴) = 𝐴) |
157 | 155, 156 | oveq12d 7182 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = (0 + 𝐴)) |
158 | 148 | addid2d 10912 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 +
𝐴) = 𝐴) |
159 | 157, 158 | eqtrd 2773 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = 𝐴) |
160 | 159 | mpteq2dva 5122 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ ((0
· 𝑦) + (1 ·
𝐴))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
161 | 154, 160 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
162 | 161 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
163 | | eqidd 2739 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐴) |
164 | 162, 163,
10, 135 | fvmptd 6776 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))‘𝑤) = 𝐴) |
165 | 147, 164 | oveq12d 7182 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) = ((cos‘(𝐴 · 𝑤)) · 𝐴)) |
166 | 165 | mpteq2dva 5122 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((cos‘(𝐴 · 𝑤)) · 𝐴))) |
167 | 8 | fveq2d 6672 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑤))) |
168 | 167 | oveq2d 7180 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝐴 · (cos‘(𝐴 · 𝑦))) = (𝐴 · (cos‘(𝐴 · 𝑤)))) |
169 | 168 | cbvmptv 5130 |
. . . . 5
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤)))) |
170 | 169 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))) |
171 | 137, 166,
170 | 3eqtr4d 2783 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
172 | 121, 133,
171 | 3eqtrd 2777 |
. 2
⊢ (𝐴 ∈ ℂ →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘f · (ℂ D
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
173 | 20, 110, 172 | 3eqtrd 2777 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |