Metamath Proof Explorer


Theorem 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 ˙=K
lhpmat.m ˙=meetK
lhpmat.z 0˙=0.K
lhpmat.a A=AtomsK
lhpmat.h H=LHypK
Assertion lhpmatb KHLWHPA¬P˙WP˙W=0˙

Proof

Step Hyp Ref Expression
1 lhpmat.l ˙=K
2 lhpmat.m ˙=meetK
3 lhpmat.z 0˙=0.K
4 lhpmat.a A=AtomsK
5 lhpmat.h H=LHypK
6 1 2 3 4 5 lhpmat KHLWHPA¬P˙WP˙W=0˙
7 6 anassrs KHLWHPA¬P˙WP˙W=0˙
8 hlatl KHLKAtLat
9 8 ad3antrrr KHLWHPAP˙W=0˙KAtLat
10 simplr KHLWHPAP˙W=0˙PA
11 3 4 atn0 KAtLatPAP0˙
12 11 necomd KAtLatPA0˙P
13 9 10 12 syl2anc KHLWHPAP˙W=0˙0˙P
14 neeq1 P˙W=0˙P˙WP0˙P
15 14 adantl KHLWHPAP˙W=0˙P˙WP0˙P
16 13 15 mpbird KHLWHPAP˙W=0˙P˙WP
17 hllat KHLKLat
18 17 ad3antrrr KHLWHPAP˙W=0˙KLat
19 eqid BaseK=BaseK
20 19 4 atbase PAPBaseK
21 10 20 syl KHLWHPAP˙W=0˙PBaseK
22 19 5 lhpbase WHWBaseK
23 22 ad3antlr KHLWHPAP˙W=0˙WBaseK
24 19 1 2 latleeqm1 KLatPBaseKWBaseKP˙WP˙W=P
25 18 21 23 24 syl3anc KHLWHPAP˙W=0˙P˙WP˙W=P
26 25 necon3bbid KHLWHPAP˙W=0˙¬P˙WP˙WP
27 16 26 mpbird KHLWHPAP˙W=0˙¬P˙W
28 7 27 impbida KHLWHPA¬P˙WP˙W=0˙