Theorem lplnnleat

Description: A lattice plane cannot majorize an atom. (Contributed by NM, 14-Jul-2012)

	Ref	Expression
Hypotheses	lplnnleat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lplnnleat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lplnnleat.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	lplnnleat	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\to \neg X\underset{\dot{}}{\le }Q$$

Proof

Step	Hyp	Ref	Expression
1		lplnnleat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lplnnleat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		lplnnleat.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
4		simp1	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\to K\in \mathrm{HL}$$
5		simp2	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\to X\in P$$
6		simp3	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\to Q\in A$$
7		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
8	1 7 2 3	lplnnle2at	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in P\wedge Q\in A\wedge Q\in A\right)\right)\to \neg X\underset{\dot{}}{\le }\left(Q\mathrm{join}\left(K\right)Q\right)$$
9	4 5 6 6 8	syl13anc	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\to \neg X\underset{\dot{}}{\le }\left(Q\mathrm{join}\left(K\right)Q\right)$$
10	7 2	hlatjidm	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to Q\mathrm{join}\left(K\right)Q=Q$$
11	10	3adant2	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\to Q\mathrm{join}\left(K\right)Q=Q$$
12	11	breq2d	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\to \left(X\underset{\dot{}}{\le }\left(Q\mathrm{join}\left(K\right)Q\right)\leftrightarrow X\underset{\dot{}}{\le }Q\right)$$
13	9 12	mtbid	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\to \neg X\underset{\dot{}}{\le }Q$$