Description: An atomic lattice has a zero element. We can use this in place of op0cl for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | atl0cl.b | |- B = ( Base ` K ) |
|
| atl0cl.z | |- .0. = ( 0. ` K ) |
||
| Assertion | atl0cl | |- ( K e. AtLat -> .0. e. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | atl0cl.b | |- B = ( Base ` K ) |
|
| 2 | atl0cl.z | |- .0. = ( 0. ` K ) |
|
| 3 | eqid | |- ( glb ` K ) = ( glb ` K ) |
|
| 4 | 1 3 2 | p0val | |- ( K e. AtLat -> .0. = ( ( glb ` K ) ` B ) ) |
| 5 | id | |- ( K e. AtLat -> K e. AtLat ) |
|
| 6 | eqid | |- ( lub ` K ) = ( lub ` K ) |
|
| 7 | 1 6 3 | atl0dm | |- ( K e. AtLat -> B e. dom ( glb ` K ) ) |
| 8 | 1 3 5 7 | glbcl | |- ( K e. AtLat -> ( ( glb ` K ) ` B ) e. B ) |
| 9 | 4 8 | eqeltrd | |- ( K e. AtLat -> .0. e. B ) |