This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 1st ` W )
vciOLD.2 
|- S = ( 2nd ` W )
vciOLD.3 
|- X = ran G
Assertion vc2OLD 
|- ( ( W e. CVecOLD /\ A e. X ) -> ( A G A ) = ( 2 S A ) )

Proof

Step Hyp Ref Expression
1 vciOLD.1 
 |-  G = ( 1st ` W )
2 vciOLD.2 
 |-  S = ( 2nd ` W )
3 vciOLD.3 
 |-  X = ran G
4 1 2 3 vcidOLD 
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A )
5 4 4 oveq12d 
 |-  ( ( W e. CVecOLD /\ A e. 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 e. CC
9 1 2 3 vcdir 
 |-  ( ( W e. CVecOLD /\ ( 1 e. CC /\ 1 e. CC /\ A e. X ) ) -> ( ( 1 + 1 ) S A ) = ( ( 1 S A ) G ( 1 S A ) ) )
10 8 9 mp3anr1 
 |-  ( ( W e. CVecOLD /\ ( 1 e. CC /\ A e. X ) ) -> ( ( 1 + 1 ) S A ) = ( ( 1 S A ) G ( 1 S A ) ) )
11 8 10 mpanr1 
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( 1 + 1 ) S A ) = ( ( 1 S A ) G ( 1 S A ) ) )
12 7 11 eqtr2id 
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( 1 S A ) G ( 1 S A ) ) = ( 2 S A ) )
13 5 12 eqtr3d 
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( A G A ) = ( 2 S A ) )