lplnnleat

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

	Ref	Expression
Hypotheses	lplnnleat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lplnnleat.a	$⊢ A = Atoms (K)$
	lplnnleat.p	$⊢ P = LPlanes (K)$
Assertion	lplnnleat	$⊢ (K \in HL \land X \in P \land Q \in A) \to \neg X \underset{˙}{\leq} Q$

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

Metamath Proof Explorer