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 
|- .- = ( -g ` W )
clmvz.s 
|- .x. = ( .s ` W )
clmvz.0 
|- .0. = ( 0g ` W )
Assertion clmvz 
|- ( ( W e. CMod /\ A e. V ) -> ( .0. .- A ) = ( -u 1 .x. A ) )

Proof

Step Hyp Ref Expression
1 clmvz.v 
 |-  V = ( Base ` W )
2 clmvz.m 
 |-  .- = ( -g ` W )
3 clmvz.s 
 |-  .x. = ( .s ` W )
4 clmvz.0 
 |-  .0. = ( 0g ` W )
5 simpl 
 |-  ( ( W e. CMod /\ A e. V ) -> W e. CMod )
6 clmgrp 
 |-  ( W e. CMod -> W e. Grp )
7 1 4 grpidcl 
 |-  ( W e. Grp -> .0. e. V )
8 6 7 syl 
 |-  ( W e. CMod -> .0. e. V )
9 8 adantr 
 |-  ( ( W e. CMod /\ A e. V ) -> .0. e. V )
10 simpr 
 |-  ( ( W e. CMod /\ A e. V ) -> A e. V )
11 eqid 
 |-  ( +g ` W ) = ( +g ` W )
12 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
13 1 11 2 12 3 clmvsubval2 
 |-  ( ( W e. CMod /\ .0. e. V /\ A e. V ) -> ( .0. .- A ) = ( ( -u 1 .x. A ) ( +g ` W ) .0. ) )
14 5 9 10 13 syl3anc 
 |-  ( ( W e. CMod /\ A e. V ) -> ( .0. .- A ) = ( ( -u 1 .x. A ) ( +g ` W ) .0. ) )
15 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
16 12 15 clmneg1 
 |-  ( W e. CMod -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
17 16 adantr 
 |-  ( ( W e. CMod /\ A e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
18 1 12 3 15 clmvscl 
 |-  ( ( W e. CMod /\ -u 1 e. ( Base ` ( Scalar ` W ) ) /\ A e. V ) -> ( -u 1 .x. A ) e. V )
19 5 17 10 18 syl3anc 
 |-  ( ( W e. CMod /\ A e. V ) -> ( -u 1 .x. A ) e. V )
20 1 11 4 grprid 
 |-  ( ( W e. Grp /\ ( -u 1 .x. A ) e. V ) -> ( ( -u 1 .x. A ) ( +g ` W ) .0. ) = ( -u 1 .x. A ) )
21 6 19 20 syl2an2r 
 |-  ( ( W e. CMod /\ A e. V ) -> ( ( -u 1 .x. A ) ( +g ` W ) .0. ) = ( -u 1 .x. A ) )
22 14 21 eqtrd 
 |-  ( ( W e. CMod /\ A e. V ) -> ( .0. .- A ) = ( -u 1 .x. A ) )