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 ⊢ 𝐺 = ( 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 𝑆 𝐴 ) )