Metamath Proof Explorer

Theorem normsub

Description: Swapping order of subtraction doesn't change the norm of a vector. (Contributed by NM, 14-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion normsub ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ B - ℎ A

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
2 oveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → B - ℎ A = B - ℎ if A ∈ ℋ A 0 ℎ
3 2 fveq2d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ B - ℎ A = norm ℎ ⁡ B - ℎ if A ∈ ℋ A 0 ℎ
4 1 3 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ B - ℎ A ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = norm ℎ ⁡ B - ℎ if A ∈ ℋ A 0 ℎ
5 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
6 5 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
7 fvoveq1 ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ B - ℎ if A ∈ ℋ A 0 ℎ = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ - ℎ if A ∈ ℋ A 0 ℎ
8 6 7 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = norm ℎ ⁡ B - ℎ if A ∈ ℋ A 0 ℎ ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ - ℎ if A ∈ ℋ A 0 ℎ
9 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
10 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
11 9 10 normsubi ⊢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ - ℎ if A ∈ ℋ A 0 ℎ
12 4 8 11 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ B - ℎ A