Theorem hst1a

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

	Ref	Expression
Assertion	hst1a	$$⊢S\in \mathrm{CHStates}\to {norm}_{ℎ}\left(S\left(\mathscr{H}\right)\right)=1$$

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	simp2bi	$$⊢S\in \mathrm{CHStates}\to {norm}_{ℎ}\left(S\left(\mathscr{H}\right)\right)=1$$