This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clmvsneg

Description: Multiplication of a vector by a negated scalar. ( lmodvsneg analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmvsneg.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
clmvsneg.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
clmvsneg.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
clmvsneg.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
clmvsneg.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
clmvsneg.w ⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
clmvsneg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
clmvsneg.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
Assertion clmvsneg ( 𝜑 → ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( - 𝑅 · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 clmvsneg.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 clmvsneg.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 clmvsneg.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 clmvsneg.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
5 clmvsneg.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
6 clmvsneg.w ⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
7 clmvsneg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 clmvsneg.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
9 eqid ⊢ ( invg ‘ 𝐹 ) = ( invg ‘ 𝐹 )
10 clmlmod ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
11 6 10 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
12 1 2 3 4 5 9 11 7 8 lmodvsneg ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( ( ( invg ‘ 𝐹 ) ‘ 𝑅 ) · 𝑋 ) )
13 2 5 clmneg ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑅 ∈ 𝐾 ) → - 𝑅 = ( ( invg ‘ 𝐹 ) ‘ 𝑅 ) )
14 6 8 13 syl2anc ⊢ ( 𝜑 → - 𝑅 = ( ( invg ‘ 𝐹 ) ‘ 𝑅 ) )
15 14 oveq1d ⊢ ( 𝜑 → ( - 𝑅 · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ 𝑅 ) · 𝑋 ) )
16 12 15 eqtr4d ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( - 𝑅 · 𝑋 ) )