Metamath Proof Explorer


Theorem clmvs2

Description: A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007) (Revised by AV, 21-Sep-2021)

Ref Expression
Hypotheses clmvs1.v V = Base W
clmvs1.s · ˙ = W
clmvs2.a + ˙ = + W
Assertion clmvs2 W CMod A V A + ˙ A = 2 · ˙ A

Proof

Step Hyp Ref Expression
1 clmvs1.v V = Base W
2 clmvs1.s · ˙ = W
3 clmvs2.a + ˙ = + W
4 df-2 2 = 1 + 1
5 4 oveq1i 2 · ˙ A = 1 + 1 · ˙ A
6 5 a1i W CMod A V 2 · ˙ A = 1 + 1 · ˙ A
7 simpl W CMod A V W CMod
8 eqid Scalar W = Scalar W
9 8 clm1 W CMod 1 = 1 Scalar W
10 clmlmod W CMod W LMod
11 eqid Base Scalar W = Base Scalar W
12 eqid 1 Scalar W = 1 Scalar W
13 8 11 12 lmod1cl W LMod 1 Scalar W Base Scalar W
14 10 13 syl W CMod 1 Scalar W Base Scalar W
15 9 14 eqeltrd W CMod 1 Base Scalar W
16 15 adantr W CMod A V 1 Base Scalar W
17 simpr W CMod A V A V
18 1 8 2 11 3 clmvsdir W CMod 1 Base Scalar W 1 Base Scalar W A V 1 + 1 · ˙ A = 1 · ˙ A + ˙ 1 · ˙ A
19 7 16 16 17 18 syl13anc W CMod A V 1 + 1 · ˙ A = 1 · ˙ A + ˙ 1 · ˙ A
20 1 2 clmvs1 W CMod A V 1 · ˙ A = A
21 20 20 oveq12d W CMod A V 1 · ˙ A + ˙ 1 · ˙ A = A + ˙ A
22 6 19 21 3eqtrrd W CMod A V A + ˙ A = 2 · ˙ A