Theorem cvr1

Description: A Hilbert lattice has the covering property. Proposition 1(ii) in Kalmbach p. 140 (and its converse). ( chcv1 analog.) (Contributed by NM, 17-Nov-2011)

	Ref	Expression
Hypotheses	cvr1.b	$$⊢B={\mathrm{Base}}_K$$
	cvr1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cvr1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cvr1.c	$$⊢C={⋖}_K$$
	cvr1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	cvr1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to \left(\neg P\underset{\dot{}}{\le }X\leftrightarrow XC\left(X\underset{\dot{}}{\vee }P\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cvr1.b	$$⊢B={\mathrm{Base}}_K$$
2		cvr1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cvr1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cvr1.c	$$⊢C={⋖}_K$$
5		cvr1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		hlomcmcv	$$⊢K\in \mathrm{HL}\to \left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{CvLat}\right)$$
7	1 2 3 4 5	cvlcvr1	$$⊢\left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{CvLat}\right)\wedge X\in B\wedge P\in A\right)\to \left(\neg P\underset{\dot{}}{\le }X\leftrightarrow XC\left(X\underset{\dot{}}{\vee }P\right)\right)$$
8	6 7	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to \left(\neg P\underset{\dot{}}{\le }X\leftrightarrow XC\left(X\underset{\dot{}}{\vee }P\right)\right)$$