Theorem lhpjat2

Description: The join of a co-atom (hyperplane) and an atom not under it is the lattice unity. (Contributed by NM, 4-Jun-2012)

	Ref	Expression
Hypotheses	lhpjat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lhpjat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	lhpjat.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
	lhpjat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lhpjat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	lhpjat2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to P\underset{\dot{}}{\vee }W=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		lhpjat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lhpjat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		lhpjat.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
4		lhpjat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		lhpjat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
7	6	ad2antrr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to K\in \mathrm{Lat}$$
8		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
9	8 4	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
10	9	ad2antrl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to P\in {\mathrm{Base}}_K$$
11	8 5	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
12	11	ad2antlr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to W\in {\mathrm{Base}}_K$$
13	8 2	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge P\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\to P\underset{\dot{}}{\vee }W=W\underset{\dot{}}{\vee }P$$
14	7 10 12 13	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to P\underset{\dot{}}{\vee }W=W\underset{\dot{}}{\vee }P$$
15	1 2 3 4 5	lhpjat1	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to W\underset{\dot{}}{\vee }P=\underset{\dot{}}{1}$$
16	14 15	eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to P\underset{\dot{}}{\vee }W=\underset{\dot{}}{1}$$