Metamath Proof Explorer


Theorem cvlcvrp

Description: A Hilbert lattice satisfies the covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlcvrp.b
|- B = ( Base ` K )
cvlcvrp.j
|- .\/ = ( join ` K )
cvlcvrp.m
|- ./\ = ( meet ` K )
cvlcvrp.z
|- .0. = ( 0. ` K )
cvlcvrp.c
|- C = ( 
cvlcvrp.a
|- A = ( Atoms ` K )
Assertion cvlcvrp
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = .0. <-> X C ( X .\/ P ) ) )

Proof

Step Hyp Ref Expression
1 cvlcvrp.b
 |-  B = ( Base ` K )
2 cvlcvrp.j
 |-  .\/ = ( join ` K )
3 cvlcvrp.m
 |-  ./\ = ( meet ` K )
4 cvlcvrp.z
 |-  .0. = ( 0. ` K )
5 cvlcvrp.c
 |-  C = ( 
6 cvlcvrp.a
 |-  A = ( Atoms ` K )
7 simp13
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> K e. CvLat )
8 cvllat
 |-  ( K e. CvLat -> K e. Lat )
9 7 8 syl
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> K e. Lat )
10 simp2
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> X e. B )
11 1 6 atbase
 |-  ( P e. A -> P e. B )
12 11 3ad2ant3
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> P e. B )
13 1 3 latmcom
 |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( X ./\ P ) = ( P ./\ X ) )
14 9 10 12 13 syl3anc
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( X ./\ P ) = ( P ./\ X ) )
15 14 eqeq1d
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = .0. <-> ( P ./\ X ) = .0. ) )
16 cvlatl
 |-  ( K e. CvLat -> K e. AtLat )
17 7 16 syl
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> K e. AtLat )
18 simp3
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> P e. A )
19 eqid
 |-  ( le ` K ) = ( le ` K )
20 1 19 3 4 6 atnle
 |-  ( ( K e. AtLat /\ P e. A /\ X e. B ) -> ( -. P ( le ` K ) X <-> ( P ./\ X ) = .0. ) )
21 17 18 10 20 syl3anc
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P ( le ` K ) X <-> ( P ./\ X ) = .0. ) )
22 1 19 2 5 6 cvlcvr1
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P ( le ` K ) X <-> X C ( X .\/ P ) ) )
23 15 21 22 3bitr2d
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = .0. <-> X C ( X .\/ P ) ) )