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 𝐺 = ( 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 eqtr2id ( ( 𝑊 ∈ CVecOLD𝐴𝑋 ) → ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( 2 𝑆 𝐴 ) )
13 5 12 eqtr3d ( ( 𝑊 ∈ CVecOLD𝐴𝑋 ) → ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 ) )