Theorem hatomic

Description: A Hilbert lattice is atomic, i.e. any nonzero element is greater than or equal to some atom. Remark in Kalmbach p. 140. Also Definition 3.4-2 in MegPav2000 p. 2345 (PDF p. 8). (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	hatomic	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge A\ne 0_{\mathscr{H}}\right)\to \exists x\in \mathrm{HAtoms}x\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		neeq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(A\ne 0_{\mathscr{H}}\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\ne 0_{\mathscr{H}}\right)$$
2		sseq2	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(x\subseteq A\leftrightarrow x\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\right)$$
3	2	rexbidv	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(\exists x\in \mathrm{HAtoms}x\subseteq A\leftrightarrow \exists x\in \mathrm{HAtoms}x\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\right)$$
4	1 3	imbi12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(\left(A\ne 0_{\mathscr{H}}\to \exists x\in \mathrm{HAtoms}x\subseteq A\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\ne 0_{\mathscr{H}}\to \exists x\in \mathrm{HAtoms}x\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\right)\right)$$
5		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
6	5	elimel	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	6	hatomici	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\ne 0_{\mathscr{H}}\to \exists x\in \mathrm{HAtoms}x\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)$$
8	4 7	dedth	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\ne 0_{\mathscr{H}}\to \exists x\in \mathrm{HAtoms}x\subseteq A\right)$$
9	8	imp	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge A\ne 0_{\mathscr{H}}\right)\to \exists x\in \mathrm{HAtoms}x\subseteq A$$