Theorem nv2

Description: A vector plus itself is two times the vector. (Contributed by NM, 9-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvdi.1	|- X = ( BaseSet ` U )
	nvdi.2	|- G = ( +v ` U )
	nvdi.4	|- S = ( .sOLD ` U )
Assertion	nv2	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G A ) = ( 2 S A ) )

Proof

Step	Hyp	Ref	Expression
1		nvdi.1	|- X = ( BaseSet ` U )
2		nvdi.2	|- G = ( +v ` U )
3		nvdi.4	|- S = ( .sOLD ` U )
4		eqid	|- ( 1st ` U ) = ( 1st ` U )
5	4	nvvc	|- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
6	2	vafval	|- G = ( 1st ` ( 1st ` U ) )
7	3	smfval	|- S = ( 2nd ` ( 1st ` U ) )
8	1 2	bafval	|- X = ran G
9	6 7 8	vc2OLD	|- ( ( ( 1st ` U ) e. CVecOLD /\ A e. X ) -> ( A G A ) = ( 2 S A ) )
10	5 9	sylan	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G A ) = ( 2 S A ) )