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 ⊢ G = 1 st ⁡ W
vciOLD.2 ⊢ S = 2 nd ⁡ W
vciOLD.3 ⊢ X = ran ⁡ G
Assertion vc2OLD ⊢ W ∈ CVec OLD ∧ A ∈ X → A G A = 2 S A

Proof

Step Hyp Ref Expression
1 vciOLD.1 ⊢ G = 1 st ⁡ W
2 vciOLD.2 ⊢ S = 2 nd ⁡ W
3 vciOLD.3 ⊢ X = ran ⁡ G
4 1 2 3 vcidOLD ⊢ W ∈ CVec OLD ∧ A ∈ X → 1 S A = A
5 4 4 oveq12d ⊢ W ∈ CVec OLD ∧ A ∈ 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 ∈ ℂ
9 1 2 3 vcdir ⊢ W ∈ CVec OLD ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ A ∈ X → 1 + 1 S A = 1 S A G 1 S A
10 8 9 mp3anr1 ⊢ W ∈ CVec OLD ∧ 1 ∈ ℂ ∧ A ∈ X → 1 + 1 S A = 1 S A G 1 S A
11 8 10 mpanr1 ⊢ W ∈ CVec OLD ∧ A ∈ X → 1 + 1 S A = 1 S A G 1 S A
12 7 11 syl5req ⊢ W ∈ CVec OLD ∧ A ∈ X → 1 S A G 1 S A = 2 S A
13 5 12 eqtr3d ⊢ W ∈ CVec OLD ∧ A ∈ X → A G A = 2 S A