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=BaseW
ncvsprp.n ⊢N=norm⁡W
ncvsprp.s ⊢·˙=⋅W
Assertion ncvsm1 ⊢W∈NrmVec∩ℂVec∧A∈V→N⁡-1·˙A=N⁡A

Proof

Step Hyp Ref Expression
1 ncvsprp.v ⊢V=BaseW
2 ncvsprp.n ⊢N=norm⁡W
3 ncvsprp.s ⊢·˙=⋅W
4 simpl ⊢W∈NrmVec∩ℂVec∧A∈V→W∈NrmVec∩ℂVec
5 elin ⊢W∈NrmVec∩ℂVec↔W∈NrmVec∧W∈ℂVec
6 id ⊢W∈ℂVec→W∈ℂVec
7 6 cvsclm ⊢W∈ℂVec→W∈CMod
8 eqid ⊢Scalar⁡W=Scalar⁡W
9 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
10 8 9 clmneg1 ⊢W∈CMod→−1∈BaseScalar⁡W
11 7 10 syl ⊢W∈ℂVec→−1∈BaseScalar⁡W
12 5 11 simplbiim ⊢W∈NrmVec∩ℂVec→−1∈BaseScalar⁡W
13 12 adantr ⊢W∈NrmVec∩ℂVec∧A∈V→−1∈BaseScalar⁡W
14 simpr ⊢W∈NrmVec∩ℂVec∧A∈V→A∈V
15 1 2 3 8 9 ncvsprp ⊢W∈NrmVec∩ℂVec∧−1∈BaseScalar⁡W∧A∈V→N⁡-1·˙A=−1⁢N⁡A
16 4 13 14 15 syl3anc ⊢W∈NrmVec∩ℂVec∧A∈V→N⁡-1·˙A=−1⁢N⁡A
17 ax-1cn ⊢1∈ℂ
18 17 absnegi ⊢−1=1
19 abs1 ⊢1=1
20 18 19 eqtri ⊢−1=1
21 20 oveq1i ⊢−1⁢N⁡A=1⁢N⁡A
22 nvcnlm ⊢W∈NrmVec→W∈NrmMod
23 nlmngp ⊢W∈NrmMod→W∈NrmGrp
24 22 23 syl ⊢W∈NrmVec→W∈NrmGrp
25 24 adantr ⊢W∈NrmVec∧W∈ℂVec→W∈NrmGrp
26 5 25 sylbi ⊢W∈NrmVec∩ℂVec→W∈NrmGrp
27 1 2 nmcl ⊢W∈NrmGrp∧A∈V→N⁡A∈ℝ
28 26 27 sylan ⊢W∈NrmVec∩ℂVec∧A∈V→N⁡A∈ℝ
29 28 recnd ⊢W∈NrmVec∩ℂVec∧A∈V→N⁡A∈ℂ
30 29 mullidd ⊢W∈NrmVec∩ℂVec∧A∈V→1⁢N⁡A=N⁡A
31 21 30 eqtrid ⊢W∈NrmVec∩ℂVec∧A∈V→−1⁢N⁡A=N⁡A
32 16 31 eqtrd ⊢W∈NrmVec∩ℂVec∧A∈V→N⁡-1·˙A=N⁡A