Metamath Proof Explorer

Theorem normsub0

Description: Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion normsub0 ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A - ℎ B = 0 ↔ A = B

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
2 1 eqeq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = 0 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = 0
3 eqeq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A = B ↔ if A ∈ ℋ A 0 ℎ = B
4 2 3 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = 0 ↔ A = B ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = 0 ↔ if A ∈ ℋ A 0 ℎ = B
5 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
6 5 fveqeq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = 0 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = 0
7 eqeq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ = B ↔ if A ∈ ℋ A 0 ℎ = if B ∈ ℋ B 0 ℎ
8 6 7 bibi12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = 0 ↔ if A ∈ ℋ A 0 ℎ = B ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = 0 ↔ if A ∈ ℋ A 0 ℎ = if B ∈ ℋ B 0 ℎ
9 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
10 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
11 9 10 normsub0i ⊢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = 0 ↔ if A ∈ ℋ A 0 ℎ = if B ∈ ℋ B 0 ℎ
12 4 8 11 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A - ℎ B = 0 ↔ A = B