Theorem helch 10749

Description: The unit Hilbert lattice element (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of [Kalmbach] p. 65.

Assertion

Ref	Expression
helch	|- ~H e. CH

Proof of Theorem helch

Step	Hyp	Ref	Expression
1		closedsub 10726	. 2 |- (~H e. CH <-> (~H e. SH /\ A.fA.x((f:NN-->~H /\ f ~~>v x) -> x e. ~H)))
2		sh 10711	. . 3 |- (~H e. SH <-> ((~H C_ ~H /\ 0h e. ~H) /\ (A.x e. ~H A.y e. ~H (x +h y) e. ~H /\ A.x e. CC A.y e. ~H (x .h y) e. ~H)))
3		ssid 2634	. . . 4 |- ~H C_ ~H
4		ax-hv0cl 10505	. . . 4 |- 0h e. ~H
5	3, 4	pm3.2i 307	. . 3 |- (~H C_ ~H /\ 0h e. ~H)
6		hvaddcl 10514	. . . . 5 |- ((x e. ~H /\ y e. ~H) -> (x +h y) e. ~H)
7	6	rgen2a 2160	. . . 4 |- A.x e. ~H A.y e. ~H (x +h y) e. ~H
8		hvmulcl 10515	. . . . 5 |- ((x e. CC /\ y e. ~H) -> (x .h y) e. ~H)
9	8	rgen2 2186	. . . 4 |- A.x e. CC A.y e. ~H (x .h y) e. ~H
10	7, 9	pm3.2i 307	. . 3 |- (A.x e. ~H A.y e. ~H (x +h y) e. ~H /\ A.x e. CC A.y e. ~H (x .h y) e. ~H)
11	2, 5, 10	mpbir2an 800	. 2 |- ~H e. SH
12		visset 2295	. . . . 5 |- f e. _V
13		visset 2295	. . . . 5 |- x e. _V
14	12, 13	hlimveci 10691	. . . 4 |- (f ~~>v x -> x e. ~H)
15	14	adantl 424	. . 3 |- ((f:NN-->~H /\ f ~~>v x) -> x e. ~H)
16	15	gen2 1329	. 2 |- A.fA.x((f:NN-->~H /\ f ~~>v x) -> x e. ~H)
17	1, 11, 16	mpbir2an 800	1 |- ~H e. CH

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   e. wcel 1300  A.wral 2105   C_ wss 2593   class class class wbr 3338  -->wf 3994  (class class class)co 4884  CCcc 6384  NNcn 6449  ~Hchil 10420   +h cva 10421   .h csm 10422  0hc0v 10423   ~~>v chli 10428  SHcsh 10429  CHcch 10430

This theorem is referenced by:  helsh 10750  pjth 10867  pjtheu 10869  ococ 10881  axpjpj 10889  pjoc1 10900  ococin 10930  hsupval2 10933  shlub 10987  chj1i 11045  chincl 11055  chsscon3 11056  chjo 11071  chdmm1 11081  chjass 11089  hne0 11103  pjoml3 11188  osum 11223  spansnj 11227  spansncv 11233  pjch1 11250  pjo 11251  pjsslem 11259  pjcjt2 11272  pjch 11274  pjopyth 11300  pjnorm 11304  pjpyth 11305  pjnel 11306  ho0val 11313  dfiop2 11316  hoid1i 11352  hoid1ri 11353  pjtoi 11751  pjoci 11752  pjclem3 11770  hst0 11805  st0 11821  strlem3a 11824  hstrlem3a 11832  stcltr2i 11847  cvmd 11908  chrelat2 11942  cvexch 11946  mdsym 11984

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-hilex 10501  ax-hfvadd 10502  ax-hv0cl 10505  ax-hfvmul 10507

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-hlim 10473  df-sh 10709  df-ch 10725

Copyright terms: Public domain