Metamath Proof Explorer


Theorem hv2times

Description: Two times a vector. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hv2times A2A=A+A

Proof

Step Hyp Ref Expression
1 df-2 2=1+1
2 1 oveq1i 2A=1+1A
3 ax-1cn 1
4 ax-hvdistr2 11A1+1A=1A+1A
5 3 3 4 mp3an12 A1+1A=1A+1A
6 2 5 eqtrid A2A=1A+1A
7 ax-hvdistr1 1AA1A+A=1A+1A
8 3 7 mp3an1 AA1A+A=1A+1A
9 8 anidms A1A+A=1A+1A
10 hvaddcl AAA+A
11 10 anidms AA+A
12 ax-hvmulid A+A1A+A=A+A
13 11 12 syl A1A+A=A+A
14 6 9 13 3eqtr2d A2A=A+A