Metamath Proof Explorer

Theorem 2atnelpln

Description: The join of two atoms is not a lattice plane. (Contributed by NM, 16-Jul-2012)

		Ref	Expression
	Hypotheses	2atnelpln.j	$⊢ \underset{˙}{\lor} = join (K)$
		2atnelpln.a	$⊢ A = Atoms (K)$
		2atnelpln.p	$⊢ P = LPlanes (K)$
	Assertion	2atnelpln	$⊢ (K \in HL \land Q \in A \land R \in A) \to \neg Q \underset{˙}{\lor} R \in P$

Proof

Step	Hyp	Ref	Expression
1		2atnelpln.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2atnelpln.a	$⊢ A = Atoms (K)$
3		2atnelpln.p	$⊢ P = LPlanes (K)$
4		hllat	$⊢ K \in HL \to K \in Lat$
5	4	3ad2ant1	$⊢ (K \in HL \land Q \in A \land R \in A) \to K \in Lat$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 1 2	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	6 8	latref	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R \in {Base}_{K}) \to (Q \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} R)$
10	5 7 9	syl2anc	$⊢ (K \in HL \land Q \in A \land R \in A) \to (Q \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} R)$
11		simpl1	$⊢ ((K \in HL \land Q \in A \land R \in A) \land Q \underset{˙}{\lor} R \in P) \to K \in HL$
12		simpr	$⊢ ((K \in HL \land Q \in A \land R \in A) \land Q \underset{˙}{\lor} R \in P) \to Q \underset{˙}{\lor} R \in P$
13		simpl2	$⊢ ((K \in HL \land Q \in A \land R \in A) \land Q \underset{˙}{\lor} R \in P) \to Q \in A$
14		simpl3	$⊢ ((K \in HL \land Q \in A \land R \in A) \land Q \underset{˙}{\lor} R \in P) \to R \in A$
15	8 1 2 3	lplnnle2at	$⊢ (K \in HL \land (Q \underset{˙}{\lor} R \in P \land Q \in A \land R \in A)) \to \neg (Q \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} R)$
16	11 12 13 14 15	syl13anc	$⊢ ((K \in HL \land Q \in A \land R \in A) \land Q \underset{˙}{\lor} R \in P) \to \neg (Q \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} R)$
17	16	ex	$⊢ (K \in HL \land Q \in A \land R \in A) \to (Q \underset{˙}{\lor} R \in P \to \neg (Q \underset{˙}{\lor} R) \leq_{K} (Q \underset{˙}{\lor} R))$
18	10 17	mt2d	$⊢ (K \in HL \land Q \in A \land R \in A) \to \neg Q \underset{˙}{\lor} R \in P$