lhpmatb

Description: An element covered by the lattice unity, when conjoined with an atom, equals zero iff the atom is not under it. (Contributed by NM, 15-Jun-2013)

	Ref	Expression
Hypotheses	lhpmat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhpmat.m	$⊢ \underset{˙}{\land} = meet (K)$
	lhpmat.z	$⊢ \underset{˙}{0} = 0. (K)$
	lhpmat.a	$⊢ A = Atoms (K)$
	lhpmat.h	$⊢ H = LHyp (K)$
Assertion	lhpmatb	$⊢ ((K \in HL \land W \in H) \land P \in A) \to (\neg P \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\land} W = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		lhpmat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lhpmat.m	$⊢ \underset{˙}{\land} = meet (K)$
3		lhpmat.z	$⊢ \underset{˙}{0} = 0. (K)$
4		lhpmat.a	$⊢ A = Atoms (K)$
5		lhpmat.h	$⊢ H = LHyp (K)$
6	1 2 3 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = \underset{˙}{0}$
7	6	anassrs	$⊢ (((K \in HL \land W \in H) \land P \in A) \land \neg P \underset{˙}{\leq} W) \to P \underset{˙}{\land} W = \underset{˙}{0}$
8		hlatl	$⊢ K \in HL \to K \in AtLat$
9	8	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to K \in AtLat$
10		simplr	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to P \in A$
11	3 4	atn0	$⊢ (K \in AtLat \land P \in A) \to P \neq \underset{˙}{0}$
12	11	necomd	$⊢ (K \in AtLat \land P \in A) \to \underset{˙}{0} \neq P$
13	9 10 12	syl2anc	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to \underset{˙}{0} \neq P$
14		neeq1	$⊢ P \underset{˙}{\land} W = \underset{˙}{0} \to (P \underset{˙}{\land} W \neq P \leftrightarrow \underset{˙}{0} \neq P)$
15	14	adantl	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to (P \underset{˙}{\land} W \neq P \leftrightarrow \underset{˙}{0} \neq P)$
16	13 15	mpbird	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to P \underset{˙}{\land} W \neq P$
17		hllat	$⊢ K \in HL \to K \in Lat$
18	17	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to K \in Lat$
19		eqid	$⊢ {Base}_{K} = {Base}_{K}$
20	19 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
21	10 20	syl	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to P \in {Base}_{K}$
22	19 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
23	22	ad3antlr	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to W \in {Base}_{K}$
24	19 1 2	latleeqm1	$⊢ (K \in Lat \land P \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\land} W = P)$
25	18 21 23 24	syl3anc	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to (P \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\land} W = P)$
26	25	necon3bbid	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to (\neg P \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\land} W \neq P)$
27	16 26	mpbird	$⊢ (((K \in HL \land W \in H) \land P \in A) \land P \underset{˙}{\land} W = \underset{˙}{0}) \to \neg P \underset{˙}{\leq} W$
28	7 27	impbida	$⊢ ((K \in HL \land W \in H) \land P \in A) \to (\neg P \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\land} W = \underset{˙}{0})$

Metamath Proof Explorer

Theorem lhpmatb

Proof