Step | Hyp | Ref
| Expression |
1 | | sinf 16063 |
. . . . . 6
β’
sin:ββΆβ |
2 | 1 | a1i 11 |
. . . . 5
β’ (π΄ β β β
sin:ββΆβ) |
3 | | mulcl 11190 |
. . . . . 6
β’ ((π΄ β β β§ π¦ β β) β (π΄ Β· π¦) β β) |
4 | 3 | fmpttd 7111 |
. . . . 5
β’ (π΄ β β β (π¦ β β β¦ (π΄ Β· π¦)):ββΆβ) |
5 | | fcompt 7127 |
. . . . 5
β’
((sin:ββΆβ β§ (π¦ β β β¦ (π΄ Β· π¦)):ββΆβ) β (sin
β (π¦ β β
β¦ (π΄ Β· π¦))) = (π€ β β β¦ (sinβ((π¦ β β β¦ (π΄ Β· π¦))βπ€)))) |
6 | 2, 4, 5 | syl2anc 584 |
. . . 4
β’ (π΄ β β β (sin
β (π¦ β β
β¦ (π΄ Β· π¦))) = (π€ β β β¦ (sinβ((π¦ β β β¦ (π΄ Β· π¦))βπ€)))) |
7 | | eqidd 2733 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β (π¦ β β β¦ (π΄ Β· π¦)) = (π¦ β β β¦ (π΄ Β· π¦))) |
8 | | oveq2 7413 |
. . . . . . . 8
β’ (π¦ = π€ β (π΄ Β· π¦) = (π΄ Β· π€)) |
9 | 8 | adantl 482 |
. . . . . . 7
β’ (((π΄ β β β§ π€ β β) β§ π¦ = π€) β (π΄ Β· π¦) = (π΄ Β· π€)) |
10 | | simpr 485 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β π€ β
β) |
11 | | mulcl 11190 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β (π΄ Β· π€) β β) |
12 | 7, 9, 10, 11 | fvmptd 7002 |
. . . . . 6
β’ ((π΄ β β β§ π€ β β) β ((π¦ β β β¦ (π΄ Β· π¦))βπ€) = (π΄ Β· π€)) |
13 | 12 | fveq2d 6892 |
. . . . 5
β’ ((π΄ β β β§ π€ β β) β
(sinβ((π¦ β
β β¦ (π΄ Β·
π¦))βπ€)) = (sinβ(π΄ Β· π€))) |
14 | 13 | mpteq2dva 5247 |
. . . 4
β’ (π΄ β β β (π€ β β β¦
(sinβ((π¦ β
β β¦ (π΄ Β·
π¦))βπ€))) = (π€ β β β¦ (sinβ(π΄ Β· π€)))) |
15 | | oveq2 7413 |
. . . . . . 7
β’ (π€ = π¦ β (π΄ Β· π€) = (π΄ Β· π¦)) |
16 | 15 | fveq2d 6892 |
. . . . . 6
β’ (π€ = π¦ β (sinβ(π΄ Β· π€)) = (sinβ(π΄ Β· π¦))) |
17 | 16 | cbvmptv 5260 |
. . . . 5
β’ (π€ β β β¦
(sinβ(π΄ Β·
π€))) = (π¦ β β β¦ (sinβ(π΄ Β· π¦))) |
18 | 17 | a1i 11 |
. . . 4
β’ (π΄ β β β (π€ β β β¦
(sinβ(π΄ Β·
π€))) = (π¦ β β β¦ (sinβ(π΄ Β· π¦)))) |
19 | 6, 14, 18 | 3eqtrrd 2777 |
. . 3
β’ (π΄ β β β (π¦ β β β¦
(sinβ(π΄ Β·
π¦))) = (sin β (π¦ β β β¦ (π΄ Β· π¦)))) |
20 | 19 | oveq2d 7421 |
. 2
β’ (π΄ β β β (β
D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) = (β D (sin
β (π¦ β β
β¦ (π΄ Β· π¦))))) |
21 | | cnelprrecn 11199 |
. . . 4
β’ β
β {β, β} |
22 | 21 | a1i 11 |
. . 3
β’ (π΄ β β β β
β {β, β}) |
23 | | dvsin 25490 |
. . . . . 6
β’ (β
D sin) = cos |
24 | 23 | dmeqi 5902 |
. . . . 5
β’ dom
(β D sin) = dom cos |
25 | | cosf 16064 |
. . . . . 6
β’
cos:ββΆβ |
26 | 25 | fdmi 6726 |
. . . . 5
β’ dom cos =
β |
27 | 24, 26 | eqtri 2760 |
. . . 4
β’ dom
(β D sin) = β |
28 | 27 | a1i 11 |
. . 3
β’ (π΄ β β β dom
(β D sin) = β) |
29 | | id 22 |
. . . . . . . . . . 11
β’ (π¦ = π€ β π¦ = π€) |
30 | 29 | cbvmptv 5260 |
. . . . . . . . . 10
β’ (π¦ β β β¦ π¦) = (π€ β β β¦ π€) |
31 | 30 | oveq2i 7416 |
. . . . . . . . 9
β’ ((β
Γ {π΄})
βf Β· (π¦ β β β¦ π¦)) = ((β Γ {π΄}) βf Β· (π€ β β β¦ π€)) |
32 | 31 | a1i 11 |
. . . . . . . 8
β’ (π΄ β β β ((β
Γ {π΄})
βf Β· (π¦ β β β¦ π¦)) = ((β Γ {π΄}) βf Β· (π€ β β β¦ π€))) |
33 | | cnex 11187 |
. . . . . . . . . . 11
β’ β
β V |
34 | 33 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ β β β β
β V) |
35 | | snex 5430 |
. . . . . . . . . . 11
β’ {π΄} β V |
36 | 35 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ β β β {π΄} β V) |
37 | 34, 36 | xpexd 7734 |
. . . . . . . . 9
β’ (π΄ β β β (β
Γ {π΄}) β
V) |
38 | 33 | mptex 7221 |
. . . . . . . . . 10
β’ (π€ β β β¦ π€) β V |
39 | 38 | a1i 11 |
. . . . . . . . 9
β’ (π΄ β β β (π€ β β β¦ π€) β V) |
40 | | offval3 7965 |
. . . . . . . . 9
β’
(((β Γ {π΄}) β V β§ (π€ β β β¦ π€) β V) β ((β Γ {π΄}) βf Β·
(π€ β β β¦
π€)) = (π¦ β (dom (β Γ {π΄}) β© dom (π€ β β β¦ π€)) β¦ (((β Γ {π΄})βπ¦) Β· ((π€ β β β¦ π€)βπ¦)))) |
41 | 37, 39, 40 | syl2anc 584 |
. . . . . . . 8
β’ (π΄ β β β ((β
Γ {π΄})
βf Β· (π€ β β β¦ π€)) = (π¦ β (dom (β Γ {π΄}) β© dom (π€ β β β¦ π€)) β¦ (((β Γ {π΄})βπ¦) Β· ((π€ β β β¦ π€)βπ¦)))) |
42 | | fconst6g 6777 |
. . . . . . . . . . . . 13
β’ (π΄ β β β (β
Γ {π΄}):ββΆβ) |
43 | 42 | fdmd 6725 |
. . . . . . . . . . . 12
β’ (π΄ β β β dom
(β Γ {π΄}) =
β) |
44 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ (π€ β β β¦ π€) = (π€ β β β¦ π€) |
45 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π€ β β β π€ β
β) |
46 | 44, 45 | fmpti 7108 |
. . . . . . . . . . . . . 14
β’ (π€ β β β¦ π€):ββΆβ |
47 | 46 | fdmi 6726 |
. . . . . . . . . . . . 13
β’ dom
(π€ β β β¦
π€) =
β |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
β’ (π΄ β β β dom
(π€ β β β¦
π€) =
β) |
49 | 43, 48 | ineq12d 4212 |
. . . . . . . . . . 11
β’ (π΄ β β β (dom
(β Γ {π΄}) β©
dom (π€ β β
β¦ π€)) = (β
β© β)) |
50 | | inidm 4217 |
. . . . . . . . . . . 12
β’ (β
β© β) = β |
51 | 50 | a1i 11 |
. . . . . . . . . . 11
β’ (π΄ β β β (β
β© β) = β) |
52 | 49, 51 | eqtrd 2772 |
. . . . . . . . . 10
β’ (π΄ β β β (dom
(β Γ {π΄}) β©
dom (π€ β β
β¦ π€)) =
β) |
53 | 52 | mpteq1d 5242 |
. . . . . . . . 9
β’ (π΄ β β β (π¦ β (dom (β Γ
{π΄}) β© dom (π€ β β β¦ π€)) β¦ (((β Γ
{π΄})βπ¦) Β· ((π€ β β β¦ π€)βπ¦))) = (π¦ β β β¦ (((β Γ
{π΄})βπ¦) Β· ((π€ β β β¦ π€)βπ¦)))) |
54 | | fvconst2g 7199 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π¦ β β) β
((β Γ {π΄})βπ¦) = π΄) |
55 | | eqidd 2733 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π€ β β β¦ π€) = (π€ β β β¦ π€)) |
56 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((π¦ β β β§ π€ = π¦) β π€ = π¦) |
57 | | id 22 |
. . . . . . . . . . . . 13
β’ (π¦ β β β π¦ β
β) |
58 | 55, 56, 57, 57 | fvmptd 7002 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((π€ β β β¦ π€)βπ¦) = π¦) |
59 | 58 | adantl 482 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π¦ β β) β ((π€ β β β¦ π€)βπ¦) = π¦) |
60 | 54, 59 | oveq12d 7423 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β β) β
(((β Γ {π΄})βπ¦) Β· ((π€ β β β¦ π€)βπ¦)) = (π΄ Β· π¦)) |
61 | 60 | mpteq2dva 5247 |
. . . . . . . . 9
β’ (π΄ β β β (π¦ β β β¦
(((β Γ {π΄})βπ¦) Β· ((π€ β β β¦ π€)βπ¦))) = (π¦ β β β¦ (π΄ Β· π¦))) |
62 | 53, 61 | eqtrd 2772 |
. . . . . . . 8
β’ (π΄ β β β (π¦ β (dom (β Γ
{π΄}) β© dom (π€ β β β¦ π€)) β¦ (((β Γ
{π΄})βπ¦) Β· ((π€ β β β¦ π€)βπ¦))) = (π¦ β β β¦ (π΄ Β· π¦))) |
63 | 32, 41, 62 | 3eqtrrd 2777 |
. . . . . . 7
β’ (π΄ β β β (π¦ β β β¦ (π΄ Β· π¦)) = ((β Γ {π΄}) βf Β· (π¦ β β β¦ π¦))) |
64 | 63 | oveq2d 7421 |
. . . . . 6
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = (β D ((β
Γ {π΄})
βf Β· (π¦ β β β¦ π¦)))) |
65 | | eqid 2732 |
. . . . . . . . 9
β’ (π¦ β β β¦ π¦) = (π¦ β β β¦ π¦) |
66 | 65, 57 | fmpti 7108 |
. . . . . . . 8
β’ (π¦ β β β¦ π¦):ββΆβ |
67 | 66 | a1i 11 |
. . . . . . 7
β’ (π΄ β β β (π¦ β β β¦ π¦):ββΆβ) |
68 | | id 22 |
. . . . . . 7
β’ (π΄ β β β π΄ β
β) |
69 | 21 | a1i 11 |
. . . . . . . . . . . 12
β’ (β€
β β β {β, β}) |
70 | 69 | dvmptid 25465 |
. . . . . . . . . . 11
β’ (β€
β (β D (π¦ β
β β¦ π¦)) =
(π¦ β β β¦
1)) |
71 | 70 | mptru 1548 |
. . . . . . . . . 10
β’ (β
D (π¦ β β β¦
π¦)) = (π¦ β β β¦ 1) |
72 | 71 | dmeqi 5902 |
. . . . . . . . 9
β’ dom
(β D (π¦ β
β β¦ π¦)) = dom
(π¦ β β β¦
1) |
73 | | ax-1cn 11164 |
. . . . . . . . . . . 12
β’ 1 β
β |
74 | 73 | rgenw 3065 |
. . . . . . . . . . 11
β’
βπ¦ β
β 1 β β |
75 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (π¦ β β β¦ 1) =
(π¦ β β β¦
1) |
76 | 75 | fmpt 7106 |
. . . . . . . . . . 11
β’
(βπ¦ β
β 1 β β β (π¦ β β β¦
1):ββΆβ) |
77 | 74, 76 | mpbi 229 |
. . . . . . . . . 10
β’ (π¦ β β β¦
1):ββΆβ |
78 | 77 | fdmi 6726 |
. . . . . . . . 9
β’ dom
(π¦ β β β¦
1) = β |
79 | 72, 78 | eqtri 2760 |
. . . . . . . 8
β’ dom
(β D (π¦ β
β β¦ π¦)) =
β |
80 | 79 | a1i 11 |
. . . . . . 7
β’ (π΄ β β β dom
(β D (π¦ β
β β¦ π¦)) =
β) |
81 | 22, 67, 68, 80 | dvcmulf 25453 |
. . . . . 6
β’ (π΄ β β β (β
D ((β Γ {π΄})
βf Β· (π¦ β β β¦ π¦))) = ((β Γ {π΄}) βf Β· (β D
(π¦ β β β¦
π¦)))) |
82 | 64, 81 | eqtrd 2772 |
. . . . 5
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = ((β Γ {π΄}) βf Β·
(β D (π¦ β
β β¦ π¦)))) |
83 | 82 | dmeqd 5903 |
. . . 4
β’ (π΄ β β β dom
(β D (π¦ β
β β¦ (π΄ Β·
π¦))) = dom ((β
Γ {π΄})
βf Β· (β D (π¦ β β β¦ π¦)))) |
84 | | ovexd 7440 |
. . . . . 6
β’ (π΄ β β β (β
D (π¦ β β β¦
π¦)) β
V) |
85 | | offval3 7965 |
. . . . . 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 5903 |
. . . 4
β’ (π΄ β β β dom
((β Γ {π΄})
βf Β· (β D (π¦ β β β¦ π¦))) = dom (π€ β (dom (β Γ {π΄}) β© dom (β D (π¦ β β β¦ π¦))) β¦ (((β Γ
{π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€)))) |
88 | 43, 80 | ineq12d 4212 |
. . . . . . . 8
β’ (π΄ β β β (dom
(β Γ {π΄}) β©
dom (β D (π¦ β
β β¦ π¦))) =
(β β© β)) |
89 | 88, 51 | eqtrd 2772 |
. . . . . . 7
β’ (π΄ β β β (dom
(β Γ {π΄}) β©
dom (β D (π¦ β
β β¦ π¦))) =
β) |
90 | 89 | mpteq1d 5242 |
. . . . . 6
β’ (π΄ β β β (π€ β (dom (β Γ
{π΄}) β© dom (β D
(π¦ β β β¦
π¦))) β¦ (((β
Γ {π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€))) = (π€ β β β¦ (((β Γ
{π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€)))) |
91 | 90 | dmeqd 5903 |
. . . . 5
β’ (π΄ β β β dom
(π€ β (dom (β
Γ {π΄}) β© dom
(β D (π¦ β
β β¦ π¦)))
β¦ (((β Γ {π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€))) = dom (π€ β β β¦ (((β Γ
{π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€)))) |
92 | | eqid 2732 |
. . . . . 6
β’ (π€ β β β¦
(((β Γ {π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€))) = (π€ β β β¦ (((β Γ
{π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€))) |
93 | | fvconst2g 7199 |
. . . . . . . 8
β’ ((π΄ β β β§ π€ β β) β
((β Γ {π΄})βπ€) = π΄) |
94 | 71 | fveq1i 6889 |
. . . . . . . . . . 11
β’ ((β
D (π¦ β β β¦
π¦))βπ€) = ((π¦ β β β¦ 1)βπ€) |
95 | 94 | a1i 11 |
. . . . . . . . . 10
β’ (π€ β β β ((β
D (π¦ β β β¦
π¦))βπ€) = ((π¦ β β β¦ 1)βπ€)) |
96 | | eqidd 2733 |
. . . . . . . . . . 11
β’ (π€ β β β (π¦ β β β¦ 1) =
(π¦ β β β¦
1)) |
97 | | eqidd 2733 |
. . . . . . . . . . 11
β’ ((π€ β β β§ π¦ = π€) β 1 = 1) |
98 | 73 | a1i 11 |
. . . . . . . . . . 11
β’ (π€ β β β 1 β
β) |
99 | 96, 97, 45, 98 | fvmptd 7002 |
. . . . . . . . . 10
β’ (π€ β β β ((π¦ β β β¦
1)βπ€) =
1) |
100 | 95, 99 | eqtrd 2772 |
. . . . . . . . 9
β’ (π€ β β β ((β
D (π¦ β β β¦
π¦))βπ€) = 1) |
101 | 100 | adantl 482 |
. . . . . . . 8
β’ ((π΄ β β β§ π€ β β) β
((β D (π¦ β
β β¦ π¦))βπ€) = 1) |
102 | 93, 101 | oveq12d 7423 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β
(((β Γ {π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€)) = (π΄ Β· 1)) |
103 | | mulcl 11190 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β
β) β (π΄ Β·
1) β β) |
104 | 73, 103 | mpan2 689 |
. . . . . . . 8
β’ (π΄ β β β (π΄ Β· 1) β
β) |
105 | 104 | adantr 481 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β (π΄ Β· 1) β
β) |
106 | 102, 105 | eqeltrd 2833 |
. . . . . 6
β’ ((π΄ β β β§ π€ β β) β
(((β Γ {π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€)) β β) |
107 | 92, 106 | dmmptd 6692 |
. . . . 5
β’ (π΄ β β β dom
(π€ β β β¦
(((β Γ {π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€))) = β) |
108 | 91, 107 | eqtrd 2772 |
. . . 4
β’ (π΄ β β β dom
(π€ β (dom (β
Γ {π΄}) β© dom
(β D (π¦ β
β β¦ π¦)))
β¦ (((β Γ {π΄})βπ€) Β· ((β D (π¦ β β β¦ π¦))βπ€))) = β) |
109 | 83, 87, 108 | 3eqtrd 2776 |
. . 3
β’ (π΄ β β β dom
(β D (π¦ β
β β¦ (π΄ Β·
π¦))) =
β) |
110 | 22, 22, 2, 4, 28, 109 | dvcof 25456 |
. 2
β’ (π΄ β β β (β
D (sin β (π¦ β
β β¦ (π΄ Β·
π¦)))) = (((β D sin)
β (π¦ β β
β¦ (π΄ Β· π¦))) βf Β·
(β D (π¦ β
β β¦ (π΄ Β·
π¦))))) |
111 | 23 | a1i 11 |
. . . . . 6
β’ (π΄ β β β (β
D sin) = cos) |
112 | | coscn 25948 |
. . . . . . 7
β’ cos
β (ββcnββ) |
113 | 112 | a1i 11 |
. . . . . 6
β’ (π΄ β β β cos
β (ββcnββ)) |
114 | 111, 113 | eqeltrd 2833 |
. . . . 5
β’ (π΄ β β β (β
D sin) β (ββcnββ)) |
115 | 33 | mptex 7221 |
. . . . . 6
β’ (π¦ β β β¦ (π΄ Β· π¦)) β V |
116 | 115 | a1i 11 |
. . . . 5
β’ (π΄ β β β (π¦ β β β¦ (π΄ Β· π¦)) β V) |
117 | | coexg 7916 |
. . . . 5
β’
(((β D sin) β (ββcnββ) β§ (π¦ β β β¦ (π΄ Β· π¦)) β V) β ((β D sin) β
(π¦ β β β¦
(π΄ Β· π¦))) β V) |
118 | 114, 116,
117 | syl2anc 584 |
. . . 4
β’ (π΄ β β β ((β
D sin) β (π¦ β
β β¦ (π΄ Β·
π¦))) β
V) |
119 | | ovexd 7440 |
. . . 4
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) β V) |
120 | | offval3 7965 |
. . . 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 6722 |
. . . . . . . . 9
β’ (π΄ β β β ran
(π¦ β β β¦
(π΄ Β· π¦)) β
β) |
123 | 122, 28 | sseqtrrd 4022 |
. . . . . . . 8
β’ (π΄ β β β ran
(π¦ β β β¦
(π΄ Β· π¦)) β dom (β D
sin)) |
124 | | dmcosseq 5970 |
. . . . . . . 8
β’ (ran
(π¦ β β β¦
(π΄ Β· π¦)) β dom (β D sin)
β dom ((β D sin) β (π¦ β β β¦ (π΄ Β· π¦))) = dom (π¦ β β β¦ (π΄ Β· π¦))) |
125 | 123, 124 | syl 17 |
. . . . . . 7
β’ (π΄ β β β dom
((β D sin) β (π¦
β β β¦ (π΄
Β· π¦))) = dom (π¦ β β β¦ (π΄ Β· π¦))) |
126 | | ovex 7438 |
. . . . . . . . 9
β’ (π΄ Β· π¦) β V |
127 | | eqid 2732 |
. . . . . . . . 9
β’ (π¦ β β β¦ (π΄ Β· π¦)) = (π¦ β β β¦ (π΄ Β· π¦)) |
128 | 126, 127 | dmmpti 6691 |
. . . . . . . 8
β’ dom
(π¦ β β β¦
(π΄ Β· π¦)) = β |
129 | 128 | a1i 11 |
. . . . . . 7
β’ (π΄ β β β dom
(π¦ β β β¦
(π΄ Β· π¦)) = β) |
130 | 125, 129 | eqtrd 2772 |
. . . . . 6
β’ (π΄ β β β dom
((β D sin) β (π¦
β β β¦ (π΄
Β· π¦))) =
β) |
131 | 130, 109 | ineq12d 4212 |
. . . . 5
β’ (π΄ β β β (dom
((β D sin) β (π¦
β β β¦ (π΄
Β· π¦))) β© dom
(β D (π¦ β
β β¦ (π΄ Β·
π¦)))) = (β β©
β)) |
132 | 131, 51 | eqtrd 2772 |
. . . 4
β’ (π΄ β β β (dom
((β D sin) β (π¦
β β β¦ (π΄
Β· π¦))) β© dom
(β D (π¦ β
β β¦ (π΄ Β·
π¦)))) =
β) |
133 | 132 | mpteq1d 5242 |
. . 3
β’ (π΄ β β β (π€ β (dom ((β D sin)
β (π¦ β β
β¦ (π΄ Β· π¦))) β© dom (β D (π¦ β β β¦ (π΄ Β· π¦)))) β¦ ((((β D sin) β
(π¦ β β β¦
(π΄ Β· π¦)))βπ€) Β· ((β D (π¦ β β β¦ (π΄ Β· π¦)))βπ€))) = (π€ β β β¦ ((((β D sin)
β (π¦ β β
β¦ (π΄ Β· π¦)))βπ€) Β· ((β D (π¦ β β β¦ (π΄ Β· π¦)))βπ€)))) |
134 | 11 | coscld 16070 |
. . . . . 6
β’ ((π΄ β β β§ π€ β β) β
(cosβ(π΄ Β·
π€)) β
β) |
135 | | simpl 483 |
. . . . . 6
β’ ((π΄ β β β§ π€ β β) β π΄ β
β) |
136 | 134, 135 | mulcomd 11231 |
. . . . 5
β’ ((π΄ β β β§ π€ β β) β
((cosβ(π΄ Β·
π€)) Β· π΄) = (π΄ Β· (cosβ(π΄ Β· π€)))) |
137 | 136 | mpteq2dva 5247 |
. . . 4
β’ (π΄ β β β (π€ β β β¦
((cosβ(π΄ Β·
π€)) Β· π΄)) = (π€ β β β¦ (π΄ Β· (cosβ(π΄ Β· π€))))) |
138 | 23 | coeq1i 5857 |
. . . . . . . . 9
β’ ((β
D sin) β (π¦ β
β β¦ (π΄ Β·
π¦))) = (cos β (π¦ β β β¦ (π΄ Β· π¦))) |
139 | 138 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§ π€ β β) β
((β D sin) β (π¦
β β β¦ (π΄
Β· π¦))) = (cos
β (π¦ β β
β¦ (π΄ Β· π¦)))) |
140 | 139 | fveq1d 6890 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β
(((β D sin) β (π¦ β β β¦ (π΄ Β· π¦)))βπ€) = ((cos β (π¦ β β β¦ (π΄ Β· π¦)))βπ€)) |
141 | 4 | ffund 6718 |
. . . . . . . . 9
β’ (π΄ β β β Fun
(π¦ β β β¦
(π΄ Β· π¦))) |
142 | 141 | adantr 481 |
. . . . . . . 8
β’ ((π΄ β β β§ π€ β β) β Fun
(π¦ β β β¦
(π΄ Β· π¦))) |
143 | 10, 128 | eleqtrrdi 2844 |
. . . . . . . 8
β’ ((π΄ β β β§ π€ β β) β π€ β dom (π¦ β β β¦ (π΄ Β· π¦))) |
144 | | fvco 6986 |
. . . . . . . 8
β’ ((Fun
(π¦ β β β¦
(π΄ Β· π¦)) β§ π€ β dom (π¦ β β β¦ (π΄ Β· π¦))) β ((cos β (π¦ β β β¦ (π΄ Β· π¦)))βπ€) = (cosβ((π¦ β β β¦ (π΄ Β· π¦))βπ€))) |
145 | 142, 143,
144 | syl2anc 584 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β ((cos
β (π¦ β β
β¦ (π΄ Β· π¦)))βπ€) = (cosβ((π¦ β β β¦ (π΄ Β· π¦))βπ€))) |
146 | 12 | fveq2d 6892 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β
(cosβ((π¦ β
β β¦ (π΄ Β·
π¦))βπ€)) = (cosβ(π΄ Β· π€))) |
147 | 140, 145,
146 | 3eqtrd 2776 |
. . . . . 6
β’ ((π΄ β β β§ π€ β β) β
(((β D sin) β (π¦ β β β¦ (π΄ Β· π¦)))βπ€) = (cosβ(π΄ Β· π€))) |
148 | | simpl 483 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β β) β π΄ β
β) |
149 | | 0cnd 11203 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β β) β 0 β
β) |
150 | 22, 68 | dvmptc 25466 |
. . . . . . . . . 10
β’ (π΄ β β β (β
D (π¦ β β β¦
π΄)) = (π¦ β β β¦ 0)) |
151 | | simpr 485 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β β) β π¦ β
β) |
152 | 73 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β β) β 1 β
β) |
153 | 71 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ β β β (β
D (π¦ β β β¦
π¦)) = (π¦ β β β¦ 1)) |
154 | 22, 148, 149, 150, 151, 152, 153 | dvmptmul 25469 |
. . . . . . . . 9
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = (π¦ β β β¦ ((0 Β· π¦) + (1 Β· π΄)))) |
155 | 151 | mul02d 11408 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β β) β (0
Β· π¦) =
0) |
156 | 148 | mullidd 11228 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β β) β (1
Β· π΄) = π΄) |
157 | 155, 156 | oveq12d 7423 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π¦ β β) β ((0
Β· π¦) + (1 Β·
π΄)) = (0 + π΄)) |
158 | 148 | addlidd 11411 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π¦ β β) β (0 +
π΄) = π΄) |
159 | 157, 158 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β β) β ((0
Β· π¦) + (1 Β·
π΄)) = π΄) |
160 | 159 | mpteq2dva 5247 |
. . . . . . . . 9
β’ (π΄ β β β (π¦ β β β¦ ((0
Β· π¦) + (1 Β·
π΄))) = (π¦ β β β¦ π΄)) |
161 | 154, 160 | eqtrd 2772 |
. . . . . . . 8
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = (π¦ β β β¦ π΄)) |
162 | 161 | adantr 481 |
. . . . . . 7
β’ ((π΄ β β β§ π€ β β) β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = (π¦ β β β¦ π΄)) |
163 | | eqidd 2733 |
. . . . . . 7
β’ (((π΄ β β β§ π€ β β) β§ π¦ = π€) β π΄ = π΄) |
164 | 162, 163,
10, 135 | fvmptd 7002 |
. . . . . 6
β’ ((π΄ β β β§ π€ β β) β
((β D (π¦ β
β β¦ (π΄ Β·
π¦)))βπ€) = π΄) |
165 | 147, 164 | oveq12d 7423 |
. . . . 5
β’ ((π΄ β β β§ π€ β β) β
((((β D sin) β (π¦ β β β¦ (π΄ Β· π¦)))βπ€) Β· ((β D (π¦ β β β¦ (π΄ Β· π¦)))βπ€)) = ((cosβ(π΄ Β· π€)) Β· π΄)) |
166 | 165 | mpteq2dva 5247 |
. . . 4
β’ (π΄ β β β (π€ β β β¦
((((β D sin) β (π¦ β β β¦ (π΄ Β· π¦)))βπ€) Β· ((β D (π¦ β β β¦ (π΄ Β· π¦)))βπ€))) = (π€ β β β¦ ((cosβ(π΄ Β· π€)) Β· π΄))) |
167 | 8 | fveq2d 6892 |
. . . . . . 7
β’ (π¦ = π€ β (cosβ(π΄ Β· π¦)) = (cosβ(π΄ Β· π€))) |
168 | 167 | oveq2d 7421 |
. . . . . 6
β’ (π¦ = π€ β (π΄ Β· (cosβ(π΄ Β· π¦))) = (π΄ Β· (cosβ(π΄ Β· π€)))) |
169 | 168 | cbvmptv 5260 |
. . . . 5
β’ (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦)))) = (π€ β β β¦ (π΄ Β· (cosβ(π΄ Β· π€)))) |
170 | 169 | a1i 11 |
. . . 4
β’ (π΄ β β β (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦)))) = (π€ β β β¦ (π΄ Β· (cosβ(π΄ Β· π€))))) |
171 | 137, 166,
170 | 3eqtr4d 2782 |
. . 3
β’ (π΄ β β β (π€ β β β¦
((((β D sin) β (π¦ β β β¦ (π΄ Β· π¦)))βπ€) Β· ((β D (π¦ β β β¦ (π΄ Β· π¦)))βπ€))) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) |
172 | 121, 133,
171 | 3eqtrd 2776 |
. 2
β’ (π΄ β β β
(((β D sin) β (π¦ β β β¦ (π΄ Β· π¦))) βf Β· (β D
(π¦ β β β¦
(π΄ Β· π¦)))) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) |
173 | 20, 110, 172 | 3eqtrd 2776 |
1
β’ (π΄ β β β (β
D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) |