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 ) )