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 ⊢ B = Base W
clmvsneg.f ⊢ F = Scalar ⁡ W
clmvsneg.s ⊢ · ˙ = ⋅ W
clmvsneg.n ⊢ N = inv g ⁡ W
clmvsneg.k ⊢ K = Base F
clmvsneg.w ⊢ φ → W ∈ CMod
clmvsneg.x ⊢ φ → X ∈ B
clmvsneg.r ⊢ φ → R ∈ K
Assertion clmvsneg ⊢ φ → N ⁡ R · ˙ X = − R · ˙ X

Proof

Step Hyp Ref Expression
1 clmvsneg.b ⊢ B = Base W
2 clmvsneg.f ⊢ F = Scalar ⁡ W
3 clmvsneg.s ⊢ · ˙ = ⋅ W
4 clmvsneg.n ⊢ N = inv g ⁡ W
5 clmvsneg.k ⊢ K = Base F
6 clmvsneg.w ⊢ φ → W ∈ CMod
7 clmvsneg.x ⊢ φ → X ∈ B
8 clmvsneg.r ⊢ φ → R ∈ K
9 eqid ⊢ inv g ⁡ F = inv g ⁡ F
10 clmlmod ⊢ W ∈ CMod → W ∈ LMod
11 6 10 syl ⊢ φ → W ∈ LMod
12 1 2 3 4 5 9 11 7 8 lmodvsneg ⊢ φ → N ⁡ R · ˙ X = inv g ⁡ F ⁡ R · ˙ X
13 2 5 clmneg ⊢ W ∈ CMod ∧ R ∈ K → − R = inv g ⁡ F ⁡ R
14 6 8 13 syl2anc ⊢ φ → − R = inv g ⁡ F ⁡ R
15 14 oveq1d ⊢ φ → − R · ˙ X = inv g ⁡ F ⁡ R · ˙ X
16 12 15 eqtr4d ⊢ φ → N ⁡ R · ˙ X = − R · ˙ X