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	mulid2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 · ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
15	11 14	syl5eq	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
16	6 15	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 𝑆 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )