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 | |
|
clmvs1.s | |
||
clmvs2.a | |
||
Assertion | clmvs2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clmvs1.v | |
|
2 | clmvs1.s | |
|
3 | clmvs2.a | |
|
4 | df-2 | |
|
5 | 4 | oveq1i | |
6 | 5 | a1i | |
7 | simpl | |
|
8 | eqid | |
|
9 | 8 | clm1 | |
10 | clmlmod | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | 8 11 12 | lmod1cl | |
14 | 10 13 | syl | |
15 | 9 14 | eqeltrd | |
16 | 15 | adantr | |
17 | simpr | |
|
18 | 1 8 2 11 3 | clmvsdir | |
19 | 7 16 16 17 18 | syl13anc | |
20 | 1 2 | clmvs1 | |
21 | 20 20 | oveq12d | |
22 | 6 19 21 | 3eqtrrd | |