Theorem hstcl

Description: Closure of the value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hstcl	$$⊢\left(S\in \mathrm{CHStates}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to S\left(A\right)\in \mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		ishst	$$⊢S\in \mathrm{CHStates}\leftrightarrow \left(S:{\mathbf{C}}_{\mathscr{H}}⟶\mathscr{H}\wedge {norm}_{ℎ}\left(S\left(\mathscr{H}\right)\right)=1\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\right)\right)\right)$$
2	1	simp1bi	$$⊢S\in \mathrm{CHStates}\to S:{\mathbf{C}}_{\mathscr{H}}⟶\mathscr{H}$$
3	2	ffvelcdmda	$$⊢\left(S\in \mathrm{CHStates}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to S\left(A\right)\in \mathscr{H}$$