Metamath Proof Explorer

Theorem lhpmat

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

		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	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}$

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		simprr	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \neg P \underset{˙}{\leq} W$
7		hlatl	$⊢ K \in HL \to K \in AtLat$
8	7	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in AtLat$
9		simprl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in A$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
12	11	ad2antlr	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
13	10 1 2 3 4	atnle	$⊢ (K \in AtLat \land P \in A \land W \in {Base}_{K}) \to (\neg P \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\land} W = \underset{˙}{0})$
14	8 9 12 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (\neg P \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\land} W = \underset{˙}{0})$
15	6 14	mpbid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = \underset{˙}{0}$