Theorem hstri

Description: Hilbert space admits a strong set of Hilbert-space-valued states (CH-states). Theorem in Mayet3 p. 10. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hstr.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	hstr.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	hstri	$$⊢\forall f\in \mathrm{CHStates}\left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\to A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		hstr.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		hstr.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		dfral2	$$⊢\forall f\in \mathrm{CHStates}\left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\leftrightarrow \neg \exists f\in \mathrm{CHStates}\neg \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
4	1 2	strlem1	$$⊢\neg A\subseteq B\to \exists u\in \left(A\setminus B\right){norm}_{ℎ}\left(u\right)=1$$
5		eqid	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)$$
6		biid	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\leftrightarrow \left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)$$
7	5 6 1 2	hstrlem3	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\in \mathrm{CHStates}$$
8	5 6 1 2	hstrlem6	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \neg \left({norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(A\right)\right)=1\to {norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(B\right)\right)=1\right)$$
9		fveq1	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\to f\left(A\right)=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(A\right)$$
10	9	fveqeq2d	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\to \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\leftrightarrow {norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(A\right)\right)=1\right)$$
11		fveq1	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\to f\left(B\right)=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(B\right)$$
12	11	fveqeq2d	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\to \left({norm}_{ℎ}\left(f\left(B\right)\right)=1\leftrightarrow {norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(B\right)\right)=1\right)$$
13	10 12	imbi12d	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\to \left(\left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\leftrightarrow \left({norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(A\right)\right)=1\to {norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(B\right)\right)=1\right)\right)$$
14	13	notbid	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\to \left(\neg \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\leftrightarrow \neg \left({norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(A\right)\right)=1\to {norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(B\right)\right)=1\right)\right)$$
15	14	rspcev	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\in \mathrm{CHStates}\wedge \neg \left({norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(A\right)\right)=1\to {norm}_{ℎ}\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)\left(B\right)\right)=1\right)\right)\to \exists f\in \mathrm{CHStates}\neg \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
16	7 8 15	syl2anc	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \exists f\in \mathrm{CHStates}\neg \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
17	16	rexlimiva	$$⊢\exists u\in \left(A\setminus B\right){norm}_{ℎ}\left(u\right)=1\to \exists f\in \mathrm{CHStates}\neg \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
18	4 17	syl	$$⊢\neg A\subseteq B\to \exists f\in \mathrm{CHStates}\neg \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
19	18	con1i	$$⊢\neg \exists f\in \mathrm{CHStates}\neg \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\to A\subseteq B$$
20	3 19	sylbi	$$⊢\forall f\in \mathrm{CHStates}\left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\to A\subseteq B$$