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

Proof

Step Hyp Ref Expression
1 ncvsprp.v ⊢ V = Base W
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 ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
10 8 9 clmneg1 ⊢ W ∈ CMod → − 1 ∈ Base Scalar ⁡ W
11 7 10 syl ⊢ W ∈ ℂVec → − 1 ∈ Base Scalar ⁡ W
12 5 11 simplbiim ⊢ W ∈ NrmVec ∩ ℂVec → − 1 ∈ Base Scalar ⁡ W
13 12 adantr ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V → − 1 ∈ Base Scalar ⁡ W
14 simpr ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V → A ∈ V
15 1 2 3 8 9 ncvsprp ⊢ W ∈ NrmVec ∩ ℂVec ∧ − 1 ∈ Base Scalar ⁡ 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