Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
โข ( ๐ฅ = ๐ด โ ( i ยท ๐ฅ ) = ( i ยท ๐ด ) ) |
2 |
1
|
fveq2d |
โข ( ๐ฅ = ๐ด โ ( exp โ ( i ยท ๐ฅ ) ) = ( exp โ ( i ยท ๐ด ) ) ) |
3 |
|
oveq2 |
โข ( ๐ฅ = ๐ด โ ( - i ยท ๐ฅ ) = ( - i ยท ๐ด ) ) |
4 |
3
|
fveq2d |
โข ( ๐ฅ = ๐ด โ ( exp โ ( - i ยท ๐ฅ ) ) = ( exp โ ( - i ยท ๐ด ) ) ) |
5 |
2 4
|
oveq12d |
โข ( ๐ฅ = ๐ด โ ( ( exp โ ( i ยท ๐ฅ ) ) + ( exp โ ( - i ยท ๐ฅ ) ) ) = ( ( exp โ ( i ยท ๐ด ) ) + ( exp โ ( - i ยท ๐ด ) ) ) ) |
6 |
5
|
oveq1d |
โข ( ๐ฅ = ๐ด โ ( ( ( exp โ ( i ยท ๐ฅ ) ) + ( exp โ ( - i ยท ๐ฅ ) ) ) / 2 ) = ( ( ( exp โ ( i ยท ๐ด ) ) + ( exp โ ( - i ยท ๐ด ) ) ) / 2 ) ) |
7 |
|
df-cos |
โข cos = ( ๐ฅ โ โ โฆ ( ( ( exp โ ( i ยท ๐ฅ ) ) + ( exp โ ( - i ยท ๐ฅ ) ) ) / 2 ) ) |
8 |
|
ovex |
โข ( ( ( exp โ ( i ยท ๐ด ) ) + ( exp โ ( - i ยท ๐ด ) ) ) / 2 ) โ V |
9 |
6 7 8
|
fvmpt |
โข ( ๐ด โ โ โ ( cos โ ๐ด ) = ( ( ( exp โ ( i ยท ๐ด ) ) + ( exp โ ( - i ยท ๐ด ) ) ) / 2 ) ) |