Theorem st0

Description: The state of the zero subspace. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	sto2i	$$⊢S\in \mathrm{States}\to S\left(\perp \left(\mathscr{H}\right)\right)=1-S\left(\mathscr{H}\right)$$
3		sthil	$$⊢S\in \mathrm{States}\to S\left(\mathscr{H}\right)=1$$
4	3	oveq2d	$$⊢S\in \mathrm{States}\to 1-S\left(\mathscr{H}\right)=1-1$$
5	2 4	eqtrd	$$⊢S\in \mathrm{States}\to S\left(\perp \left(\mathscr{H}\right)\right)=1-1$$
6		choc1	$$⊢\perp \left(\mathscr{H}\right)=0_{\mathscr{H}}$$
7	6	fveq2i	$$⊢S\left(\perp \left(\mathscr{H}\right)\right)=S\left(0_{\mathscr{H}}\right)$$
8		1m1e0	$$⊢1-1=0$$
9	5 7 8	3eqtr3g	$$⊢S\in \mathrm{States}\to S\left(0_{\mathscr{H}}\right)=0$$