| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > helch | Structured version Visualization version GIF version | ||
| Description: The Hilbert lattice one (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 6-Sep-1999.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| helch | ⊢ ℋ ∈ Cℋ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssid 3956 | . . . 4 ⊢ ℋ ⊆ ℋ | |
| 2 | ax-hv0cl 31162 | . . . 4 ⊢ 0ℎ ∈ ℋ | |
| 3 | 1, 2 | pm3.2i 474 | . . 3 ⊢ ( ℋ ⊆ ℋ ∧ 0ℎ ∈ ℋ) |
| 4 | hvaddcl 31171 | . . . . 5 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 +ℎ 𝑦) ∈ ℋ) | |
| 5 | 4 | rgen2 3201 | . . . 4 ⊢ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 +ℎ 𝑦) ∈ ℋ |
| 6 | hvmulcl 31172 | . . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥 ·ℎ 𝑦) ∈ ℋ) | |
| 7 | 6 | rgen2 3201 | . . . 4 ⊢ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ (𝑥 ·ℎ 𝑦) ∈ ℋ |
| 8 | 5, 7 | pm3.2i 474 | . . 3 ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 +ℎ 𝑦) ∈ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ (𝑥 ·ℎ 𝑦) ∈ ℋ) |
| 9 | issh2 31368 | . . 3 ⊢ ( ℋ ∈ Sℋ ↔ (( ℋ ⊆ ℋ ∧ 0ℎ ∈ ℋ) ∧ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 +ℎ 𝑦) ∈ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ (𝑥 ·ℎ 𝑦) ∈ ℋ))) | |
| 10 | 3, 8, 9 | mpbir2an 721 | . 2 ⊢ ℋ ∈ Sℋ |
| 11 | vex 3457 | . . . . 5 ⊢ 𝑥 ∈ V | |
| 12 | 11 | hlimveci 31349 | . . . 4 ⊢ (𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ ℋ) |
| 13 | 12 | adantl 485 | . . 3 ⊢ ((𝑓:ℕ⟶ ℋ ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ℋ) |
| 14 | 13 | gen2 1815 | . 2 ⊢ ∀𝑓∀𝑥((𝑓:ℕ⟶ ℋ ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ℋ) |
| 15 | isch2 31382 | . 2 ⊢ ( ℋ ∈ Cℋ ↔ ( ℋ ∈ Sℋ ∧ ∀𝑓∀𝑥((𝑓:ℕ⟶ ℋ ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ℋ))) | |
| 16 | 10, 14, 15 | mpbir2an 721 | 1 ⊢ ℋ ∈ Cℋ |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 399 ∀wal 1557 ∈ wcel 2141 ∀wral 3075 ⊆ wss 3902 class class class wbr 5097 ⟶wf 6511 (class class class)co 7390 ℂcc 11064 ℕcn 12203 ℋchba 31078 +ℎ cva 31079 ·ℎ csm 31080 0ℎc0v 31083 ⇝𝑣 chli 31086 Sℋ csh 31087 Cℋ cch 31088 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-cnex 11122 ax-1cn 11124 ax-addcl 11126 ax-hilex 31158 ax-hfvadd 31159 ax-hv0cl 31162 ax-hfvmul 31164 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-map 8803 df-nn 12204 df-hlim 31131 df-sh 31366 df-ch 31380 |
| This theorem is referenced by: ifchhv 31403 helsh 31404 ococin 31567 chj1i 31648 hne0 31706 pjch1 31829 pjo 31830 pjsslem 31838 ho0val 31909 dfiop2 31912 hoid1i 31948 hoid1ri 31949 pjtoi 32338 pjoci 32339 pjclem3 32356 hst0 32392 st0 32408 strlem3a 32411 hstrlem3a 32419 stcltr2i 32434 |
| Copyright terms: Public domain | W3C validator |