Step | Hyp | Ref
| Expression |
1 | | sinf 14693 |
. . . . . 6
⊢
sin:ℂ⟶ℂ |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
sin:ℂ⟶ℂ) |
3 | | mulcl 9899 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
4 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) |
5 | 3, 4 | fmptd 6292 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) |
6 | | fcompt 6306 |
. . . . 5
⊢
((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) → (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))) |
7 | 2, 5, 6 | syl2anc 691 |
. . . 4
⊢ (𝐴 ∈ ℂ → (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))) |
8 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
9 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
10 | 9 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
11 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈
ℂ) |
12 | | mulcl 9899 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 𝑤) ∈ ℂ) |
13 | 8, 10, 11, 12 | fvmptd 6197 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤) = (𝐴 · 𝑤)) |
14 | 13 | fveq2d 6107 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(sin‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤)) = (sin‘(𝐴 · 𝑤))) |
15 | 14 | mpteq2dva 4672 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
(sin‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (sin‘(𝐴 · 𝑤)))) |
16 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝐴 · 𝑤) = (𝐴 · 𝑦)) |
17 | 16 | fveq2d 6107 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (sin‘(𝐴 · 𝑤)) = (sin‘(𝐴 · 𝑦))) |
18 | 17 | cbvmptv 4678 |
. . . . 5
⊢ (𝑤 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) |
20 | 7, 15, 19 | 3eqtrrd 2649 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) = (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) |
21 | 20 | oveq2d 6565 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (ℂ D (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))))) |
22 | | cnelprrecn 9908 |
. . . 4
⊢ ℂ
∈ {ℝ, ℂ} |
23 | 22 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
24 | | dvsin 23549 |
. . . . . 6
⊢ (ℂ
D sin) = cos |
25 | 24 | dmeqi 5247 |
. . . . 5
⊢ dom
(ℂ D sin) = dom cos |
26 | | cosf 14694 |
. . . . . 6
⊢
cos:ℂ⟶ℂ |
27 | 26 | fdmi 5965 |
. . . . 5
⊢ dom cos =
ℂ |
28 | 25, 27 | eqtri 2632 |
. . . 4
⊢ dom
(ℂ D sin) = ℂ |
29 | 28 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → dom
(ℂ D sin) = ℂ) |
30 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) |
31 | 30 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦ 𝑦) = (𝑤 ∈ ℂ ↦ 𝑤) |
32 | 31 | oveq2i 6560 |
. . . . . . . . 9
⊢ ((ℂ
× {𝐴})
∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 ·
(𝑤 ∈ ℂ ↦
𝑤)) |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 ·
(𝑤 ∈ ℂ ↦
𝑤))) |
34 | | cnex 9896 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
35 | 34 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → ℂ
∈ V) |
36 | | snex 4835 |
. . . . . . . . . . 11
⊢ {𝐴} ∈ V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → {𝐴} ∈ V) |
38 | | xpexg 6858 |
. . . . . . . . . 10
⊢ ((ℂ
∈ V ∧ {𝐴} ∈
V) → (ℂ × {𝐴}) ∈ V) |
39 | 35, 37, 38 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}) ∈
V) |
40 | 34 | mptex 6390 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) |
42 | | offval3 7053 |
. . . . . . . . 9
⊢
(((ℂ × {𝐴}) ∈ V ∧ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) → ((ℂ × {𝐴}) ∘𝑓
· (𝑤 ∈ ℂ
↦ 𝑤)) = (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
43 | 39, 41, 42 | syl2anc 691 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘𝑓 · (𝑤 ∈ ℂ ↦ 𝑤)) = (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
44 | | fconst6g 6007 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}):ℂ⟶ℂ) |
45 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ ((ℂ
× {𝐴}):ℂ⟶ℂ → dom
(ℂ × {𝐴}) =
ℂ) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → dom
(ℂ × {𝐴}) =
ℂ) |
47 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤) |
48 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ → 𝑤 ∈
ℂ) |
49 | 47, 48 | fmpti 6291 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ ↦ 𝑤):ℂ⟶ℂ |
50 | 49 | fdmi 5965 |
. . . . . . . . . . . . 13
⊢ dom
(𝑤 ∈ ℂ ↦
𝑤) =
ℂ |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ ℂ ↦
𝑤) =
ℂ) |
52 | 46, 51 | ineq12d 3777 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (𝑤 ∈ ℂ
↦ 𝑤)) = (ℂ
∩ ℂ)) |
53 | | inidm 3784 |
. . . . . . . . . . . 12
⊢ (ℂ
∩ ℂ) = ℂ |
54 | 53 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (ℂ
∩ ℂ) = ℂ) |
55 | 52, 54 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (𝑤 ∈ ℂ
↦ 𝑤)) =
ℂ) |
56 | 55 | mpteq1d 4666 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
57 | | fvconst2g 6372 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((ℂ × {𝐴})‘𝑦) = 𝐴) |
58 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤)) |
59 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧ 𝑤 = 𝑦) → 𝑤 = 𝑦) |
60 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
61 | 58, 59, 60, 60 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦) |
62 | 61 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦) |
63 | 57, 62 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)) = (𝐴 · 𝑦)) |
64 | 63 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
65 | 56, 64 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
66 | 33, 43, 65 | 3eqtrrd 2649 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 ·
(𝑦 ∈ ℂ ↦
𝑦))) |
67 | 66 | oveq2d 6565 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (ℂ D ((ℂ
× {𝐴})
∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)))) |
68 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ 𝑦) = (𝑦 ∈ ℂ ↦ 𝑦) |
69 | 68, 60 | fmpti 6291 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ |
70 | 69 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ) |
71 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
72 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
73 | 72 | dvmptid 23526 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
(𝑦 ∈ ℂ ↦
1)) |
74 | 73 | trud 1484 |
. . . . . . . . . 10
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1) |
75 | 74 | dmeqi 5247 |
. . . . . . . . 9
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) = dom
(𝑦 ∈ ℂ ↦
1) |
76 | | ax-1cn 9873 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
77 | 76 | rgenw 2908 |
. . . . . . . . . . 11
⊢
∀𝑦 ∈
ℂ 1 ∈ ℂ |
78 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ ↦ 1) =
(𝑦 ∈ ℂ ↦
1) |
79 | 78 | fmpt 6289 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
ℂ 1 ∈ ℂ ↔ (𝑦 ∈ ℂ ↦
1):ℂ⟶ℂ) |
80 | 77, 79 | mpbi 219 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦
1):ℂ⟶ℂ |
81 | 80 | fdmi 5965 |
. . . . . . . . 9
⊢ dom
(𝑦 ∈ ℂ ↦
1) = ℂ |
82 | 75, 81 | eqtri 2632 |
. . . . . . . 8
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
ℂ |
83 | 82 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
ℂ) |
84 | 23, 70, 71, 83 | dvcmulf 23514 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D ((ℂ × {𝐴})
∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦))) = ((ℂ × {𝐴}) ∘𝑓 ·
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))) |
85 | 67, 84 | eqtrd 2644 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = ((ℂ × {𝐴}) ∘𝑓
· (ℂ D (𝑦
∈ ℂ ↦ 𝑦)))) |
86 | 85 | dmeqd 5248 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) = dom ((ℂ
× {𝐴})
∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)))) |
87 | | ovex 6577 |
. . . . . . 7
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) ∈
V |
88 | 87 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) ∈
V) |
89 | | offval3 7053 |
. . . . . 6
⊢
(((ℂ × {𝐴}) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) ∈ V) → ((ℂ
× {𝐴})
∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
90 | 39, 88, 89 | syl2anc 691 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
91 | 90 | dmeqd 5248 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
((ℂ × {𝐴})
∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = dom (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
92 | 46, 83 | ineq12d 3777 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (ℂ D (𝑦 ∈
ℂ ↦ 𝑦))) =
(ℂ ∩ ℂ)) |
93 | 92, 54 | eqtrd 2644 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (ℂ D (𝑦 ∈
ℂ ↦ 𝑦))) =
ℂ) |
94 | 93 | mpteq1d 4666 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (ℂ D
(𝑦 ∈ ℂ ↦
𝑦))) ↦ (((ℂ
× {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
95 | 94 | dmeqd 5248 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ (dom (ℂ
× {𝐴}) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))
↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = dom (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
96 | | eqid 2610 |
. . . . . 6
⊢ (𝑤 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) |
97 | | fvconst2g 6372 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ × {𝐴})‘𝑤) = 𝐴) |
98 | 74 | fveq1i 6104 |
. . . . . . . . . . 11
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤) |
99 | 98 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ → ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤)) |
100 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ → (𝑦 ∈ ℂ ↦ 1) =
(𝑦 ∈ ℂ ↦
1)) |
101 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℂ ∧ 𝑦 = 𝑤) → 1 = 1) |
102 | 76 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ → 1 ∈
ℂ) |
103 | 100, 101,
48, 102 | fvmptd 6197 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ → ((𝑦 ∈ ℂ ↦
1)‘𝑤) =
1) |
104 | 99, 103 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℂ → ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = 1) |
105 | 104 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D (𝑦 ∈
ℂ ↦ 𝑦))‘𝑤) = 1) |
106 | 97, 105 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) = (𝐴 · 1)) |
107 | | mulcl 9899 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 ·
1) ∈ ℂ) |
108 | 76, 107 | mpan2 703 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) ∈
ℂ) |
109 | 108 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 1) ∈
ℂ) |
110 | 106, 109 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) ∈ ℂ) |
111 | 96, 110 | dmmptd 5937 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ) |
112 | 95, 111 | eqtrd 2644 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ (dom (ℂ
× {𝐴}) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))
↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ) |
113 | 86, 91, 112 | 3eqtrd 2648 |
. . 3
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) =
ℂ) |
114 | 23, 23, 2, 5, 29, 113 | dvcof 23517 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (sin ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∘𝑓
· (ℂ D (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))))) |
115 | 24 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D sin) = cos) |
116 | | coscn 24003 |
. . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) |
117 | 116 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → cos
∈ (ℂ–cn→ℂ)) |
118 | 115, 117 | eqeltrd 2688 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D sin) ∈ (ℂ–cn→ℂ)) |
119 | 34 | mptex 6390 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V |
120 | 119 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) |
121 | | coexg 7010 |
. . . . 5
⊢
(((ℂ D sin) ∈ (ℂ–cn→ℂ) ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) → ((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) ∈ V) |
122 | 118, 120,
121 | syl2anc 691 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((ℂ
D sin) ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) ∈
V) |
123 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
124 | | 0cnd 9912 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 0 ∈
ℂ) |
125 | 23, 71 | dvmptc 23527 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝐴)) = (𝑦 ∈ ℂ ↦ 0)) |
126 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
127 | 76 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 1 ∈
ℂ) |
128 | 74 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1)) |
129 | 23, 123, 124, 125, 126, 127, 128 | dvmptmul 23530 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ ((0 · 𝑦) + (1 · 𝐴)))) |
130 | 126 | mul02d 10113 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0
· 𝑦) =
0) |
131 | 123 | mulid2d 9937 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1
· 𝐴) = 𝐴) |
132 | 130, 131 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = (0 + 𝐴)) |
133 | 123 | addid2d 10116 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 +
𝐴) = 𝐴) |
134 | 132, 133 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = 𝐴) |
135 | 134 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ ((0
· 𝑦) + (1 ·
𝐴))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
136 | 129, 135 | eqtrd 2644 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
137 | 34 | mptex 6390 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↦ 𝐴) ∈ V |
138 | 137 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝐴) ∈ V) |
139 | 136, 138 | eqeltrd 2688 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) ∈ V) |
140 | | offval3 7053 |
. . . 4
⊢
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V) → (((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∘𝑓
· (ℂ D (𝑦
∈ ℂ ↦ (𝐴
· 𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
141 | 122, 139,
140 | syl2anc 691 |
. . 3
⊢ (𝐴 ∈ ℂ →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘𝑓 ·
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
142 | | frn 5966 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ → ran (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ⊆ ℂ) |
143 | 5, 142 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆
ℂ) |
144 | 143, 29 | sseqtr4d 3605 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆ dom (ℂ D
sin)) |
145 | | dmcosseq 5308 |
. . . . . . . 8
⊢ (ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆ dom (ℂ D sin)
→ dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
146 | 144, 145 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
147 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝐴 · 𝑦) ∈ V |
148 | 147, 4 | dmmpti 5936 |
. . . . . . . 8
⊢ dom
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) = ℂ |
149 | 148 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) = ℂ) |
150 | 146, 149 | eqtrd 2644 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) =
ℂ) |
151 | 150, 113 | ineq12d 3777 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (ℂ ∩
ℂ)) |
152 | 151, 54 | eqtrd 2644 |
. . . 4
⊢ (𝐴 ∈ ℂ → (dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) =
ℂ) |
153 | 152 | mpteq1d 4666 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ (dom ((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
154 | 12 | coscld 14700 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(cos‘(𝐴 ·
𝑤)) ∈
ℂ) |
155 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝐴 ∈
ℂ) |
156 | 154, 155 | mulcomd 9940 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((cos‘(𝐴 ·
𝑤)) · 𝐴) = (𝐴 · (cos‘(𝐴 · 𝑤)))) |
157 | 156 | mpteq2dva 4672 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((cos‘(𝐴 ·
𝑤)) · 𝐴)) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))) |
158 | 24 | coeq1i 5203 |
. . . . . . . . 9
⊢ ((ℂ
D sin) ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) = (cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
159 | 158 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) = (cos
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))) |
160 | 159 | fveq1d 6105 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) |
161 | | ffun 5961 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ → Fun (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
162 | 5, 161 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) |
163 | 162 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) |
164 | 11, 148 | syl6eleqr 2699 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
165 | | fvco 6184 |
. . . . . . . 8
⊢ ((Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ∧ 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) → ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) |
166 | 163, 164,
165 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((cos
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) |
167 | 13 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(cos‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤)) = (cos‘(𝐴 · 𝑤))) |
168 | 160, 166,
167 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘(𝐴 · 𝑤))) |
169 | 136 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
170 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐴) |
171 | 169, 170,
11, 155 | fvmptd 6197 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))‘𝑤) = 𝐴) |
172 | 168, 171 | oveq12d 6567 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) = ((cos‘(𝐴 · 𝑤)) · 𝐴)) |
173 | 172 | mpteq2dva 4672 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((cos‘(𝐴 · 𝑤)) · 𝐴))) |
174 | 9 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑤))) |
175 | 174 | oveq2d 6565 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝐴 · (cos‘(𝐴 · 𝑦))) = (𝐴 · (cos‘(𝐴 · 𝑤)))) |
176 | 175 | cbvmptv 4678 |
. . . . 5
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤)))) |
177 | 176 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))) |
178 | 157, 173,
177 | 3eqtr4d 2654 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
179 | 141, 153,
178 | 3eqtrd 2648 |
. 2
⊢ (𝐴 ∈ ℂ →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘𝑓 ·
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
180 | 21, 114, 179 | 3eqtrd 2648 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |