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

Metamath Proof Explorer

Theorem normneg

Description: The norm of a vector equals the norm of its negative. (Contributed by NM, 23-May-2005) (New usage is discouraged.)

Ref Expression
Assertion normneg ⊢ A ∈ ℋ → norm ℎ ⁡ -1 ⋅ ℎ A = norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
2 normsub ⊢ 0 ℎ ∈ ℋ ∧ A ∈ ℋ → norm ℎ ⁡ 0 ℎ - ℎ A = norm ℎ ⁡ A - ℎ 0 ℎ
3 1 2 mpan ⊢ A ∈ ℋ → norm ℎ ⁡ 0 ℎ - ℎ A = norm ℎ ⁡ A - ℎ 0 ℎ
4 hv2neg ⊢ A ∈ ℋ → 0 ℎ - ℎ A = -1 ⋅ ℎ A
5 4 fveq2d ⊢ A ∈ ℋ → norm ℎ ⁡ 0 ℎ - ℎ A = norm ℎ ⁡ -1 ⋅ ℎ A
6 hvsub0 ⊢ A ∈ ℋ → A - ℎ 0 ℎ = A
7 6 fveq2d ⊢ A ∈ ℋ → norm ℎ ⁡ A - ℎ 0 ℎ = norm ℎ ⁡ A
8 3 5 7 3eqtr3d ⊢ A ∈ ℋ → norm ℎ ⁡ -1 ⋅ ℎ A = norm ℎ ⁡ A