This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )