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 = 1 st W
vciOLD.2 S = 2 nd W
vciOLD.3 X = ran G
Assertion vc2OLD W CVec OLD A X A G A = 2 S A

Proof

Step Hyp Ref Expression
1 vciOLD.1 G = 1 st W
2 vciOLD.2 S = 2 nd W
3 vciOLD.3 X = ran G
4 1 2 3 vcidOLD W CVec OLD A X 1 S A = A
5 4 4 oveq12d W CVec OLD A X 1 S A G 1 S A = A G A
6 df-2 2 = 1 + 1
7 6 oveq1i 2 S A = 1 + 1 S A
8 ax-1cn 1
9 1 2 3 vcdir W CVec OLD 1 1 A X 1 + 1 S A = 1 S A G 1 S A
10 8 9 mp3anr1 W CVec OLD 1 A X 1 + 1 S A = 1 S A G 1 S A
11 8 10 mpanr1 W CVec OLD A X 1 + 1 S A = 1 S A G 1 S A
12 7 11 eqtr2id W CVec OLD A X 1 S A G 1 S A = 2 S A
13 5 12 eqtr3d W CVec OLD A X A G A = 2 S A