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 | |
|
lhpmat.m | |
||
lhpmat.z | |
||
lhpmat.a | |
||
lhpmat.h | |
||
Assertion | lhpmatb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhpmat.l | |
|
2 | lhpmat.m | |
|
3 | lhpmat.z | |
|
4 | lhpmat.a | |
|
5 | lhpmat.h | |
|
6 | 1 2 3 4 5 | lhpmat | |
7 | 6 | anassrs | |
8 | hlatl | |
|
9 | 8 | ad3antrrr | |
10 | simplr | |
|
11 | 3 4 | atn0 | |
12 | 11 | necomd | |
13 | 9 10 12 | syl2anc | |
14 | neeq1 | |
|
15 | 14 | adantl | |
16 | 13 15 | mpbird | |
17 | hllat | |
|
18 | 17 | ad3antrrr | |
19 | eqid | |
|
20 | 19 4 | atbase | |
21 | 10 20 | syl | |
22 | 19 5 | lhpbase | |
23 | 22 | ad3antlr | |
24 | 19 1 2 | latleeqm1 | |
25 | 18 21 23 24 | syl3anc | |
26 | 25 | necon3bbid | |
27 | 16 26 | mpbird | |
28 | 7 27 | impbida | |