Theorem normsub0i

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
Hypotheses	normsub0.1	$$⊢A\in \mathscr{H}$$
	normsub0.2	$$⊢B\in \mathscr{H}$$
Assertion	normsub0i	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)=0\leftrightarrow A=B$$

Proof

Step	Hyp	Ref	Expression
1		normsub0.1	$$⊢A\in \mathscr{H}$$
2		normsub0.2	$$⊢B\in \mathscr{H}$$
3	1 2	hvsubcli	$$⊢A{-}_{ℎ}B\in \mathscr{H}$$
4	3	norm-i-i	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)=0\leftrightarrow A{-}_{ℎ}B=0_{ℎ}$$
5	1 2	hvsubeq0i	$$⊢A{-}_{ℎ}B=0_{ℎ}\leftrightarrow A=B$$
6	4 5	bitri	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)=0\leftrightarrow A=B$$