Metamath Proof Explorer

Theorem ishlat1

Description: The predicate "is a Hilbert lattice", which is: is orthomodular ( K e. OML ), complete ( K e. CLat ), atomic and satisfies the exchange (or covering) property ( K e. CvLat ), satisfies the superposition principle, and has a minimum height of 4 (witnessed here by 0, x, y, z, 1). (Contributed by NM, 5-Nov-2012)

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

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 fveq2 
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
9 8 7 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
10 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
11 10 2 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
12 11 breqd 
 |-  ( k = K -> ( z ( le ` k ) ( x ( join ` k ) y ) <-> z .<_ ( x ( join ` k ) y ) ) )
13 fveq2 
 |-  ( k = K -> ( join ` k ) = ( join ` K ) )
14 13 4 eqtr4di 
 |-  ( k = K -> ( join ` k ) = .\/ )
15 14 oveqd 
 |-  ( k = K -> ( x ( join ` k ) y ) = ( x .\/ y ) )
16 15 breq2d 
 |-  ( k = K -> ( z .<_ ( x ( join ` k ) y ) <-> z .<_ ( x .\/ y ) ) )
17 12 16 bitrd 
 |-  ( k = K -> ( z ( le ` k ) ( x ( join ` k ) y ) <-> z .<_ ( x .\/ y ) ) )
18 17 3anbi3d 
 |-  ( k = K -> ( ( z =/= x /\ z =/= y /\ z ( le ` k ) ( x ( join ` k ) y ) ) <-> ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) )
19 9 18 rexeqbidv 
 |-  ( k = K -> ( E. z e. ( Atoms ` k ) ( z =/= x /\ z =/= y /\ z ( le ` k ) ( x ( join ` k ) y ) ) <-> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) )
20 19 imbi2d 
 |-  ( k = K -> ( ( x =/= y -> E. z e. ( Atoms ` k ) ( z =/= x /\ z =/= y /\ z ( le ` k ) ( x ( join ` k ) y ) ) ) <-> ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) ) )
21 9 20 raleqbidv 
 |-  ( k = K -> ( A. y e. ( Atoms ` k ) ( x =/= y -> E. z e. ( Atoms ` k ) ( z =/= x /\ z =/= y /\ z ( le ` k ) ( x ( join ` k ) y ) ) ) <-> A. y e. A ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) ) )
22 9 21 raleqbidv 
 |-  ( k = K -> ( A. x e. ( Atoms ` k ) A. y e. ( Atoms ` k ) ( x =/= y -> E. z e. ( Atoms ` k ) ( z =/= x /\ z =/= y /\ z ( le ` k ) ( x ( join ` k ) y ) ) ) <-> A. x e. A A. y e. A ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) ) )
23 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
24 23 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
25 fveq2 
 |-  ( k = K -> ( lt ` k ) = ( lt ` K ) )
26 25 3 eqtr4di 
 |-  ( k = K -> ( lt ` k ) = .< )
27 26 breqd 
 |-  ( k = K -> ( ( 0. ` k ) ( lt ` k ) x <-> ( 0. ` k ) .< x ) )
28 fveq2 
 |-  ( k = K -> ( 0. ` k ) = ( 0. ` K ) )
29 28 5 eqtr4di 
 |-  ( k = K -> ( 0. ` k ) = .0. )
30 29 breq1d 
 |-  ( k = K -> ( ( 0. ` k ) .< x <-> .0. .< x ) )
31 27 30 bitrd 
 |-  ( k = K -> ( ( 0. ` k ) ( lt ` k ) x <-> .0. .< x ) )
32 26 breqd 
 |-  ( k = K -> ( x ( lt ` k ) y <-> x .< y ) )
33 31 32 anbi12d 
 |-  ( k = K -> ( ( ( 0. ` k ) ( lt ` k ) x /\ x ( lt ` k ) y ) <-> ( .0. .< x /\ x .< y ) ) )
34 26 breqd 
 |-  ( k = K -> ( y ( lt ` k ) z <-> y .< z ) )
35 26 breqd 
 |-  ( k = K -> ( z ( lt ` k ) ( 1. ` k ) <-> z .< ( 1. ` k ) ) )
36 fveq2 
 |-  ( k = K -> ( 1. ` k ) = ( 1. ` K ) )
37 36 6 eqtr4di 
 |-  ( k = K -> ( 1. ` k ) = .1. )
38 37 breq2d 
 |-  ( k = K -> ( z .< ( 1. ` k ) <-> z .< .1. ) )
39 35 38 bitrd 
 |-  ( k = K -> ( z ( lt ` k ) ( 1. ` k ) <-> z .< .1. ) )
40 34 39 anbi12d 
 |-  ( k = K -> ( ( y ( lt ` k ) z /\ z ( lt ` k ) ( 1. ` k ) ) <-> ( y .< z /\ z .< .1. ) ) )
41 33 40 anbi12d 
 |-  ( k = K -> ( ( ( ( 0. ` k ) ( lt ` k ) x /\ x ( lt ` k ) y ) /\ ( y ( lt ` k ) z /\ z ( lt ` k ) ( 1. ` k ) ) ) <-> ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) )
42 24 41 rexeqbidv 
 |-  ( k = K -> ( E. z e. ( Base ` k ) ( ( ( 0. ` k ) ( lt ` k ) x /\ x ( lt ` k ) y ) /\ ( y ( lt ` k ) z /\ z ( lt ` k ) ( 1. ` k ) ) ) <-> E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) )
43 24 42 rexeqbidv 
 |-  ( k = K -> ( E. y e. ( Base ` k ) E. z e. ( Base ` k ) ( ( ( 0. ` k ) ( lt ` k ) x /\ x ( lt ` k ) y ) /\ ( y ( lt ` k ) z /\ z ( lt ` k ) ( 1. ` k ) ) ) <-> E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) )
44 24 43 rexeqbidv 
 |-  ( k = K -> ( E. x e. ( Base ` k ) E. y e. ( Base ` k ) E. z e. ( Base ` k ) ( ( ( 0. ` k ) ( lt ` k ) x /\ x ( lt ` k ) y ) /\ ( y ( lt ` k ) z /\ z ( lt ` k ) ( 1. ` k ) ) ) <-> E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) )
45 22 44 anbi12d 
 |-  ( k = K -> ( ( A. x e. ( Atoms ` k ) A. y e. ( Atoms ` k ) ( x =/= y -> E. z e. ( Atoms ` k ) ( z =/= x /\ z =/= y /\ z ( le ` k ) ( x ( join ` k ) y ) ) ) /\ E. x e. ( Base ` k ) E. y e. ( Base ` k ) E. z e. ( Base ` k ) ( ( ( 0. ` k ) ( lt ` k ) x /\ x ( lt ` k ) y ) /\ ( y ( lt ` k ) z /\ z ( lt ` k ) ( 1. ` k ) ) ) ) <-> ( 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. ) ) ) ) )
46 df-hlat 
 |-  HL = { k e. ( ( OML i^i CLat ) i^i CvLat ) | ( A. x e. ( Atoms ` k ) A. y e. ( Atoms ` k ) ( x =/= y -> E. z e. ( Atoms ` k ) ( z =/= x /\ z =/= y /\ z ( le ` k ) ( x ( join ` k ) y ) ) ) /\ E. x e. ( Base ` k ) E. y e. ( Base ` k ) E. z e. ( Base ` k ) ( ( ( 0. ` k ) ( lt ` k ) x /\ x ( lt ` k ) y ) /\ ( y ( lt ` k ) z /\ z ( lt ` k ) ( 1. ` k ) ) ) ) }
47 45 46 elrab2 
 |-  ( K e. HL <-> ( K e. ( ( OML i^i CLat ) i^i 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. ) ) ) ) )
48 elin 
 |-  ( K e. ( OML i^i CLat ) <-> ( K e. OML /\ K e. CLat ) )
49 48 anbi1i 
 |-  ( ( K e. ( OML i^i CLat ) /\ K e. CvLat ) <-> ( ( K e. OML /\ K e. CLat ) /\ K e. CvLat ) )
50 elin 
 |-  ( K e. ( ( OML i^i CLat ) i^i CvLat ) <-> ( K e. ( OML i^i CLat ) /\ K e. CvLat ) )
51 df-3an 
 |-  ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) <-> ( ( K e. OML /\ K e. CLat ) /\ K e. CvLat ) )
52 49 50 51 3bitr4ri 
 |-  ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) <-> K e. ( ( OML i^i CLat ) i^i CvLat ) )
53 52 anbi1i 
 |-  ( ( ( 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 i^i CLat ) i^i 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. ) ) ) ) )
54 47 53 bitr4i 
 |-  ( 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. ) ) ) ) )