Theorem cvrp

Description: A Hilbert lattice satisfies the covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 18-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		cvrp.b	$$⊢B={\mathrm{Base}}_K$$
2		cvrp.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cvrp.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cvrp.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
5		cvrp.c	$$⊢C={⋖}_K$$
6		cvrp.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
7		hlomcmcv	$$⊢K\in \mathrm{HL}\to \left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{CvLat}\right)$$
8	1 2 3 4 5 6	cvlcvrp	$$⊢\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(X\underset{\dot{}}{\wedge }P=\underset{\dot{}}{0}\leftrightarrow XC\left(X\underset{\dot{}}{\vee }P\right)\right)$$
9	7 8	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{\wedge }P=\underset{\dot{}}{0}\leftrightarrow XC\left(X\underset{\dot{}}{\vee }P\right)\right)$$