lhpm0atN

Description: If the meet of a lattice hyperplane with a nonzero element is zero, the element is an atom. (Contributed by NM, 28-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lhpm0at.b	$⊢ B = {Base}_{K}$
	lhpm0at.m	$⊢ \underset{˙}{\land} = meet (K)$
	lhpm0at.o	$⊢ \underset{˙}{0} = 0. (K)$
	lhpm0at.a	$⊢ A = Atoms (K)$
	lhpm0at.h	$⊢ H = LHyp (K)$
Assertion	lhpm0atN	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to X \in A$

Proof

Step	Hyp	Ref	Expression
1		lhpm0at.b	$⊢ B = {Base}_{K}$
2		lhpm0at.m	$⊢ \underset{˙}{\land} = meet (K)$
3		lhpm0at.o	$⊢ \underset{˙}{0} = 0. (K)$
4		lhpm0at.a	$⊢ A = Atoms (K)$
5		lhpm0at.h	$⊢ H = LHyp (K)$
6		simpr3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to X \underset{˙}{\land} W = \underset{˙}{0}$
7		simpl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to (K \in HL \land W \in H)$
8		simpr1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to X \in B$
9		simpr2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to X \neq \underset{˙}{0}$
10		hllat	$⊢ K \in HL \to K \in Lat$
11	10	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to K \in Lat$
12	1 5	lhpbase	$⊢ W \in H \to W \in B$
13	12	ad2antlr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to W \in B$
14		eqid	$⊢ \leq_{K} = \leq_{K}$
15	1 14 2	latleeqm1	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \leq_{K} W \leftrightarrow X \underset{˙}{\land} W = X)$
16	11 8 13 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to (X \leq_{K} W \leftrightarrow X \underset{˙}{\land} W = X)$
17	16	biimpa	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \land X \leq_{K} W) \to X \underset{˙}{\land} W = X$
18		simplr3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \land X \leq_{K} W) \to X \underset{˙}{\land} W = \underset{˙}{0}$
19	17 18	eqtr3d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \land X \leq_{K} W) \to X = \underset{˙}{0}$
20	19	ex	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to (X \leq_{K} W \to X = \underset{˙}{0})$
21	20	necon3ad	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to (X \neq \underset{˙}{0} \to \neg X \leq_{K} W)$
22	9 21	mpd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to \neg X \leq_{K} W$
23		eqid	$⊢ ⋖_{K} = ⋖_{K}$
24	1 14 2 23 5	lhpmcvr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \leq_{K} W)) \to (X \underset{˙}{\land} W) ⋖_{K} X$
25	7 8 22 24	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to (X \underset{˙}{\land} W) ⋖_{K} X$
26	6 25	eqbrtrrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to \underset{˙}{0} ⋖_{K} X$
27		simpll	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to K \in HL$
28	1 3 23 4	isat2	$⊢ (K \in HL \land X \in B) \to (X \in A \leftrightarrow \underset{˙}{0} ⋖_{K} X)$
29	27 8 28	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to (X \in A \leftrightarrow \underset{˙}{0} ⋖_{K} X)$
30	26 29	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \neq \underset{˙}{0} \land X \underset{˙}{\land} W = \underset{˙}{0})) \to X \in A$

Metamath Proof Explorer

Theorem lhpm0atN

Proof