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 ˙ = K
ishlat.s < ˙ = < K
ishlat.j ˙ = join K
ishlat.z 0 ˙ = 0. K
ishlat.u 1 ˙ = 1. K
ishlat.a A = Atoms K
Assertion ishlat3N K HL K OML K CLat K CvLat x A y A z A x ˙ z = y ˙ z 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 1 2 3 4 5 6 7 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 ˙
9 simpll3 K OML K CLat K CvLat x A y A z A K CvLat
10 simplrl K OML K CLat K CvLat x A y A z A x A
11 simplrr K OML K CLat K CvLat x A y A z A y A
12 simpr K OML K CLat K CvLat x A y A z A z A
13 7 2 4 cvlsupr3 K CvLat x A y A z A x ˙ z = y ˙ z x y z x z y z ˙ x ˙ y
14 9 10 11 12 13 syl13anc K OML K CLat K CvLat x A y A z A x ˙ z = y ˙ z x y z x z y z ˙ x ˙ y
15 14 rexbidva K OML K CLat K CvLat x A y A z A x ˙ z = y ˙ z z A x y z x z y z ˙ x ˙ y
16 ne0i x A A
17 16 ad2antrl K OML K CLat K CvLat x A y A A
18 r19.37zv A z A x y z x z y z ˙ x ˙ y x y z A z x z y z ˙ x ˙ y
19 17 18 syl K OML K CLat K CvLat x A y A z A x y z x z y z ˙ x ˙ y x y z A z x z y z ˙ x ˙ y
20 15 19 bitr2d K OML K CLat K CvLat x A y A x y z A z x z y z ˙ x ˙ y z A x ˙ z = y ˙ z
21 20 2ralbidva K OML K CLat K CvLat x A y A x y z A z x z y z ˙ x ˙ y x A y A z A x ˙ z = y ˙ z
22 21 anbi1d 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 ˙ x A y A z A x ˙ z = y ˙ z x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
23 22 pm5.32i 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 K CLat K CvLat x A y A z A x ˙ z = y ˙ z x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
24 8 23 bitri K HL K OML K CLat K CvLat x A y A z A x ˙ z = y ˙ z x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙