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 ˙ = K
ishlat.s < ˙ = < K
ishlat.j ˙ = join K
ishlat.z 0 ˙ = 0. K
ishlat.u 1 ˙ = 1. K
ishlat.a A = Atoms K
Assertion ishlat1 K HL K OML K CLat K CvLat x A y A x y z A z x z y z ˙ x ˙ y x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙

Proof

Step Hyp Ref Expression
1 ishlat.b B = Base K
2 ishlat.l ˙ = K
3 ishlat.s < ˙ = < 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 k = K
11 10 2 eqtr4di k = K k = ˙
12 11 breqd k = K z 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 k x join k y z ˙ x ˙ y
18 17 3anbi3d k = K z x z y z k x join k y z x z y z ˙ x ˙ y
19 9 18 rexeqbidv k = K z Atoms k z x z y z k x join k y z A z x z y z ˙ x ˙ y
20 19 imbi2d k = K x y z Atoms k z x z y z k x join k y x y z A z x z y z ˙ x ˙ y
21 9 20 raleqbidv k = K y Atoms k x y z Atoms k z x z y z k x join k y y A x y z A z x z y z ˙ x ˙ y
22 9 21 raleqbidv k = K x Atoms k y Atoms k x y z Atoms k z x z y z k x join k y x A y A x y z 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 < k = < K
26 25 3 eqtr4di k = K < k = < ˙
27 26 breqd k = K 0. k < 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 < k x 0 ˙ < ˙ x
32 26 breqd k = K x < k y x < ˙ y
33 31 32 anbi12d k = K 0. k < k x x < k y 0 ˙ < ˙ x x < ˙ y
34 26 breqd k = K y < k z y < ˙ z
35 26 breqd k = K z < 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 < k 1. k z < ˙ 1 ˙
40 34 39 anbi12d k = K y < k z z < k 1. k y < ˙ z z < ˙ 1 ˙
41 33 40 anbi12d k = K 0. k < k x x < k y y < k z z < k 1. k 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
42 24 41 rexeqbidv k = K z Base k 0. k < k x x < k y y < k z z < k 1. k z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
43 24 42 rexeqbidv k = K y Base k z Base k 0. k < k x x < k y y < k z z < k 1. k y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
44 24 43 rexeqbidv k = K x Base k y Base k z Base k 0. k < k x x < k y y < k z z < k 1. k x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
45 22 44 anbi12d k = K x Atoms k y Atoms k x y z Atoms k z x z y z k x join k y x Base k y Base k z Base k 0. k < k x x < k y y < k z z < k 1. k x A y A x y z A z x z y z ˙ x ˙ y x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
46 df-hlat HL = k OML CLat CvLat | x Atoms k y Atoms k x y z Atoms k z x z y z k x join k y x Base k y Base k z Base k 0. k < k x x < k y y < k z z < k 1. k
47 45 46 elrab2 K HL K OML CLat CvLat x A y A x y z A z x z y z ˙ x ˙ y x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
48 elin K OML CLat K OML K CLat
49 48 anbi1i K OML CLat K CvLat K OML K CLat K CvLat
50 elin K OML CLat CvLat K OML CLat K CvLat
51 df-3an K OML K CLat K CvLat K OML K CLat K CvLat
52 49 50 51 3bitr4ri K OML K CLat K CvLat K OML CLat CvLat
53 52 anbi1i K OML K CLat K CvLat x A y A x y z A z x z y z ˙ x ˙ y x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙ K OML CLat CvLat x A y A x y z A z x z y z ˙ x ˙ y x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
54 47 53 bitr4i K HL K OML K CLat K CvLat x A y A x y z A z x z y z ˙ x ˙ y x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙