Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvsinax Structured version   Visualization version   GIF version

Theorem dvsinax 40445
 Description: Derivative exercise: the derivative with respect to y of sin(Ay), given a constant 𝐴. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
dvsinax (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))))
Distinct variable group:   𝑦,𝐴

Proof of Theorem dvsinax
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 sinf 14898 . . . . . 6 sin:ℂ⟶ℂ
21a1i 11 . . . . 5 (𝐴 ∈ ℂ → sin:ℂ⟶ℂ)
3 mulcl 10058 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ)
4 eqid 2651 . . . . . 6 (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))
53, 4fmptd 6425 . . . . 5 (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ)
6 fcompt 6440 . . . . 5 ((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ) → (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))))
72, 5, 6syl2anc 694 . . . 4 (𝐴 ∈ ℂ → (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))))
8 eqidd 2652 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
9 oveq2 6698 . . . . . . . 8 (𝑦 = 𝑤 → (𝐴 · 𝑦) = (𝐴 · 𝑤))
109adantl 481 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → (𝐴 · 𝑦) = (𝐴 · 𝑤))
11 simpr 476 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈ ℂ)
12 mulcl 10058 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 𝑤) ∈ ℂ)
138, 10, 11, 12fvmptd 6327 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤) = (𝐴 · 𝑤))
1413fveq2d 6233 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)) = (sin‘(𝐴 · 𝑤)))
1514mpteq2dva 4777 . . . 4 (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ (sin‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (sin‘(𝐴 · 𝑤))))
16 oveq2 6698 . . . . . . 7 (𝑤 = 𝑦 → (𝐴 · 𝑤) = (𝐴 · 𝑦))
1716fveq2d 6233 . . . . . 6 (𝑤 = 𝑦 → (sin‘(𝐴 · 𝑤)) = (sin‘(𝐴 · 𝑦)))
1817cbvmptv 4783 . . . . 5 (𝑤 ∈ ℂ ↦ (sin‘(𝐴 · 𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))
1918a1i 11 . . . 4 (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ (sin‘(𝐴 · 𝑤))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))))
207, 15, 193eqtrrd 2690 . . 3 (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) = (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))))
2120oveq2d 6706 . 2 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) = (ℂ D (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))))
22 cnelprrecn 10067 . . . 4 ℂ ∈ {ℝ, ℂ}
2322a1i 11 . . 3 (𝐴 ∈ ℂ → ℂ ∈ {ℝ, ℂ})
24 dvsin 23790 . . . . . 6 (ℂ D sin) = cos
2524dmeqi 5357 . . . . 5 dom (ℂ D sin) = dom cos
26 cosf 14899 . . . . . 6 cos:ℂ⟶ℂ
2726fdmi 6090 . . . . 5 dom cos = ℂ
2825, 27eqtri 2673 . . . 4 dom (ℂ D sin) = ℂ
2928a1i 11 . . 3 (𝐴 ∈ ℂ → dom (ℂ D sin) = ℂ)
30 id 22 . . . . . . . . . . 11 (𝑦 = 𝑤𝑦 = 𝑤)
3130cbvmptv 4783 . . . . . . . . . 10 (𝑦 ∈ ℂ ↦ 𝑦) = (𝑤 ∈ ℂ ↦ 𝑤)
3231oveq2i 6701 . . . . . . . . 9 ((ℂ × {𝐴}) ∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 · (𝑤 ∈ ℂ ↦ 𝑤))
3332a1i 11 . . . . . . . 8 (𝐴 ∈ ℂ → ((ℂ × {𝐴}) ∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 · (𝑤 ∈ ℂ ↦ 𝑤)))
34 cnex 10055 . . . . . . . . . . 11 ℂ ∈ V
3534a1i 11 . . . . . . . . . 10 (𝐴 ∈ ℂ → ℂ ∈ V)
36 snex 4938 . . . . . . . . . . 11 {𝐴} ∈ V
3736a1i 11 . . . . . . . . . 10 (𝐴 ∈ ℂ → {𝐴} ∈ V)
38 xpexg 7002 . . . . . . . . . 10 ((ℂ ∈ V ∧ {𝐴} ∈ V) → (ℂ × {𝐴}) ∈ V)
3935, 37, 38syl2anc 694 . . . . . . . . 9 (𝐴 ∈ ℂ → (ℂ × {𝐴}) ∈ V)
4034mptex 6527 . . . . . . . . . 10 (𝑤 ∈ ℂ ↦ 𝑤) ∈ V
4140a1i 11 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) ∈ V)
42 offval3 7204 . . . . . . . . 9 (((ℂ × {𝐴}) ∈ V ∧ (𝑤 ∈ ℂ ↦ 𝑤) ∈ V) → ((ℂ × {𝐴}) ∘𝑓 · (𝑤 ∈ ℂ ↦ 𝑤)) = (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))))
4339, 41, 42syl2anc 694 . . . . . . . 8 (𝐴 ∈ ℂ → ((ℂ × {𝐴}) ∘𝑓 · (𝑤 ∈ ℂ ↦ 𝑤)) = (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))))
44 fconst6g 6132 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (ℂ × {𝐴}):ℂ⟶ℂ)
45 fdm 6089 . . . . . . . . . . . . 13 ((ℂ × {𝐴}):ℂ⟶ℂ → dom (ℂ × {𝐴}) = ℂ)
4644, 45syl 17 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → dom (ℂ × {𝐴}) = ℂ)
47 eqid 2651 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤)
48 id 22 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ → 𝑤 ∈ ℂ)
4947, 48fmpti 6423 . . . . . . . . . . . . . 14 (𝑤 ∈ ℂ ↦ 𝑤):ℂ⟶ℂ
5049fdmi 6090 . . . . . . . . . . . . 13 dom (𝑤 ∈ ℂ ↦ 𝑤) = ℂ
5150a1i 11 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → dom (𝑤 ∈ ℂ ↦ 𝑤) = ℂ)
5246, 51ineq12d 3848 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) = (ℂ ∩ ℂ))
53 inidm 3855 . . . . . . . . . . . 12 (ℂ ∩ ℂ) = ℂ
5453a1i 11 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (ℂ ∩ ℂ) = ℂ)
5552, 54eqtrd 2685 . . . . . . . . . 10 (𝐴 ∈ ℂ → (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) = ℂ)
5655mpteq1d 4771 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))))
57 fvconst2g 6508 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((ℂ × {𝐴})‘𝑦) = 𝐴)
58 eqidd 2652 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → (𝑤 ∈ ℂ ↦ 𝑤) = (𝑤 ∈ ℂ ↦ 𝑤))
59 simpr 476 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ∧ 𝑤 = 𝑦) → 𝑤 = 𝑦)
60 id 22 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
6158, 59, 60, 60fvmptd 6327 . . . . . . . . . . . 12 (𝑦 ∈ ℂ → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦)
6261adantl 481 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦) = 𝑦)
6357, 62oveq12d 6708 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦)) = (𝐴 · 𝑦))
6463mpteq2dva 4777 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
6556, 64eqtrd 2685 . . . . . . . 8 (𝐴 ∈ ℂ → (𝑦 ∈ (dom (ℂ × {𝐴}) ∩ dom (𝑤 ∈ ℂ ↦ 𝑤)) ↦ (((ℂ × {𝐴})‘𝑦) · ((𝑤 ∈ ℂ ↦ 𝑤)‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
6633, 43, 653eqtrrd 2690 . . . . . . 7 (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = ((ℂ × {𝐴}) ∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦)))
6766oveq2d 6706 . . . . . 6 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = (ℂ D ((ℂ × {𝐴}) ∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦))))
68 eqid 2651 . . . . . . . . 9 (𝑦 ∈ ℂ ↦ 𝑦) = (𝑦 ∈ ℂ ↦ 𝑦)
6968, 60fmpti 6423 . . . . . . . 8 (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ
7069a1i 11 . . . . . . 7 (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝑦):ℂ⟶ℂ)
71 id 22 . . . . . . 7 (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
7222a1i 11 . . . . . . . . . . . 12 (⊤ → ℂ ∈ {ℝ, ℂ})
7372dvmptid 23765 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
7473trud 1533 . . . . . . . . . 10 (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1)
7574dmeqi 5357 . . . . . . . . 9 dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = dom (𝑦 ∈ ℂ ↦ 1)
76 ax-1cn 10032 . . . . . . . . . . . 12 1 ∈ ℂ
7776rgenw 2953 . . . . . . . . . . 11 𝑦 ∈ ℂ 1 ∈ ℂ
78 eqid 2651 . . . . . . . . . . . 12 (𝑦 ∈ ℂ ↦ 1) = (𝑦 ∈ ℂ ↦ 1)
7978fmpt 6421 . . . . . . . . . . 11 (∀𝑦 ∈ ℂ 1 ∈ ℂ ↔ (𝑦 ∈ ℂ ↦ 1):ℂ⟶ℂ)
8077, 79mpbi 220 . . . . . . . . . 10 (𝑦 ∈ ℂ ↦ 1):ℂ⟶ℂ
8180fdmi 6090 . . . . . . . . 9 dom (𝑦 ∈ ℂ ↦ 1) = ℂ
8275, 81eqtri 2673 . . . . . . . 8 dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = ℂ
8382a1i 11 . . . . . . 7 (𝐴 ∈ ℂ → dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = ℂ)
8423, 70, 71, 83dvcmulf 23753 . . . . . 6 (𝐴 ∈ ℂ → (ℂ D ((ℂ × {𝐴}) ∘𝑓 · (𝑦 ∈ ℂ ↦ 𝑦))) = ((ℂ × {𝐴}) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))))
8567, 84eqtrd 2685 . . . . 5 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = ((ℂ × {𝐴}) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))))
8685dmeqd 5358 . . . 4 (𝐴 ∈ ℂ → dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = dom ((ℂ × {𝐴}) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))))
87 ovexd 6720 . . . . . 6 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) ∈ V)
88 offval3 7204 . . . . . 6 (((ℂ × {𝐴}) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) ∈ V) → ((ℂ × {𝐴}) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))))
8939, 87, 88syl2anc 694 . . . . 5 (𝐴 ∈ ℂ → ((ℂ × {𝐴}) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))))
9089dmeqd 5358 . . . 4 (𝐴 ∈ ℂ → dom ((ℂ × {𝐴}) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = dom (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))))
9146, 83ineq12d 3848 . . . . . . . 8 (𝐴 ∈ ℂ → (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = (ℂ ∩ ℂ))
9291, 54eqtrd 2685 . . . . . . 7 (𝐴 ∈ ℂ → (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) = ℂ)
9392mpteq1d 4771 . . . . . 6 (𝐴 ∈ ℂ → (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))))
9493dmeqd 5358 . . . . 5 (𝐴 ∈ ℂ → dom (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = dom (𝑤 ∈ ℂ ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))))
95 eqid 2651 . . . . . 6 (𝑤 ∈ ℂ ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = (𝑤 ∈ ℂ ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)))
96 fvconst2g 6508 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((ℂ × {𝐴})‘𝑤) = 𝐴)
9774fveq1i 6230 . . . . . . . . . . 11 ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤)
9897a1i 11 . . . . . . . . . 10 (𝑤 ∈ ℂ → ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤) = ((𝑦 ∈ ℂ ↦ 1)‘𝑤))
99 eqidd 2652 . . . . . . . . . . 11 (𝑤 ∈ ℂ → (𝑦 ∈ ℂ ↦ 1) = (𝑦 ∈ ℂ ↦ 1))
100 eqidd 2652 . . . . . . . . . . 11 ((𝑤 ∈ ℂ ∧ 𝑦 = 𝑤) → 1 = 1)
10176a1i 11 . . . . . . . . . . 11 (𝑤 ∈ ℂ → 1 ∈ ℂ)
10299, 100, 48, 101fvmptd 6327 . . . . . . . . . 10 (𝑤 ∈ ℂ → ((𝑦 ∈ ℂ ↦ 1)‘𝑤) = 1)
10398, 102eqtrd 2685 . . . . . . . . 9 (𝑤 ∈ ℂ → ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤) = 1)
104103adantl 481 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤) = 1)
10596, 104oveq12d 6708 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) = (𝐴 · 1))
106 mulcl 10058 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 · 1) ∈ ℂ)
10776, 106mpan2 707 . . . . . . . 8 (𝐴 ∈ ℂ → (𝐴 · 1) ∈ ℂ)
108107adantr 480 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝐴 · 1) ∈ ℂ)
109105, 108eqeltrd 2730 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤)) ∈ ℂ)
11095, 109dmmptd 6062 . . . . 5 (𝐴 ∈ ℂ → dom (𝑤 ∈ ℂ ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ)
11194, 110eqtrd 2685 . . . 4 (𝐴 ∈ ℂ → dom (𝑤 ∈ (dom (ℂ × {𝐴}) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ 𝑦))) ↦ (((ℂ × {𝐴})‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ 𝑦))‘𝑤))) = ℂ)
11286, 90, 1113eqtrd 2689 . . 3 (𝐴 ∈ ℂ → dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = ℂ)
11323, 23, 2, 5, 29, 112dvcof 23756 . 2 (𝐴 ∈ ℂ → (ℂ D (sin ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) = (((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))))
11424a1i 11 . . . . . 6 (𝐴 ∈ ℂ → (ℂ D sin) = cos)
115 coscn 24244 . . . . . . 7 cos ∈ (ℂ–cn→ℂ)
116115a1i 11 . . . . . 6 (𝐴 ∈ ℂ → cos ∈ (ℂ–cn→ℂ))
117114, 116eqeltrd 2730 . . . . 5 (𝐴 ∈ ℂ → (ℂ D sin) ∈ (ℂ–cn→ℂ))
11834mptex 6527 . . . . . 6 (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V
119118a1i 11 . . . . 5 (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V)
120 coexg 7159 . . . . 5 (((ℂ D sin) ∈ (ℂ–cn→ℂ) ∧ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ V) → ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V)
121117, 119, 120syl2anc 694 . . . 4 (𝐴 ∈ ℂ → ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V)
122 ovexd 6720 . . . 4 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V)
123 offval3 7204 . . . 4 ((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V ∧ (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∈ V) → (((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))))
124121, 122, 123syl2anc 694 . . 3 (𝐴 ∈ ℂ → (((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) = (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))))
125 frn 6091 . . . . . . . . . 10 ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ → ran (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ⊆ ℂ)
1265, 125syl 17 . . . . . . . . 9 (𝐴 ∈ ℂ → ran (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ⊆ ℂ)
127126, 29sseqtr4d 3675 . . . . . . . 8 (𝐴 ∈ ℂ → ran (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ⊆ dom (ℂ D sin))
128 dmcosseq 5419 . . . . . . . 8 (ran (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ⊆ dom (ℂ D sin) → dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
129127, 128syl 17 . . . . . . 7 (𝐴 ∈ ℂ → dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
130 ovex 6718 . . . . . . . . 9 (𝐴 · 𝑦) ∈ V
131130, 4dmmpti 6061 . . . . . . . 8 dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = ℂ
132131a1i 11 . . . . . . 7 (𝐴 ∈ ℂ → dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) = ℂ)
133129, 132eqtrd 2685 . . . . . 6 (𝐴 ∈ ℂ → dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = ℂ)
134133, 112ineq12d 3848 . . . . 5 (𝐴 ∈ ℂ → (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) = (ℂ ∩ ℂ))
135134, 54eqtrd 2685 . . . 4 (𝐴 ∈ ℂ → (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) = ℂ)
136135mpteq1d 4771 . . 3 (𝐴 ∈ ℂ → (𝑤 ∈ (dom ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∩ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) ↦ ((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))))
13712coscld 14905 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (cos‘(𝐴 · 𝑤)) ∈ ℂ)
138 simpl 472 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝐴 ∈ ℂ)
139137, 138mulcomd 10099 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((cos‘(𝐴 · 𝑤)) · 𝐴) = (𝐴 · (cos‘(𝐴 · 𝑤))))
140139mpteq2dva 4777 . . . 4 (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ ((cos‘(𝐴 · 𝑤)) · 𝐴)) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤)))))
14124coeq1i 5314 . . . . . . . . 9 ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = (cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
142141a1i 11 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = (cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))))
143142fveq1d 6231 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))
144 ffun 6086 . . . . . . . . . 10 ((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)):ℂ⟶ℂ → Fun (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
1455, 144syl 17 . . . . . . . . 9 (𝐴 ∈ ℂ → Fun (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
146145adantr 480 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → Fun (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
14711, 131syl6eleqr 2741 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))
148 fvco 6313 . . . . . . . 8 ((Fun (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∧ 𝑤 ∈ dom (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) → ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))
149146, 147, 148syl2anc 694 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((cos ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)))
15013fveq2d 6233 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (cos‘((𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))‘𝑤)) = (cos‘(𝐴 · 𝑤)))
151143, 149, 1503eqtrd 2689 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = (cos‘(𝐴 · 𝑤)))
152 simpl 472 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈ ℂ)
153 0cnd 10071 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
15423, 71dvmptc 23766 . . . . . . . . . 10 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ 𝐴)) = (𝑦 ∈ ℂ ↦ 0))
155 simpr 476 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
15676a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
15774a1i 11 . . . . . . . . . 10 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
15823, 152, 153, 154, 155, 156, 157dvmptmul 23769 . . . . . . . . 9 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ ((0 · 𝑦) + (1 · 𝐴))))
159155mul02d 10272 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 · 𝑦) = 0)
160152mulid2d 10096 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 · 𝐴) = 𝐴)
161159, 160oveq12d 6708 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0 · 𝑦) + (1 · 𝐴)) = (0 + 𝐴))
162152addid2d 10275 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 + 𝐴) = 𝐴)
163161, 162eqtrd 2685 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0 · 𝑦) + (1 · 𝐴)) = 𝐴)
164163mpteq2dva 4777 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ ((0 · 𝑦) + (1 · 𝐴))) = (𝑦 ∈ ℂ ↦ 𝐴))
165158, 164eqtrd 2685 . . . . . . . 8 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴))
166165adantr 480 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴))
167 eqidd 2652 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐴)
168166, 167, 11, 138fvmptd 6327 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) = 𝐴)
169151, 168oveq12d 6708 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ) → ((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤)) = ((cos‘(𝐴 · 𝑤)) · 𝐴))
170169mpteq2dva 4777 . . . 4 (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ ((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑤 ∈ ℂ ↦ ((cos‘(𝐴 · 𝑤)) · 𝐴)))
1719fveq2d 6233 . . . . . . 7 (𝑦 = 𝑤 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑤)))
172171oveq2d 6706 . . . . . 6 (𝑦 = 𝑤 → (𝐴 · (cos‘(𝐴 · 𝑦))) = (𝐴 · (cos‘(𝐴 · 𝑤))))
173172cbvmptv 4783 . . . . 5 (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤))))
174173a1i 11 . . . 4 (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = (𝑤 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑤)))))
175140, 170, 1743eqtr4d 2695 . . 3 (𝐴 ∈ ℂ → (𝑤 ∈ ℂ ↦ ((((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤) · ((ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))‘𝑤))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))))
176124, 136, 1753eqtrd 2689 . 2 (𝐴 ∈ ℂ → (((ℂ D sin) ∘ (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦))) ∘𝑓 · (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))))
17721, 113, 1763eqtrd 2689 1 (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523  ⊤wtru 1524   ∈ wcel 2030  ∀wral 2941  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607  {csn 4210  {cpr 4212   ↦ cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144   ∘ ccom 5147  Fun wfun 5920  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ∘𝑓 cof 6937  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  sincsin 14838  cosccos 14839  –cn→ccncf 22726   D cdv 23672 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676 This theorem is referenced by:  dvasinbx  40453  itgcoscmulx  40503  dirkeritg  40637  dirkercncflem2  40639
 Copyright terms: Public domain W3C validator