Theorem cvp

Description: The Hilbert lattice satisfies the covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	cvp	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to \left(A\cap B=0_{\mathscr{H}}\leftrightarrow A{⋖}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		atelch	$$⊢B\in \mathrm{HAtoms}\to B\in {\mathbf{C}}_{\mathscr{H}}$$
2		chincl	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	sylan2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
4		atcveq0	$$⊢\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow A\cap B=0_{\mathscr{H}}\right)$$
5	3 4	sylancom	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow A\cap B=0_{\mathscr{H}}\right)$$
6		cvexch	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow A{⋖}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\right)$$
7	1 6	sylan2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow A{⋖}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\right)$$
8	5 7	bitr3d	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to \left(A\cap B=0_{\mathscr{H}}\leftrightarrow A{⋖}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\right)$$