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=ifA∈ℋA0ℎ→normℎ⁡A-ℎB=normℎ⁡ifA∈ℋA0ℎ-ℎB
2 1 eqeq1d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎB=0↔normℎ⁡ifA∈ℋA0ℎ-ℎB=0
3 eqeq1 ⊢A=ifA∈ℋA0ℎ→A=B↔ifA∈ℋA0ℎ=B
4 2 3 bibi12d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎB=0↔A=B↔normℎ⁡ifA∈ℋA0ℎ-ℎB=0↔ifA∈ℋA0ℎ=B
5 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
6 5 fveqeq2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎB=0↔normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=0
7 eqeq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ=B↔ifA∈ℋA0ℎ=ifB∈ℋB0ℎ
8 6 7 bibi12d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎB=0↔ifA∈ℋA0ℎ=B↔normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=0↔ifA∈ℋA0ℎ=ifB∈ℋB0ℎ
9 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
10 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
11 9 10 normsub0i ⊢normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=0↔ifA∈ℋA0ℎ=ifB∈ℋB0ℎ
12 4 8 11 dedth2h ⊢A∈ℋ∧B∈ℋ→normℎ⁡A-ℎB=0↔A=B