Description: A Hilbert lattice satisfies the covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 18-Nov-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cvrp.b | |- B = ( Base ` K ) |
|
| cvrp.j | |- .\/ = ( join ` K ) |
||
| cvrp.m | |- ./\ = ( meet ` K ) |
||
| cvrp.z | |- .0. = ( 0. ` K ) |
||
| cvrp.c | |- C = ( |
||
| cvrp.a | |- A = ( Atoms ` K ) |
||
| Assertion | cvrp | |- ( ( K e. HL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = .0. <-> X C ( X .\/ P ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cvrp.b | |- B = ( Base ` K ) |
|
| 2 | cvrp.j | |- .\/ = ( join ` K ) |
|
| 3 | cvrp.m | |- ./\ = ( meet ` K ) |
|
| 4 | cvrp.z | |- .0. = ( 0. ` K ) |
|
| 5 | cvrp.c | |- C = ( |
|
| 6 | cvrp.a | |- A = ( Atoms ` K ) |
|
| 7 | hlomcmcv | |- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. CvLat ) ) |
|
| 8 | 1 2 3 4 5 6 | cvlcvrp | |- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = .0. <-> X C ( X .\/ P ) ) ) |
| 9 | 7 8 | syl3an1 | |- ( ( K e. HL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = .0. <-> X C ( X .\/ P ) ) ) |