Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ishlat1 Structured version   Visualization version   GIF version

Theorem ishlat1 39334
Description: The predicate "is a Hilbert lattice", which is: is orthomodular (𝐾 ∈ OML), complete (𝐾 ∈ CLat), atomic and satisfies the exchange (or covering) property (𝐾 ∈ 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.)
Hypotheses
Ref Expression
ishlat.b 𝐵 = (Base‘𝐾)
ishlat.l = (le‘𝐾)
ishlat.s < = (lt‘𝐾)
ishlat.j = (join‘𝐾)
ishlat.z 0 = (0.‘𝐾)
ishlat.u 1 = (1.‘𝐾)
ishlat.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
ishlat1 (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 )))))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐾,𝑦,𝑧
Allowed substitution hints:   < (𝑥,𝑦,𝑧)   1 (𝑥,𝑦,𝑧)   (𝑥,𝑦,𝑧)   (𝑥,𝑦,𝑧)   0 (𝑥,𝑦,𝑧)

Proof of Theorem ishlat1
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6907 . . . . . 6 (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾))
2 ishlat.a . . . . . 6 𝐴 = (Atoms‘𝐾)
31, 2eqtr4di 2793 . . . . 5 (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴)
4 fveq2 6907 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
5 ishlat.l . . . . . . . . . . . 12 = (le‘𝐾)
64, 5eqtr4di 2793 . . . . . . . . . . 11 (𝑘 = 𝐾 → (le‘𝑘) = )
76breqd 5159 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦) ↔ 𝑧 (𝑥(join‘𝑘)𝑦)))
8 fveq2 6907 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾))
9 ishlat.j . . . . . . . . . . . . 13 = (join‘𝐾)
108, 9eqtr4di 2793 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (join‘𝑘) = )
1110oveqd 7448 . . . . . . . . . . 11 (𝑘 = 𝐾 → (𝑥(join‘𝑘)𝑦) = (𝑥 𝑦))
1211breq2d 5160 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑧 (𝑥(join‘𝑘)𝑦) ↔ 𝑧 (𝑥 𝑦)))
137, 12bitrd 279 . . . . . . . . 9 (𝑘 = 𝐾 → (𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦) ↔ 𝑧 (𝑥 𝑦)))
14133anbi3d 1441 . . . . . . . 8 (𝑘 = 𝐾 → ((𝑧𝑥𝑧𝑦𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦)) ↔ (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))))
153, 14rexeqbidv 3345 . . . . . . 7 (𝑘 = 𝐾 → (∃𝑧 ∈ (Atoms‘𝑘)(𝑧𝑥𝑧𝑦𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦)) ↔ ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))))
1615imbi2d 340 . . . . . 6 (𝑘 = 𝐾 → ((𝑥𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧𝑥𝑧𝑦𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦)))))
173, 16raleqbidv 3344 . . . . 5 (𝑘 = 𝐾 → (∀𝑦 ∈ (Atoms‘𝑘)(𝑥𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧𝑥𝑧𝑦𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ ∀𝑦𝐴 (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦)))))
183, 17raleqbidv 3344 . . . 4 (𝑘 = 𝐾 → (∀𝑥 ∈ (Atoms‘𝑘)∀𝑦 ∈ (Atoms‘𝑘)(𝑥𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧𝑥𝑧𝑦𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦)))))
19 fveq2 6907 . . . . . 6 (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
20 ishlat.b . . . . . 6 𝐵 = (Base‘𝐾)
2119, 20eqtr4di 2793 . . . . 5 (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
22 fveq2 6907 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (lt‘𝑘) = (lt‘𝐾))
23 ishlat.s . . . . . . . . . . . 12 < = (lt‘𝐾)
2422, 23eqtr4di 2793 . . . . . . . . . . 11 (𝑘 = 𝐾 → (lt‘𝑘) = < )
2524breqd 5159 . . . . . . . . . 10 (𝑘 = 𝐾 → ((0.‘𝑘)(lt‘𝑘)𝑥 ↔ (0.‘𝑘) < 𝑥))
26 fveq2 6907 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (0.‘𝑘) = (0.‘𝐾))
27 ishlat.z . . . . . . . . . . . 12 0 = (0.‘𝐾)
2826, 27eqtr4di 2793 . . . . . . . . . . 11 (𝑘 = 𝐾 → (0.‘𝑘) = 0 )
2928breq1d 5158 . . . . . . . . . 10 (𝑘 = 𝐾 → ((0.‘𝑘) < 𝑥0 < 𝑥))
3025, 29bitrd 279 . . . . . . . . 9 (𝑘 = 𝐾 → ((0.‘𝑘)(lt‘𝑘)𝑥0 < 𝑥))
3124breqd 5159 . . . . . . . . 9 (𝑘 = 𝐾 → (𝑥(lt‘𝑘)𝑦𝑥 < 𝑦))
3230, 31anbi12d 632 . . . . . . . 8 (𝑘 = 𝐾 → (((0.‘𝑘)(lt‘𝑘)𝑥𝑥(lt‘𝑘)𝑦) ↔ ( 0 < 𝑥𝑥 < 𝑦)))
3324breqd 5159 . . . . . . . . 9 (𝑘 = 𝐾 → (𝑦(lt‘𝑘)𝑧𝑦 < 𝑧))
3424breqd 5159 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑧(lt‘𝑘)(1.‘𝑘) ↔ 𝑧 < (1.‘𝑘)))
35 fveq2 6907 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (1.‘𝑘) = (1.‘𝐾))
36 ishlat.u . . . . . . . . . . . 12 1 = (1.‘𝐾)
3735, 36eqtr4di 2793 . . . . . . . . . . 11 (𝑘 = 𝐾 → (1.‘𝑘) = 1 )
3837breq2d 5160 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑧 < (1.‘𝑘) ↔ 𝑧 < 1 ))
3934, 38bitrd 279 . . . . . . . . 9 (𝑘 = 𝐾 → (𝑧(lt‘𝑘)(1.‘𝑘) ↔ 𝑧 < 1 ))
4033, 39anbi12d 632 . . . . . . . 8 (𝑘 = 𝐾 → ((𝑦(lt‘𝑘)𝑧𝑧(lt‘𝑘)(1.‘𝑘)) ↔ (𝑦 < 𝑧𝑧 < 1 )))
4132, 40anbi12d 632 . . . . . . 7 (𝑘 = 𝐾 → ((((0.‘𝑘)(lt‘𝑘)𝑥𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧𝑧(lt‘𝑘)(1.‘𝑘))) ↔ (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 ))))
4221, 41rexeqbidv 3345 . . . . . 6 (𝑘 = 𝐾 → (∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧𝑧(lt‘𝑘)(1.‘𝑘))) ↔ ∃𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 ))))
4321, 42rexeqbidv 3345 . . . . 5 (𝑘 = 𝐾 → (∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧𝑧(lt‘𝑘)(1.‘𝑘))) ↔ ∃𝑦𝐵𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 ))))
4421, 43rexeqbidv 3345 . . . 4 (𝑘 = 𝐾 → (∃𝑥 ∈ (Base‘𝑘)∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧𝑧(lt‘𝑘)(1.‘𝑘))) ↔ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 ))))
4518, 44anbi12d 632 . . 3 (𝑘 = 𝐾 → ((∀𝑥 ∈ (Atoms‘𝑘)∀𝑦 ∈ (Atoms‘𝑘)(𝑥𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧𝑥𝑧𝑦𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ∧ ∃𝑥 ∈ (Base‘𝑘)∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧𝑧(lt‘𝑘)(1.‘𝑘)))) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 )))))
46 df-hlat 39333 . . 3 HL = {𝑘 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑥 ∈ (Atoms‘𝑘)∀𝑦 ∈ (Atoms‘𝑘)(𝑥𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧𝑥𝑧𝑦𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ∧ ∃𝑥 ∈ (Base‘𝑘)∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧𝑧(lt‘𝑘)(1.‘𝑘))))}
4745, 46elrab2 3698 . 2 (𝐾 ∈ HL ↔ (𝐾 ∈ ((OML ∩ CLat) ∩ CvLat) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 )))))
48 elin 3979 . . . . 5 (𝐾 ∈ (OML ∩ CLat) ↔ (𝐾 ∈ OML ∧ 𝐾 ∈ CLat))
4948anbi1i 624 . . . 4 ((𝐾 ∈ (OML ∩ CLat) ∧ 𝐾 ∈ CvLat) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ CvLat))
50 elin 3979 . . . 4 (𝐾 ∈ ((OML ∩ CLat) ∩ CvLat) ↔ (𝐾 ∈ (OML ∩ CLat) ∧ 𝐾 ∈ CvLat))
51 df-3an 1088 . . . 4 ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ CvLat))
5249, 50, 513bitr4ri 304 . . 3 ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ↔ 𝐾 ∈ ((OML ∩ CLat) ∩ CvLat))
5352anbi1i 624 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 )))) ↔ (𝐾 ∈ ((OML ∩ CLat) ∩ CvLat) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 )))))
5447, 53bitr4i 278 1 (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (( 0 < 𝑥𝑥 < 𝑦) ∧ (𝑦 < 𝑧𝑧 < 1 )))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wral 3059  wrex 3068  cin 3962   class class class wbr 5148  cfv 6563  (class class class)co 7431  Basecbs 17245  lecple 17305  ltcplt 18366  joincjn 18369  0.cp0 18481  1.cp1 18482  CLatccla 18556  OMLcoml 39157  Atomscatm 39245  CvLatclc 39247  HLchlt 39332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-hlat 39333
This theorem is referenced by:  ishlat2  39335  ishlat3N  39336  hlomcmcv  39338
  Copyright terms: Public domain W3C validator