Theorem hst0

Description: A Hilbert-space-valued state is zero at the zero subspace. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
2		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
3	2	choccli	$$⊢\perp \left(\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	ch0lei	$$⊢0_{\mathscr{H}}\subseteq \perp \left(\mathscr{H}\right)$$
5		hstorth	$$⊢\left(\left(S\in \mathrm{CHStates}\wedge 0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}\wedge 0_{\mathscr{H}}\subseteq \perp \left(\mathscr{H}\right)\right)\right)\to S\left(0_{\mathscr{H}}\right){\cdot }_{\mathrm{ih}}S\left(\mathscr{H}\right)=0$$
6	2 4 5	mpanr12	$$⊢\left(S\in \mathrm{CHStates}\wedge 0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\right)\to S\left(0_{\mathscr{H}}\right){\cdot }_{\mathrm{ih}}S\left(\mathscr{H}\right)=0$$
7	1 6	mpan2	$$⊢S\in \mathrm{CHStates}\to S\left(0_{\mathscr{H}}\right){\cdot }_{\mathrm{ih}}S\left(\mathscr{H}\right)=0$$
8		hstoh	$$⊢\left(S\in \mathrm{CHStates}\wedge 0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\wedge S\left(0_{\mathscr{H}}\right){\cdot }_{\mathrm{ih}}S\left(\mathscr{H}\right)=0\right)\to S\left(0_{\mathscr{H}}\right)=0_{ℎ}$$
9	1 8	mp3an2	$$⊢\left(S\in \mathrm{CHStates}\wedge S\left(0_{\mathscr{H}}\right){\cdot }_{\mathrm{ih}}S\left(\mathscr{H}\right)=0\right)\to S\left(0_{\mathscr{H}}\right)=0_{ℎ}$$
10	7 9	mpdan	$$⊢S\in \mathrm{CHStates}\to S\left(0_{\mathscr{H}}\right)=0_{ℎ}$$