Metamath Proof Explorer

Theorem ncvsm1

Description: The norm of the opposite of a vector. (Contributed by NM, 28-Nov-2006) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses ncvsprp.v 
|- V = ( Base ` W )
ncvsprp.n 
|- N = ( norm ` W )
ncvsprp.s 
|- .x. = ( .s ` W )
Assertion ncvsm1 
|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> ( N ` ( -u 1 .x. A ) ) = ( N ` A ) )

Proof

Step Hyp Ref Expression
1 ncvsprp.v 
 |-  V = ( Base ` W )
2 ncvsprp.n 
 |-  N = ( norm ` W )
3 ncvsprp.s 
 |-  .x. = ( .s ` W )
4 simpl 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> W e. ( NrmVec i^i CVec ) )
5 elin 
 |-  ( W e. ( NrmVec i^i CVec ) <-> ( W e. NrmVec /\ W e. CVec ) )
6 id 
 |-  ( W e. CVec -> W e. CVec )
7 6 cvsclm 
 |-  ( W e. CVec -> W e. CMod )
8 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
9 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
10 8 9 clmneg1 
 |-  ( W e. CMod -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
11 7 10 syl 
 |-  ( W e. CVec -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
12 5 11 simplbiim 
 |-  ( W e. ( NrmVec i^i CVec ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
13 12 adantr 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
14 simpr 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> A e. V )
15 1 2 3 8 9 ncvsprp 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ -u 1 e. ( Base ` ( Scalar ` W ) ) /\ A e. V ) -> ( N ` ( -u 1 .x. A ) ) = ( ( abs ` -u 1 ) x. ( N ` A ) ) )
16 4 13 14 15 syl3anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> ( N ` ( -u 1 .x. A ) ) = ( ( abs ` -u 1 ) x. ( N ` A ) ) )
17 ax-1cn 
 |-  1 e. CC
18 17 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
19 abs1 
 |-  ( abs ` 1 ) = 1
20 18 19 eqtri 
 |-  ( abs ` -u 1 ) = 1
21 20 oveq1i 
 |-  ( ( abs ` -u 1 ) x. ( N ` A ) ) = ( 1 x. ( N ` A ) )
22 nvcnlm 
 |-  ( W e. NrmVec -> W e. NrmMod )
23 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
24 22 23 syl 
 |-  ( W e. NrmVec -> W e. NrmGrp )
25 24 adantr 
 |-  ( ( W e. NrmVec /\ W e. CVec ) -> W e. NrmGrp )
26 5 25 sylbi 
 |-  ( W e. ( NrmVec i^i CVec ) -> W e. NrmGrp )
27 1 2 nmcl 
 |-  ( ( W e. NrmGrp /\ A e. V ) -> ( N ` A ) e. RR )
28 26 27 sylan 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> ( N ` A ) e. RR )
29 28 recnd 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> ( N ` A ) e. CC )
30 29 mulid2d 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> ( 1 x. ( N ` A ) ) = ( N ` A ) )
31 21 30 syl5eq 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> ( ( abs ` -u 1 ) x. ( N ` A ) ) = ( N ` A ) )
32 16 31 eqtrd 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V ) -> ( N ` ( -u 1 .x. A ) ) = ( N ` A ) )