Metamath Proof Explorer


Theorem hv2times

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

Ref Expression
Assertion hv2times A 2 A = A + A

Proof

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