Metamath Proof Explorer


Theorem vc2OLD

Description: A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007) Obsolete theorem, use clmvs2 together with cvsclm instead. (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses vciOLD.1 G=1stW
vciOLD.2 S=2ndW
vciOLD.3 X=ranG
Assertion vc2OLD WCVecOLDAXAGA=2SA

Proof

Step Hyp Ref Expression
1 vciOLD.1 G=1stW
2 vciOLD.2 S=2ndW
3 vciOLD.3 X=ranG
4 1 2 3 vcidOLD WCVecOLDAX1SA=A
5 4 4 oveq12d WCVecOLDAX1SAG1SA=AGA
6 df-2 2=1+1
7 6 oveq1i 2SA=1+1SA
8 ax-1cn 1
9 1 2 3 vcdir WCVecOLD11AX1+1SA=1SAG1SA
10 8 9 mp3anr1 WCVecOLD1AX1+1SA=1SAG1SA
11 8 10 mpanr1 WCVecOLDAX1+1SA=1SAG1SA
12 7 11 eqtr2id WCVecOLDAX1SAG1SA=2SA
13 5 12 eqtr3d WCVecOLDAXAGA=2SA