This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvs.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvs.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvm1 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 𝑆 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nvs.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvs.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3 nvs.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 neg1cn ⊢ - 1 ∈ ℂ
5 1 2 3 nvs ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 𝑆 𝐴 ) ) = ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) )
6 4 5 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 𝑆 𝐴 ) ) = ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) )
7 ax-1cn ⊢ 1 ∈ ℂ
8 7 absnegi ⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
9 abs1 ⊢ ( abs ‘ 1 ) = 1
10 8 9 eqtri ⊢ ( abs ‘ - 1 ) = 1
11 10 oveq1i ⊢ ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) = ( 1 · ( 𝑁 ‘ 𝐴 ) )
12 1 3 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
13 12 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℂ )
14 13 mullidd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 · ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
15 11 14 eqtrid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
16 6 15 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 𝑆 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )