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

Metamath Proof Explorer

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 mullidi ⊢ ( 1 · ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) ) = ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) )
16 12 15 eqtri ⊢ ( ( abs ‘ - 1 ) · ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) ) = ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) )
17 5 7 16 3eqtr3i ⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) )