| Step | Hyp | Ref
| Expression |
| 1 | | sinf 16160 |
. . . . . 6
⊢
sin:ℂ⟶ℂ |
| 2 | 1 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
sin:ℂ⟶ℂ) |
| 3 | | mulcl 11239 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
| 4 | 3 | fmpttd 7135 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) |
| 5 | | fcompt 7153 |
. . . . 5
⊢
((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) → (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))) |
| 6 | 2, 4, 5 | syl2anc 584 |
. . . 4
⊢ (𝐴 ∈ ℂ → (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))) |
| 7 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
| 8 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
| 9 | 8 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
| 10 | | simpr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈
ℂ) |
| 11 | | mulcl 11239 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 𝑤) ∈ ℂ) |
| 12 | 7, 9, 10, 11 | fvmptd 7023 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤) = (𝐴 · 𝑤)) |
| 13 | 12 | fveq2d 6910 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(sin‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤)) = (sin‘(𝐴 · 𝑤))) |
| 14 | 13 | mpteq2dva 5242 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
(sin‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (sin‘(𝐴 · 𝑤)))) |
| 15 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝐴 · 𝑤) = (𝐴 · 𝑦)) |
| 16 | 15 | fveq2d 6910 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (sin‘(𝐴 · 𝑤)) = (sin‘(𝐴 · 𝑦))) |
| 17 | 16 | cbvmptv 5255 |
. . . . 5
⊢ (𝑤 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) |
| 18 | 17 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) |
| 19 | 6, 14, 18 | 3eqtrrd 2782 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) = (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) |
| 20 | 19 | oveq2d 7447 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (ℂ D (sin
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))))) |
| 21 | | cnelprrecn 11248 |
. . . 4
⊢ ℂ
∈ {ℝ, ℂ} |
| 22 | 21 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
| 23 | | dvsin 26020 |
. . . . . 6
⊢ (ℂ
D sin) = cos |
| 24 | 23 | dmeqi 5915 |
. . . . 5
⊢ dom
(ℂ D sin) = dom cos |
| 25 | | cosf 16161 |
. . . . . 6
⊢
cos:ℂ⟶ℂ |
| 26 | 25 | fdmi 6747 |
. . . . 5
⊢ dom cos =
ℂ |
| 27 | 24, 26 | eqtri 2765 |
. . . 4
⊢ dom
(ℂ D sin) = ℂ |
| 28 | 27 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → dom
(ℂ D sin) = ℂ) |
| 29 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) |
| 30 | 29 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦ 𝑦) = (𝑤 ∈ ℂ ↦ 𝑤) |
| 31 | 30 | oveq2i 7442 |
. . . . . . . . 9
⊢ ((ℂ
× {𝐴})
∘f · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘f · (𝑤 ∈ ℂ ↦ 𝑤)) |
| 32 | 31 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘f · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘f · (𝑤 ∈ ℂ ↦ 𝑤))) |
| 33 | | cnex 11236 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
| 34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → ℂ
∈ V) |
| 35 | | snex 5436 |
. . . . . . . . . . 11
⊢ {𝐴} ∈ V |
| 36 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → {𝐴} ∈ V) |
| 37 | 34, 36 | xpexd 7771 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}) ∈
V) |
| 38 | 33 | mptex 7243 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V |
| 39 | 38 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) |
| 40 | | offval3 8007 |
. . . . . . . . 9
⊢
(((ℂ × {𝐴}) ∈ V ∧ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) → ((ℂ × {𝐴}) ∘f ·
(𝑤 ∈ ℂ ↦
𝑤)) = (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
| 41 | 37, 39, 40 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘f · (𝑤 ∈ ℂ ↦ 𝑤)) = (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
| 42 | | fconst6g 6797 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}):ℂ⟶ℂ) |
| 43 | 42 | fdmd 6746 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → dom
(ℂ × {𝐴}) =
ℂ) |
| 44 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤) |
| 45 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ → 𝑤 ∈
ℂ) |
| 46 | 44, 45 | fmpti 7132 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ ↦ 𝑤):ℂ⟶ℂ |
| 47 | 46 | fdmi 6747 |
. . . . . . . . . . . . 13
⊢ dom
(𝑤 ∈ ℂ ↦
𝑤) =
ℂ |
| 48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ ℂ ↦
𝑤) =
ℂ) |
| 49 | 43, 48 | ineq12d 4221 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (𝑤 ∈ ℂ
↦ 𝑤)) = (ℂ
∩ ℂ)) |
| 50 | | inidm 4227 |
. . . . . . . . . . . 12
⊢ (ℂ
∩ ℂ) = ℂ |
| 51 | 50 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (ℂ
∩ ℂ) = ℂ) |
| 52 | 49, 51 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (𝑤 ∈ ℂ
↦ 𝑤)) =
ℂ) |
| 53 | 52 | mpteq1d 5237 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)))) |
| 54 | | fvconst2g 7222 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((ℂ × {𝐴})‘𝑦) = 𝐴) |
| 55 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤)) |
| 56 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧ 𝑤 = 𝑦) → 𝑤 = 𝑦) |
| 57 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
| 58 | 55, 56, 57, 57 | fvmptd 7023 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦) |
| 59 | 58 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦) |
| 60 | 54, 59 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)) = (𝐴 · 𝑦)) |
| 61 | 60 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
| 62 | 53, 61 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ ×
{𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
| 63 | 32, 41, 62 | 3eqtrrd 2782 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = ((ℂ × {𝐴}) ∘f · (𝑦 ∈ ℂ ↦ 𝑦))) |
| 64 | 63 | oveq2d 7447 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (ℂ D ((ℂ
× {𝐴})
∘f · (𝑦 ∈ ℂ ↦ 𝑦)))) |
| 65 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ 𝑦) = (𝑦 ∈ ℂ ↦ 𝑦) |
| 66 | 65, 57 | fmpti 7132 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ |
| 67 | 66 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ) |
| 68 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
| 69 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 70 | 69 | dvmptid 25995 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
(𝑦 ∈ ℂ ↦
1)) |
| 71 | 70 | mptru 1547 |
. . . . . . . . . 10
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1) |
| 72 | 71 | dmeqi 5915 |
. . . . . . . . 9
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) = dom
(𝑦 ∈ ℂ ↦
1) |
| 73 | | ax-1cn 11213 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
| 74 | 73 | rgenw 3065 |
. . . . . . . . . . 11
⊢
∀𝑦 ∈
ℂ 1 ∈ ℂ |
| 75 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ ↦ 1) =
(𝑦 ∈ ℂ ↦
1) |
| 76 | 75 | fmpt 7130 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
ℂ 1 ∈ ℂ ↔ (𝑦 ∈ ℂ ↦
1):ℂ⟶ℂ) |
| 77 | 74, 76 | mpbi 230 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦
1):ℂ⟶ℂ |
| 78 | 77 | fdmi 6747 |
. . . . . . . . 9
⊢ dom
(𝑦 ∈ ℂ ↦
1) = ℂ |
| 79 | 72, 78 | eqtri 2765 |
. . . . . . . 8
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
ℂ |
| 80 | 79 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
ℂ) |
| 81 | 22, 67, 68, 80 | dvcmulf 25982 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D ((ℂ × {𝐴})
∘f · (𝑦 ∈ ℂ ↦ 𝑦))) = ((ℂ × {𝐴}) ∘f · (ℂ D
(𝑦 ∈ ℂ ↦
𝑦)))) |
| 82 | 64, 81 | eqtrd 2777 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = ((ℂ × {𝐴}) ∘f ·
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))) |
| 83 | 82 | dmeqd 5916 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) = dom ((ℂ
× {𝐴})
∘f · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)))) |
| 84 | | ovexd 7466 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) ∈
V) |
| 85 | | offval3 8007 |
. . . . . 6
⊢
(((ℂ × {𝐴}) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) ∈ V) → ((ℂ
× {𝐴})
∘f · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
| 86 | 37, 84, 85 | syl2anc 584 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝐴})
∘f · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
| 87 | 86 | dmeqd 5916 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
((ℂ × {𝐴})
∘f · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = dom (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
| 88 | 43, 80 | ineq12d 4221 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (ℂ D (𝑦 ∈
ℂ ↦ 𝑦))) =
(ℂ ∩ ℂ)) |
| 89 | 88, 51 | eqtrd 2777 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (dom
(ℂ × {𝐴}) ∩
dom (ℂ D (𝑦 ∈
ℂ ↦ 𝑦))) =
ℂ) |
| 90 | 89 | mpteq1d 5237 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ (dom (ℂ ×
{𝐴}) ∩ dom (ℂ D
(𝑦 ∈ ℂ ↦
𝑦))) ↦ (((ℂ
× {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
| 91 | 90 | dmeqd 5916 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ (dom (ℂ
× {𝐴}) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))
↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = dom (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))) |
| 92 | | eqid 2737 |
. . . . . 6
⊢ (𝑤 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ ×
{𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) |
| 93 | | fvconst2g 7222 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ × {𝐴})‘𝑤) = 𝐴) |
| 94 | 71 | fveq1i 6907 |
. . . . . . . . . . 11
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤) |
| 95 | 94 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ → ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤)) |
| 96 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ → (𝑦 ∈ ℂ ↦ 1) =
(𝑦 ∈ ℂ ↦
1)) |
| 97 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℂ ∧ 𝑦 = 𝑤) → 1 = 1) |
| 98 | 73 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ → 1 ∈
ℂ) |
| 99 | 96, 97, 45, 98 | fvmptd 7023 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℂ → ((𝑦 ∈ ℂ ↦
1)‘𝑤) =
1) |
| 100 | 95, 99 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℂ → ((ℂ
D (𝑦 ∈ ℂ ↦
𝑦))‘𝑤) = 1) |
| 101 | 100 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D (𝑦 ∈
ℂ ↦ 𝑦))‘𝑤) = 1) |
| 102 | 93, 101 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) = (𝐴 · 1)) |
| 103 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 ·
1) ∈ ℂ) |
| 104 | 73, 103 | mpan2 691 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) ∈
ℂ) |
| 105 | 104 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 1) ∈
ℂ) |
| 106 | 102, 105 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) ∈ ℂ) |
| 107 | 92, 106 | dmmptd 6713 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ ℂ ↦
(((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ) |
| 108 | 91, 107 | eqtrd 2777 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(𝑤 ∈ (dom (ℂ
× {𝐴}) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ 𝑦)))
↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ) |
| 109 | 83, 87, 108 | 3eqtrd 2781 |
. . 3
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) =
ℂ) |
| 110 | 22, 22, 2, 4, 28, 109 | dvcof 25986 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (sin ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∘f ·
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))))) |
| 111 | 23 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D sin) = cos) |
| 112 | | coscn 26489 |
. . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) |
| 113 | 112 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → cos
∈ (ℂ–cn→ℂ)) |
| 114 | 111, 113 | eqeltrd 2841 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D sin) ∈ (ℂ–cn→ℂ)) |
| 115 | 33 | mptex 7243 |
. . . . . 6
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V |
| 116 | 115 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) |
| 117 | | coexg 7951 |
. . . . 5
⊢
(((ℂ D sin) ∈ (ℂ–cn→ℂ) ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) → ((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) ∈ V) |
| 118 | 114, 116,
117 | syl2anc 584 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((ℂ
D sin) ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) ∈
V) |
| 119 | | ovexd 7466 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) ∈ V) |
| 120 | | offval3 8007 |
. . . 4
⊢
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V) → (((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∘f ·
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
| 121 | 118, 119,
120 | syl2anc 584 |
. . 3
⊢ (𝐴 ∈ ℂ →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘f · (ℂ D
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
| 122 | 4 | frnd 6744 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆
ℂ) |
| 123 | 122, 28 | sseqtrrd 4021 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆ dom (ℂ D
sin)) |
| 124 | | dmcosseq 5987 |
. . . . . . . 8
⊢ (ran
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ⊆ dom (ℂ D sin)
→ dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
| 125 | 123, 124 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
| 126 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝐴 · 𝑦) ∈ V |
| 127 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) |
| 128 | 126, 127 | dmmpti 6712 |
. . . . . . . 8
⊢ dom
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) = ℂ |
| 129 | 128 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) = ℂ) |
| 130 | 125, 129 | eqtrd 2777 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) =
ℂ) |
| 131 | 130, 109 | ineq12d 4221 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) = (ℂ ∩
ℂ)) |
| 132 | 131, 51 | eqtrd 2777 |
. . . 4
⊢ (𝐴 ∈ ℂ → (dom
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) ∩ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))) =
ℂ) |
| 133 | 132 | mpteq1d 5237 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ (dom ((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((((ℂ D sin)
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)))) |
| 134 | 11 | coscld 16167 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(cos‘(𝐴 ·
𝑤)) ∈
ℂ) |
| 135 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝐴 ∈
ℂ) |
| 136 | 134, 135 | mulcomd 11282 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((cos‘(𝐴 ·
𝑤)) · 𝐴) = (𝐴 · (cos‘(𝐴 · 𝑤)))) |
| 137 | 136 | mpteq2dva 5242 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((cos‘(𝐴 ·
𝑤)) · 𝐴)) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))) |
| 138 | 23 | coeq1i 5870 |
. . . . . . . . 9
⊢ ((ℂ
D sin) ∘ (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))) = (cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
| 139 | 138 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D sin) ∘ (𝑦
∈ ℂ ↦ (𝐴
· 𝑦))) = (cos
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))) |
| 140 | 139 | fveq1d 6908 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) |
| 141 | 4 | ffund 6740 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) |
| 142 | 141 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) |
| 143 | 10, 128 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) |
| 144 | | fvco 7007 |
. . . . . . . 8
⊢ ((Fun
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)) ∧ 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) → ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) |
| 145 | 142, 143,
144 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((cos
∘ (𝑦 ∈ ℂ
↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) |
| 146 | 12 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(cos‘((𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦))‘𝑤)) = (cos‘(𝐴 · 𝑤))) |
| 147 | 140, 145,
146 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘(𝐴 · 𝑤))) |
| 148 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
| 149 | | 0cnd 11254 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 0 ∈
ℂ) |
| 150 | 22, 68 | dvmptc 25996 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝐴)) = (𝑦 ∈ ℂ ↦ 0)) |
| 151 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
| 152 | 73 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 1 ∈
ℂ) |
| 153 | 71 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1)) |
| 154 | 22, 148, 149, 150, 151, 152, 153 | dvmptmul 25999 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ ((0 · 𝑦) + (1 · 𝐴)))) |
| 155 | 151 | mul02d 11459 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0
· 𝑦) =
0) |
| 156 | 148 | mullidd 11279 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1
· 𝐴) = 𝐴) |
| 157 | 155, 156 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = (0 + 𝐴)) |
| 158 | 148 | addlidd 11462 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 +
𝐴) = 𝐴) |
| 159 | 157, 158 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = 𝐴) |
| 160 | 159 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ ((0
· 𝑦) + (1 ·
𝐴))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
| 161 | 154, 160 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
| 162 | 161 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
| 163 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐴) |
| 164 | 162, 163,
10, 135 | fvmptd 7023 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((ℂ D (𝑦 ∈
ℂ ↦ (𝐴 ·
𝑦)))‘𝑤) = 𝐴) |
| 165 | 147, 164 | oveq12d 7449 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) = ((cos‘(𝐴 · 𝑤)) · 𝐴)) |
| 166 | 165 | mpteq2dva 5242 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((cos‘(𝐴 · 𝑤)) · 𝐴))) |
| 167 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑤))) |
| 168 | 167 | oveq2d 7447 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝐴 · (cos‘(𝐴 · 𝑦))) = (𝐴 · (cos‘(𝐴 · 𝑤)))) |
| 169 | 168 | cbvmptv 5255 |
. . . . 5
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤)))) |
| 170 | 169 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))) |
| 171 | 137, 166,
170 | 3eqtr4d 2787 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦
((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
| 172 | 121, 133,
171 | 3eqtrd 2781 |
. 2
⊢ (𝐴 ∈ ℂ →
(((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘f · (ℂ D
(𝑦 ∈ ℂ ↦
(𝐴 · 𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
| 173 | 20, 110, 172 | 3eqtrd 2781 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |