Metamath Proof Explorer

Theorem ishlat3N

Description: The predicate "is a Hilbert lattice". Note that the superposition principle is expressed in the compact form E. z e. A ( x .\/ z ) = ( y .\/ z ) . The exchange property and atomicity are provided by K e. CvLat , and "minimum height 4" is shown explicitly. (Contributed by NM, 8-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses ishlat.b 
|- B = ( Base ` K )
ishlat.l 
|- .<_ = ( le ` K )
ishlat.s 
|- .< = ( lt ` K )
ishlat.j 
|- .\/ = ( join ` K )
ishlat.z 
|- .0. = ( 0. ` K )
ishlat.u 
|- .1. = ( 1. ` K )
ishlat.a 
|- A = ( Atoms ` K )
Assertion ishlat3N 
|- ( K e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( A. x e. A A. y e. A E. z e. A ( x .\/ z ) = ( y .\/ z ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ishlat.b 
 |-  B = ( Base ` K )
2 ishlat.l 
 |-  .<_ = ( le ` K )
3 ishlat.s 
 |-  .< = ( lt ` K )
4 ishlat.j 
 |-  .\/ = ( join ` K )
5 ishlat.z 
 |-  .0. = ( 0. ` K )
6 ishlat.u 
 |-  .1. = ( 1. ` K )
7 ishlat.a 
 |-  A = ( Atoms ` K )
8 1 2 3 4 5 6 7 ishlat1 
 |-  ( K e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( A. x e. A A. y e. A ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )
9 simpll3 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> K e. CvLat )
10 simplrl 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> x e. A )
11 simplrr 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> y e. A )
12 simpr 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> z e. A )
13 7 2 4 cvlsupr3 
 |-  ( ( K e. CvLat /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x .\/ z ) = ( y .\/ z ) <-> ( x =/= y -> ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) ) )
14 9 10 11 12 13 syl13anc 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> ( ( x .\/ z ) = ( y .\/ z ) <-> ( x =/= y -> ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) ) )
15 14 rexbidva 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) -> ( E. z e. A ( x .\/ z ) = ( y .\/ z ) <-> E. z e. A ( x =/= y -> ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) ) )
16 ne0i 
 |-  ( x e. A -> A =/= (/) )
17 16 ad2antrl 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) -> A =/= (/) )
18 r19.37zv 
 |-  ( A =/= (/) -> ( E. z e. A ( x =/= y -> ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) <-> ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) ) )
19 17 18 syl 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) -> ( E. z e. A ( x =/= y -> ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) <-> ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) ) )
20 15 19 bitr2d 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( x e. A /\ y e. A ) ) -> ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) <-> E. z e. A ( x .\/ z ) = ( y .\/ z ) ) )
21 20 2ralbidva 
 |-  ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) -> ( A. x e. A A. y e. A ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) <-> A. x e. A A. y e. A E. z e. A ( x .\/ z ) = ( y .\/ z ) ) )
22 21 anbi1d 
 |-  ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) -> ( ( A. x e. A A. y e. A ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) <-> ( A. x e. A A. y e. A E. z e. A ( x .\/ z ) = ( y .\/ z ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )
23 22 pm5.32i 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( A. x e. A A. y e. A ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) <-> ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( A. x e. A A. y e. A E. z e. A ( x .\/ z ) = ( y .\/ z ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )
24 8 23 bitri 
 |-  ( K e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( A. x e. A A. y e. A E. z e. A ( x .\/ z ) = ( y .\/ z ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )