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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmvs1.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
clmvs2.a ⊢ + = ( +g ‘ 𝑊 )
Assertion clmvs2 ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 + 𝐴 ) = ( 2 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 clmvs1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clmvs1.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 clmvs2.a ⊢ + = ( +g ‘ 𝑊 )
4 df-2 ⊢ 2 = ( 1 + 1 )
5 4 oveq1i ⊢ ( 2 · 𝐴 ) = ( ( 1 + 1 ) · 𝐴 )
6 5 a1i ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( 2 · 𝐴 ) = ( ( 1 + 1 ) · 𝐴 ) )
7 simpl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
8 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
9 8 clm1 ⊢ ( 𝑊 ∈ ℂMod → 1 = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
10 clmlmod ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
11 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
12 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
13 8 11 12 lmod1cl ⊢ ( 𝑊 ∈ LMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
14 10 13 syl ⊢ ( 𝑊 ∈ ℂMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
15 9 14 eqeltrd ⊢ ( 𝑊 ∈ ℂMod → 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
16 15 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 simpr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
18 1 8 2 11 3 clmvsdir ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ 𝑉 ) ) → ( ( 1 + 1 ) · 𝐴 ) = ( ( 1 · 𝐴 ) + ( 1 · 𝐴 ) ) )
19 7 16 16 17 18 syl13anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( ( 1 + 1 ) · 𝐴 ) = ( ( 1 · 𝐴 ) + ( 1 · 𝐴 ) ) )
20 1 2 clmvs1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( 1 · 𝐴 ) = 𝐴 )
21 20 20 oveq12d ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( ( 1 · 𝐴 ) + ( 1 · 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
22 6 19 21 3eqtrrd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 + 𝐴 ) = ( 2 · 𝐴 ) )