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

Metamath Proof Explorer

Theorem lmodvsneg

Description: Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Hypotheses lmodvsneg.b ⊢ B = Base W
lmodvsneg.f ⊢ F = Scalar ⁡ W
lmodvsneg.s ⊢ · ˙ = ⋅ W
lmodvsneg.n ⊢ N = inv g ⁡ W
lmodvsneg.k ⊢ K = Base F
lmodvsneg.m ⊢ M = inv g ⁡ F
lmodvsneg.w ⊢ φ → W ∈ LMod
lmodvsneg.x ⊢ φ → X ∈ B
lmodvsneg.r ⊢ φ → R ∈ K
Assertion lmodvsneg ⊢ φ → N ⁡ R · ˙ X = M ⁡ R · ˙ X

Proof

Step Hyp Ref Expression
1 lmodvsneg.b ⊢ B = Base W
2 lmodvsneg.f ⊢ F = Scalar ⁡ W
3 lmodvsneg.s ⊢ · ˙ = ⋅ W
4 lmodvsneg.n ⊢ N = inv g ⁡ W
5 lmodvsneg.k ⊢ K = Base F
6 lmodvsneg.m ⊢ M = inv g ⁡ F
7 lmodvsneg.w ⊢ φ → W ∈ LMod
8 lmodvsneg.x ⊢ φ → X ∈ B
9 lmodvsneg.r ⊢ φ → R ∈ K
10 2 lmodring ⊢ W ∈ LMod → F ∈ Ring
11 7 10 syl ⊢ φ → F ∈ Ring
12 ringgrp ⊢ F ∈ Ring → F ∈ Grp
13 11 12 syl ⊢ φ → F ∈ Grp
14 eqid ⊢ 1 F = 1 F
15 5 14 ringidcl ⊢ F ∈ Ring → 1 F ∈ K
16 11 15 syl ⊢ φ → 1 F ∈ K
17 5 6 grpinvcl ⊢ F ∈ Grp ∧ 1 F ∈ K → M ⁡ 1 F ∈ K
18 13 16 17 syl2anc ⊢ φ → M ⁡ 1 F ∈ K
19 eqid ⊢ ⋅ F = ⋅ F
20 1 2 3 5 19 lmodvsass ⊢ W ∈ LMod ∧ M ⁡ 1 F ∈ K ∧ R ∈ K ∧ X ∈ B → M ⁡ 1 F ⋅ F R · ˙ X = M ⁡ 1 F · ˙ R · ˙ X
21 7 18 9 8 20 syl13anc ⊢ φ → M ⁡ 1 F ⋅ F R · ˙ X = M ⁡ 1 F · ˙ R · ˙ X
22 5 19 14 6 11 9 ringnegl ⊢ φ → M ⁡ 1 F ⋅ F R = M ⁡ R
23 22 oveq1d ⊢ φ → M ⁡ 1 F ⋅ F R · ˙ X = M ⁡ R · ˙ X
24 1 2 3 5 lmodvscl ⊢ W ∈ LMod ∧ R ∈ K ∧ X ∈ B → R · ˙ X ∈ B
25 7 9 8 24 syl3anc ⊢ φ → R · ˙ X ∈ B
26 1 4 2 3 14 6 lmodvneg1 ⊢ W ∈ LMod ∧ R · ˙ X ∈ B → M ⁡ 1 F · ˙ R · ˙ X = N ⁡ R · ˙ X
27 7 25 26 syl2anc ⊢ φ → M ⁡ 1 F · ˙ R · ˙ X = N ⁡ R · ˙ X
28 21 23 27 3eqtr3rd ⊢ φ → N ⁡ R · ˙ X = M ⁡ R · ˙ X