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	⊢ 𝐺 = ( 1st ‘ 𝑊 )
	vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
	vciOLD.3	⊢ 𝑋 = ran 𝐺
Assertion	vc2OLD	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
2		vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
3		vciOLD.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	vcidOLD	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
5	4 4	oveq12d	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( 𝐴 𝐺 𝐴 ) )
6		df-2	⊢ 2 = ( 1 + 1 )
7	6	oveq1i	⊢ ( 2 𝑆 𝐴 ) = ( ( 1 + 1 ) 𝑆 𝐴 )
8		ax-1cn	⊢ 1 ∈ ℂ
9	1 2 3	vcdir	⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + 1 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
10	8 9	mp3anr1	⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + 1 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
11	8 10	mpanr1	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 + 1 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
12	7 11	syl5req	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( 2 𝑆 𝐴 ) )
13	5 12	eqtr3d	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 ) )