Theorem chm0

Description: Meet with Hilbert lattice zero. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	chm0	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\cap 0_{\mathscr{H}}=0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to A\cap 0_{\mathscr{H}}=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap 0_{\mathscr{H}}$$
2	1	eqeq1d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(A\cap 0_{\mathscr{H}}=0_{\mathscr{H}}\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap 0_{\mathscr{H}}=0_{\mathscr{H}}\right)$$
3		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	elimel	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	4	chm0i	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap 0_{\mathscr{H}}=0_{\mathscr{H}}$$
6	2 5	dedth	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\cap 0_{\mathscr{H}}=0_{\mathscr{H}}$$