Theorem hst0h

Description: The norm of a Hilbert-space-valued state equals zero iff the state value equals zero. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hst0h	$$⊢\left(S\in \mathrm{CHStates}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left({norm}_{ℎ}\left(S\left(A\right)\right)=0\leftrightarrow S\left(A\right)=0_{ℎ}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hstcl	$$⊢\left(S\in \mathrm{CHStates}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to S\left(A\right)\in \mathscr{H}$$
2		norm-i	$$⊢S\left(A\right)\in \mathscr{H}\to \left({norm}_{ℎ}\left(S\left(A\right)\right)=0\leftrightarrow S\left(A\right)=0_{ℎ}\right)$$
3	1 2	syl	$$⊢\left(S\in \mathrm{CHStates}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left({norm}_{ℎ}\left(S\left(A\right)\right)=0\leftrightarrow S\left(A\right)=0_{ℎ}\right)$$