Theorem stri

Description: Strong state theorem. The states on a Hilbert lattice define an ordering. Remark in Mayet p. 370. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	str.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	str.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stri	$$⊢\forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(B\right)=1\right)\to A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		str.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		str.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		dfral2	$$⊢\forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(B\right)=1\right)\leftrightarrow \neg \exists f\in \mathrm{States}\neg \left(f\left(A\right)=1\to f\left(B\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}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\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	strlem3	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\in \mathrm{States}$$
8	5 6 1 2	strlem6	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \neg \left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(A\right)=1\to \left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(B\right)=1\right)$$
9		fveq1	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\to f\left(A\right)=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(A\right)$$
10	9	eqeq1d	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\to \left(f\left(A\right)=1\leftrightarrow \left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(A\right)=1\right)$$
11		fveq1	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\to f\left(B\right)=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(B\right)$$
12	11	eqeq1d	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\to \left(f\left(B\right)=1\leftrightarrow \left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(B\right)=1\right)$$
13	10 12	imbi12d	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\to \left(\left(f\left(A\right)=1\to f\left(B\right)=1\right)\leftrightarrow \left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(A\right)=1\to \left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(B\right)=1\right)\right)$$
14	13	notbid	$$⊢f=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\to \left(\neg \left(f\left(A\right)=1\to f\left(B\right)=1\right)\leftrightarrow \neg \left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(A\right)=1\to \left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(B\right)=1\right)\right)$$
15	14	rspcev	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\in \mathrm{States}\wedge \neg \left(\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(A\right)=1\to \left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)\left(B\right)=1\right)\right)\to \exists f\in \mathrm{States}\neg \left(f\left(A\right)=1\to f\left(B\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{States}\neg \left(f\left(A\right)=1\to f\left(B\right)=1\right)$$
17	16	rexlimiva	$$⊢\exists u\in \left(A\setminus B\right){norm}_{ℎ}\left(u\right)=1\to \exists f\in \mathrm{States}\neg \left(f\left(A\right)=1\to f\left(B\right)=1\right)$$
18	4 17	syl	$$⊢\neg A\subseteq B\to \exists f\in \mathrm{States}\neg \left(f\left(A\right)=1\to f\left(B\right)=1\right)$$
19	18	con1i	$$⊢\neg \exists f\in \mathrm{States}\neg \left(f\left(A\right)=1\to f\left(B\right)=1\right)\to A\subseteq B$$
20	3 19	sylbi	$$⊢\forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(B\right)=1\right)\to A\subseteq B$$