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 ⊢ A ∈ ℋ
normsub.2 ⊢ B ∈ ℋ
Assertion normsubi ⊢ norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ B - ℎ A

Proof

Step Hyp Ref Expression
1 normsub.1 ⊢ A ∈ ℋ
2 normsub.2 ⊢ B ∈ ℋ
3 neg1cn ⊢ − 1 ∈ ℂ
4 2 1 hvsubcli ⊢ B - ℎ A ∈ ℋ
5 3 4 norm-iii-i ⊢ norm ℎ ⁡ -1 ⋅ ℎ B - ℎ A = − 1 ⁢ norm ℎ ⁡ B - ℎ A
6 2 1 hvnegdii ⊢ -1 ⋅ ℎ B - ℎ A = A - ℎ B
7 6 fveq2i ⊢ norm ℎ ⁡ -1 ⋅ ℎ B - ℎ A = norm ℎ ⁡ A - ℎ B
8 ax-1cn ⊢ 1 ∈ ℂ
9 8 absnegi ⊢ − 1 = 1
10 abs1 ⊢ 1 = 1
11 9 10 eqtri ⊢ − 1 = 1
12 11 oveq1i ⊢ − 1 ⁢ norm ℎ ⁡ B - ℎ A = 1 ⁢ norm ℎ ⁡ B - ℎ A
13 4 normcli ⊢ norm ℎ ⁡ B - ℎ A ∈ ℝ
14 13 recni ⊢ norm ℎ ⁡ B - ℎ A ∈ ℂ
15 14 mullidi ⊢ 1 ⁢ norm ℎ ⁡ B - ℎ A = norm ℎ ⁡ B - ℎ A
16 12 15 eqtri ⊢ − 1 ⁢ norm ℎ ⁡ B - ℎ A = norm ℎ ⁡ B - ℎ A
17 5 7 16 3eqtr3i ⊢ norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ B - ℎ A