Theorem cvr2N

Description: Less-than and covers equivalence in a Hilbert lattice. ( chcv2 analog.) (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cvr2.b	$$⊢B={\mathrm{Base}}_K$$
2		cvr2.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3		cvr2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cvr2.c	$$⊢C={⋖}_K$$
5		cvr2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
7	6	3ad2ant1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to K\in \mathrm{Lat}$$
8		simp2	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to X\in B$$
9	1 5	atbase	$$⊢P\in A\to P\in B$$
10	9	3ad2ant3	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to P\in B$$
11		eqid	$$⊢{\le }_K={\le }_K$$
12	1 11 2 3	latnle	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge P\in B\right)\to \left(\neg P{\le }_{K}X\leftrightarrow X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }P\right)\right)$$
13	7 8 10 12	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to \left(\neg P{\le }_{K}X\leftrightarrow X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }P\right)\right)$$
14	1 11 3 4 5	cvr1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to \left(\neg P{\le }_{K}X\leftrightarrow XC\left(X\underset{\dot{}}{\vee }P\right)\right)$$
15	13 14	bitr3d	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }P\right)\leftrightarrow XC\left(X\underset{\dot{}}{\vee }P\right)\right)$$