Metamath Proof Explorer

Theorem nvm1

Description: The norm of the negative of a vector. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvs.1 ⊢ X = BaseSet ⁡ U
nvs.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvs.6 ⊢ N = norm CV ⁡ U
Assertion nvm1 ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ -1 S A = N ⁡ A

Proof

Step Hyp Ref Expression
1 nvs.1 ⊢ X = BaseSet ⁡ U
2 nvs.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 nvs.6 ⊢ N = norm CV ⁡ U
4 neg1cn ⊢ − 1 ∈ ℂ
5 1 2 3 nvs ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ A ∈ X → N ⁡ -1 S A = − 1 ⁢ N ⁡ A
6 4 5 mp3an2 ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ -1 S A = − 1 ⁢ N ⁡ A
7 ax-1cn ⊢ 1 ∈ ℂ
8 7 absnegi ⊢ − 1 = 1
9 abs1 ⊢ 1 = 1
10 8 9 eqtri ⊢ − 1 = 1
11 10 oveq1i ⊢ − 1 ⁢ N ⁡ A = 1 ⁢ N ⁡ A
12 1 3 nvcl ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℝ
13 12 recnd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℂ
14 13 mullidd ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 ⁢ N ⁡ A = N ⁡ A
15 11 14 eqtrid ⊢ U ∈ NrmCVec ∧ A ∈ X → − 1 ⁢ N ⁡ A = N ⁡ A
16 6 15 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ -1 S A = N ⁡ A