2llnm3N

Description: Two lattice lines in a lattice plane always meet. (Contributed by NM, 5-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2llnm3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2llnm3.m	$⊢ \underset{˙}{\land} = meet (K)$
	2llnm3.z	$⊢ \underset{˙}{0} = 0. (K)$
	2llnm3.n	$⊢ N = LLines (K)$
	2llnm3.p	$⊢ P = LPlanes (K)$
Assertion	2llnm3N	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to X \underset{˙}{\land} Y \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		2llnm3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2llnm3.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2llnm3.z	$⊢ \underset{˙}{0} = 0. (K)$
4		2llnm3.n	$⊢ N = LLines (K)$
5		2llnm3.p	$⊢ P = LPlanes (K)$
6		oveq1	$⊢ X = Y \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} Y$
7	6	neeq1d	$⊢ X = Y \to (X \underset{˙}{\land} Y \neq \underset{˙}{0} \leftrightarrow Y \underset{˙}{\land} Y \neq \underset{˙}{0})$
8		simpl1	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to K \in HL$
9		hlatl	$⊢ K \in HL \to K \in AtLat$
10	8 9	syl	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to K \in AtLat$
11		simpl2	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to (X \in N \land Y \in N \land W \in P)$
12		simpl3l	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to X \underset{˙}{\leq} W$
13		simpl3r	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to Y \underset{˙}{\leq} W$
14		simpr	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to X \neq Y$
15		eqid	$⊢ Atoms (K) = Atoms (K)$
16	1 2 15 4 5	2llnm2N	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to X \underset{˙}{\land} Y \in Atoms (K)$
17	8 11 12 13 14 16	syl113anc	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to X \underset{˙}{\land} Y \in Atoms (K)$
18	3 15	atn0	$⊢ (K \in AtLat \land X \underset{˙}{\land} Y \in Atoms (K)) \to X \underset{˙}{\land} Y \neq \underset{˙}{0}$
19	10 17 18	syl2anc	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to X \underset{˙}{\land} Y \neq \underset{˙}{0}$
20		hllat	$⊢ K \in HL \to K \in Lat$
21	20	3ad2ant1	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to K \in Lat$
22		simp22	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \in N$
23		eqid	$⊢ {Base}_{K} = {Base}_{K}$
24	23 4	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
25	22 24	syl	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \in {Base}_{K}$
26	23 2	latmidm	$⊢ (K \in Lat \land Y \in {Base}_{K}) \to Y \underset{˙}{\land} Y = Y$
27	21 25 26	syl2anc	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \underset{˙}{\land} Y = Y$
28		simp1	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to K \in HL$
29	3 4	llnn0	$⊢ (K \in HL \land Y \in N) \to Y \neq \underset{˙}{0}$
30	28 22 29	syl2anc	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \neq \underset{˙}{0}$
31	27 30	eqnetrd	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \underset{˙}{\land} Y \neq \underset{˙}{0}$
32	7 19 31	pm2.61ne	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to X \underset{˙}{\land} Y \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem 2llnm3N

Proof