lplnnlelln

Description: A lattice plane is not less than or equal to a lattice line. (Contributed by NM, 14-Jul-2012)

	Ref	Expression
Hypotheses	lplnnlelln.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lplnnlelln.n	$⊢ N = LLines (K)$
	lplnnlelln.p	$⊢ P = LPlanes (K)$
Assertion	lplnnlelln	$⊢ (K \in HL \land X \in P \land Y \in N) \to \neg X \underset{˙}{\leq} Y$

Proof

Step	Hyp	Ref	Expression
1		lplnnlelln.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lplnnlelln.n	$⊢ N = LLines (K)$
3		lplnnlelln.p	$⊢ P = LPlanes (K)$
4		simp3	$⊢ (K \in HL \land X \in P \land Y \in N) \to Y \in N$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ join (K) = join (K)$
7		eqid	$⊢ Atoms (K) = Atoms (K)$
8	5 6 7 2	islln2	$⊢ K \in HL \to (Y \in N \leftrightarrow (Y \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land Y = q join (K) r)))$
9	8	3ad2ant1	$⊢ (K \in HL \land X \in P \land Y \in N) \to (Y \in N \leftrightarrow (Y \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land Y = q join (K) r)))$
10	4 9	mpbid	$⊢ (K \in HL \land X \in P \land Y \in N) \to (Y \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land Y = q join (K) r))$
11		simp11	$⊢ ((K \in HL \land X \in P \land Y \in N) \land (q \in Atoms (K) \land r \in Atoms (K)) \land (q \neq r \land Y = q join (K) r)) \to K \in HL$
12		simp12	$⊢ ((K \in HL \land X \in P \land Y \in N) \land (q \in Atoms (K) \land r \in Atoms (K)) \land (q \neq r \land Y = q join (K) r)) \to X \in P$
13		simp2l	$⊢ ((K \in HL \land X \in P \land Y \in N) \land (q \in Atoms (K) \land r \in Atoms (K)) \land (q \neq r \land Y = q join (K) r)) \to q \in Atoms (K)$
14		simp2r	$⊢ ((K \in HL \land X \in P \land Y \in N) \land (q \in Atoms (K) \land r \in Atoms (K)) \land (q \neq r \land Y = q join (K) r)) \to r \in Atoms (K)$
15	1 6 7 3	lplnnle2at	$⊢ (K \in HL \land (X \in P \land q \in Atoms (K) \land r \in Atoms (K))) \to \neg X \underset{˙}{\leq} (q join (K) r)$
16	11 12 13 14 15	syl13anc	$⊢ ((K \in HL \land X \in P \land Y \in N) \land (q \in Atoms (K) \land r \in Atoms (K)) \land (q \neq r \land Y = q join (K) r)) \to \neg X \underset{˙}{\leq} (q join (K) r)$
17		simp3r	$⊢ ((K \in HL \land X \in P \land Y \in N) \land (q \in Atoms (K) \land r \in Atoms (K)) \land (q \neq r \land Y = q join (K) r)) \to Y = q join (K) r$
18	17	breq2d	$⊢ ((K \in HL \land X \in P \land Y \in N) \land (q \in Atoms (K) \land r \in Atoms (K)) \land (q \neq r \land Y = q join (K) r)) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\leq} (q join (K) r))$
19	16 18	mtbird	$⊢ ((K \in HL \land X \in P \land Y \in N) \land (q \in Atoms (K) \land r \in Atoms (K)) \land (q \neq r \land Y = q join (K) r)) \to \neg X \underset{˙}{\leq} Y$
20	19	3exp	$⊢ (K \in HL \land X \in P \land Y \in N) \to ((q \in Atoms (K) \land r \in Atoms (K)) \to ((q \neq r \land Y = q join (K) r) \to \neg X \underset{˙}{\leq} Y))$
21	20	rexlimdvv	$⊢ (K \in HL \land X \in P \land Y \in N) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land Y = q join (K) r) \to \neg X \underset{˙}{\leq} Y)$
22	21	adantld	$⊢ (K \in HL \land X \in P \land Y \in N) \to ((Y \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land Y = q join (K) r)) \to \neg X \underset{˙}{\leq} Y)$
23	10 22	mpd	$⊢ (K \in HL \land X \in P \land Y \in N) \to \neg X \underset{˙}{\leq} Y$

Metamath Proof Explorer

Theorem lplnnlelln

Proof