Theorem helch 5151

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	⊢ ℋ ∈ Cℋ

Proof of Theorem helch

Step	Hyp	Ref	Expression
1		ssid 1519	. . . . . 6 ⊢ ℋ ⊆ ℋ
2		ax-hvzercl 4987	. . . . . 6 ⊢ 0v ∈ ℋ
3	1, 2	pm3.2i 234	. . . . 5 ⊢ ( ℋ ⊆ ℋ ∧ 0v ∈ ℋ )
4		ax-hvaddcl 4984	. . . . . . 7 ⊢ ((x ∈ ℋ ∧ y ∈ ℋ ) → (x +v y) ∈ ℋ )
5	4	rgen2 1248	. . . . . 6 ⊢ ∀x ∈ ℋ ∀y ∈ ℋ (x +v y) ∈ ℋ
6		ax-hvmulcl 4989	. . . . . . 7 ⊢ ((x ∈ ℂ ∧ y ∈ ℋ ) → (x ·s y) ∈ ℋ )
7	6	rgen2a 1264	. . . . . 6 ⊢ ∀x ∈ ℂ ∀y ∈ ℋ (x ·s y) ∈ ℋ
8	5, 7	pm3.2i 234	. . . . 5 ⊢ (∀x ∈ ℋ ∀y ∈ ℋ (x +v y) ∈ ℋ ∧ ∀x ∈ ℂ ∀y ∈ ℋ (x ·s y) ∈ ℋ )
9	3, 8	pm3.2i 234	. . . 4 ⊢ (( ℋ ⊆ ℋ ∧ 0v ∈ ℋ ) ∧ (∀x ∈ ℋ ∀y ∈ ℋ (x +v y) ∈ ℋ ∧ ∀x ∈ ℂ ∀y ∈ ℋ (x ·s y) ∈ ℋ ))
10		sh 5116	. . . 4 ⊢ ( ℋ ∈ Sℋ ↔ (( ℋ ⊆ ℋ ∧ 0v ∈ ℋ ) ∧ (∀x ∈ ℋ ∀y ∈ ℋ (x +v y) ∈ ℋ ∧ ∀x ∈ ℂ ∀y ∈ ℋ (x ·s y) ∈ ℋ )))
11	9, 10	mpbir 165	. . 3 ⊢ ℋ ∈ Sℋ
12		visset 1350	. . . . . 6 ⊢ f ∈ V
13		visset 1350	. . . . . 6 ⊢ x ∈ V
14	12, 13	hlimvec 5110	. . . . 5 ⊢ (f ⇝v x → x ∈ ℋ )
15	14	adantl 305	. . . 4 ⊢ ((f:ℕ–→ ℋ ∧ f ⇝v x) → x ∈ ℋ )
16	15	gen2 681	. . 3 ⊢ ∀f∀x((f:ℕ–→ ℋ ∧ f ⇝v x) → x ∈ ℋ )
17	11, 16	pm3.2i 234	. 2 ⊢ ( ℋ ∈ Sℋ ∧ ∀f∀x((f:ℕ–→ ℋ ∧ f ⇝v x) → x ∈ ℋ ))
18		closedsub 5128	. 2 ⊢ ( ℋ ∈ Cℋ ↔ ( ℋ ∈ Sℋ ∧ ∀f∀x((f:ℕ–→ ℋ ∧ f ⇝v x) → x ∈ ℋ )))
19	17, 18	mpbir 165	1 ⊢ ℋ ∈ Cℋ

Syntax hints:   → wi 2   ∧ wa 196  ∀wal 672   ∈ wcel 1092  ∀wral 1201   ⊆ wss 1487   class class class wbr 2054  –→wf 2418  (class class class)co 3001  ℂcc 4026  ℕcn 4093   ℋ chil 4958   +_v cva 4959   ·_s csm 4960  0_vc0v 4961   ⇝_v chli 4966   S_ℋ csh 4967   C_ℋ cch 4968

This theorem is referenced by:  helsh 5152  pjtht 5240  pjthut 5243  ococt 5253  axpjpjt 5260  pjoc1t 5270  choc1 5292  ococint 5298  hsupval2t 5301  shlubt 5355  chj1 5410  chinclt 5416  chsscon3t 5417  chdmm1t 5438  chjasst 5446  pjoml3t 5517  spansnjt 5540  spansncvt 5543  pjch1t 5560  pjot 5561  pjch0t 5562  pjsslem 5570  pjcjt2 5580  pjcht 5582  ho1 5613  hoid1 5617  hoid1r 5618  pjtot 5644  pjoc 5645  pjclem3 5651  pjopytht 5662  pjnormt 5666  pjnelt 5667  st0 5690  strlem3a 5693  stcltr2 5708  chrelat2t 5761  cvexcht 5763

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077  ax-hilex 4983  ax-hvaddcl 4984  ax-hvzercl 4987  ax-hvmulcl 4989

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-fv 2438  df-opr 3003  df-hlim 5107  df-sh 5114  df-ch 5127

metamath.org