Theorem normsubi

Description: Negative doesn't change the norm of a Hilbert space vector. (Contributed by NM, 11-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	normsub.1	⊢ 𝐴 ∈ ℋ
	normsub.2	⊢ 𝐵 ∈ ℋ
Assertion	normsubi	⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		normsub.1	⊢ 𝐴 ∈ ℋ
2		normsub.2	⊢ 𝐵 ∈ ℋ
3		neg1cn	⊢ - 1 ∈ ℂ
4	2 1	hvsubcli	⊢ ( 𝐵 −ℎ 𝐴 ) ∈ ℋ
5	3 4	norm-iii-i	⊢ ( normℎ ‘ ( - 1 ·ℎ ( 𝐵 −ℎ 𝐴 ) ) ) = ( ( abs ‘ - 1 ) · ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) )
6	2 1	hvnegdii	⊢ ( - 1 ·ℎ ( 𝐵 −ℎ 𝐴 ) ) = ( 𝐴 −ℎ 𝐵 )
7	6	fveq2i	⊢ ( normℎ ‘ ( - 1 ·ℎ ( 𝐵 −ℎ 𝐴 ) ) ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) )
8		ax-1cn	⊢ 1 ∈ ℂ
9	8	absnegi	⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
10		abs1	⊢ ( abs ‘ 1 ) = 1
11	9 10	eqtri	⊢ ( abs ‘ - 1 ) = 1
12	11	oveq1i	⊢ ( ( abs ‘ - 1 ) · ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) ) = ( 1 · ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) )
13	4	normcli	⊢ ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) ∈ ℝ
14	13	recni	⊢ ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) ∈ ℂ
15	14	mulid2i	⊢ ( 1 · ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) ) = ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) )
16	12 15	eqtri	⊢ ( ( abs ‘ - 1 ) · ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) ) = ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) )
17	5 7 16	3eqtr3i	⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) )