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=BaseW
clmvs1.s ·˙=W
clmvs2.a +˙=+W
Assertion clmvs2 WCModAVA+˙A=2·˙A

Proof

Step Hyp Ref Expression
1 clmvs1.v V=BaseW
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 WCModAV2·˙A=1+1·˙A
7 simpl WCModAVWCMod
8 eqid ScalarW=ScalarW
9 8 clm1 WCMod1=1ScalarW
10 clmlmod WCModWLMod
11 eqid BaseScalarW=BaseScalarW
12 eqid 1ScalarW=1ScalarW
13 8 11 12 lmod1cl WLMod1ScalarWBaseScalarW
14 10 13 syl WCMod1ScalarWBaseScalarW
15 9 14 eqeltrd WCMod1BaseScalarW
16 15 adantr WCModAV1BaseScalarW
17 simpr WCModAVAV
18 1 8 2 11 3 clmvsdir WCMod1BaseScalarW1BaseScalarWAV1+1·˙A=1·˙A+˙1·˙A
19 7 16 16 17 18 syl13anc WCModAV1+1·˙A=1·˙A+˙1·˙A
20 1 2 clmvs1 WCModAV1·˙A=A
21 20 20 oveq12d WCModAV1·˙A+˙1·˙A=A+˙A
22 6 19 21 3eqtrrd WCModAVA+˙A=2·˙A