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

Metamath Proof Explorer

Theorem clmvz

Description: Two ways to express the negative of a vector. (Contributed by NM, 29-Feb-2008) (Revised by AV, 7-Oct-2021)

Ref Expression
Hypotheses clmvz.v ⊢ V = Base W
clmvz.m ⊢ - ˙ = - W
clmvz.s ⊢ · ˙ = ⋅ W
clmvz.0 ⊢ 0 ˙ = 0 W
Assertion clmvz ⊢ W ∈ CMod ∧ A ∈ V → 0 ˙ - ˙ A = -1 · ˙ A

Proof

Step Hyp Ref Expression
1 clmvz.v ⊢ V = Base W
2 clmvz.m ⊢ - ˙ = - W
3 clmvz.s ⊢ · ˙ = ⋅ W
4 clmvz.0 ⊢ 0 ˙ = 0 W
5 simpl ⊢ W ∈ CMod ∧ A ∈ V → W ∈ CMod
6 clmgrp ⊢ W ∈ CMod → W ∈ Grp
7 1 4 grpidcl ⊢ W ∈ Grp → 0 ˙ ∈ V
8 6 7 syl ⊢ W ∈ CMod → 0 ˙ ∈ V
9 8 adantr ⊢ W ∈ CMod ∧ A ∈ V → 0 ˙ ∈ V
10 simpr ⊢ W ∈ CMod ∧ A ∈ V → A ∈ V
11 eqid ⊢ + W = + W
12 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
13 1 11 2 12 3 clmvsubval2 ⊢ W ∈ CMod ∧ 0 ˙ ∈ V ∧ A ∈ V → 0 ˙ - ˙ A = -1 · ˙ A + W 0 ˙
14 5 9 10 13 syl3anc ⊢ W ∈ CMod ∧ A ∈ V → 0 ˙ - ˙ A = -1 · ˙ A + W 0 ˙
15 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
16 12 15 clmneg1 ⊢ W ∈ CMod → − 1 ∈ Base Scalar ⁡ W
17 16 adantr ⊢ W ∈ CMod ∧ A ∈ V → − 1 ∈ Base Scalar ⁡ W
18 1 12 3 15 clmvscl ⊢ W ∈ CMod ∧ − 1 ∈ Base Scalar ⁡ W ∧ A ∈ V → -1 · ˙ A ∈ V
19 5 17 10 18 syl3anc ⊢ W ∈ CMod ∧ A ∈ V → -1 · ˙ A ∈ V
20 1 11 4 grprid ⊢ W ∈ Grp ∧ -1 · ˙ A ∈ V → -1 · ˙ A + W 0 ˙ = -1 · ˙ A
21 6 19 20 syl2an2r ⊢ W ∈ CMod ∧ A ∈ V → -1 · ˙ A + W 0 ˙ = -1 · ˙ A
22 14 21 eqtrd ⊢ W ∈ CMod ∧ A ∈ V → 0 ˙ - ˙ A = -1 · ˙ A