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