Theorem lhpmcvr2

Description: Alternate way to express that the meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 9-Apr-2013)

	Ref	Expression
Hypotheses	lhpmcvr2.b	$$⊢B={\mathrm{Base}}_K$$
	lhpmcvr2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lhpmcvr2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	lhpmcvr2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	lhpmcvr2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lhpmcvr2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	lhpmcvr2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge p\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		lhpmcvr2.b	$$⊢B={\mathrm{Base}}_K$$
2		lhpmcvr2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lhpmcvr2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		lhpmcvr2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		lhpmcvr2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		lhpmcvr2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		eqid	$$⊢{⋖}_K={⋖}_K$$
8	1 2 4 7 6	lhpmcvr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to \left(X\underset{\dot{}}{\wedge }W\right){⋖}_{K}X$$
9		simpll	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to K\in \mathrm{HL}$$
10		simprl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to X\in B$$
11	1 6	lhpbase	$$⊢W\in H\to W\in B$$
12	11	ad2antlr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to W\in B$$
13	1 2 3 4 7 5	cvrval5	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge W\in B\right)\to \left(\left(X\underset{\dot{}}{\wedge }W\right){⋖}_{K}X\leftrightarrow \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge p\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\right)$$
14	9 10 12 13	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to \left(\left(X\underset{\dot{}}{\wedge }W\right){⋖}_{K}X\leftrightarrow \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge p\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\right)$$
15	8 14	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }W\wedge p\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)$$