Theorem largei

Description: A Hilbert lattice admits a largei set of states. Remark in Mayet p. 370. (Contributed by NM, 7-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Hypothesis	large.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	largei	$$⊢\neg A=0_{\mathscr{H}}\leftrightarrow \exists f\in \mathrm{States}f\left(A\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		large.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		ralnex	$$⊢\forall f\in \mathrm{States}\neg f\left(A\right)=1\leftrightarrow \neg \exists f\in \mathrm{States}f\left(A\right)=1$$
3		ax-1ne0	$$⊢1\ne 0$$
4	3	neii	$$⊢\neg 1=0$$
5		st0	$$⊢f\in \mathrm{States}\to f\left(0_{\mathscr{H}}\right)=0$$
6	5	eqeq1d	$$⊢f\in \mathrm{States}\to \left(f\left(0_{\mathscr{H}}\right)=1\leftrightarrow 0=1\right)$$
7		eqcom	$$⊢0=1\leftrightarrow 1=0$$
8	6 7	bitrdi	$$⊢f\in \mathrm{States}\to \left(f\left(0_{\mathscr{H}}\right)=1\leftrightarrow 1=0\right)$$
9	4 8	mtbiri	$$⊢f\in \mathrm{States}\to \neg f\left(0_{\mathscr{H}}\right)=1$$
10		mtt	$$⊢\neg f\left(0_{\mathscr{H}}\right)=1\to \left(\neg f\left(A\right)=1\leftrightarrow \left(f\left(A\right)=1\to f\left(0_{\mathscr{H}}\right)=1\right)\right)$$
11	9 10	syl	$$⊢f\in \mathrm{States}\to \left(\neg f\left(A\right)=1\leftrightarrow \left(f\left(A\right)=1\to f\left(0_{\mathscr{H}}\right)=1\right)\right)$$
12	11	ralbiia	$$⊢\forall f\in \mathrm{States}\neg f\left(A\right)=1\leftrightarrow \forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(0_{\mathscr{H}}\right)=1\right)$$
13		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
14	1 13	strb	$$⊢\forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(0_{\mathscr{H}}\right)=1\right)\leftrightarrow A\subseteq 0_{\mathscr{H}}$$
15	1	chle0i	$$⊢A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}$$
16	12 14 15	3bitri	$$⊢\forall f\in \mathrm{States}\neg f\left(A\right)=1\leftrightarrow A=0_{\mathscr{H}}$$
17	2 16	bitr3i	$$⊢\neg \exists f\in \mathrm{States}f\left(A\right)=1\leftrightarrow A=0_{\mathscr{H}}$$
18	17	con1bii	$$⊢\neg A=0_{\mathscr{H}}\leftrightarrow \exists f\in \mathrm{States}f\left(A\right)=1$$