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 e. ~H
	normsub0.2	|- B e. ~H
Assertion	normsub0i	|- ( ( normh ` ( A -h B ) ) = 0 <-> A = B )

Proof

Step	Hyp	Ref	Expression
1		normsub0.1	|- A e. ~H
2		normsub0.2	|- B e. ~H
3	1 2	hvsubcli	|- ( A -h B ) e. ~H
4	3	norm-i-i	|- ( ( normh ` ( A -h B ) ) = 0 <-> ( A -h B ) = 0h )
5	1 2	hvsubeq0i	|- ( ( A -h B ) = 0h <-> A = B )
6	4 5	bitri	|- ( ( normh ` ( A -h B ) ) = 0 <-> A = B )