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 
|- .x. = ( .s ` W )
clmvs2.a 
|- .+ = ( +g ` W )
Assertion clmvs2 
|- ( ( W e. CMod /\ A e. V ) -> ( A .+ A ) = ( 2 .x. A ) )

Proof

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