Description: Two times a vector. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | hv2times | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 | |
|
2 | 1 | oveq1i | |
3 | ax-1cn | |
|
4 | ax-hvdistr2 | |
|
5 | 3 3 4 | mp3an12 | |
6 | 2 5 | eqtrid | |
7 | ax-hvdistr1 | |
|
8 | 3 7 | mp3an1 | |
9 | 8 | anidms | |
10 | hvaddcl | |
|
11 | 10 | anidms | |
12 | ax-hvmulid | |
|
13 | 11 12 | syl | |
14 | 6 9 13 | 3eqtr2d | |