| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > chsh | Structured version Visualization version GIF version | ||
| Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| chsh | ⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isch 31297 | . 2 ⊢ (𝐻 ∈ Cℋ ↔ (𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ (𝐻 ↑m ℕ)) ⊆ 𝐻)) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2113 ⊆ wss 3901 “ cima 5627 (class class class)co 7358 ↑m cmap 8763 ℕcn 12145 ⇝𝑣 chli 31002 Sℋ csh 31003 Cℋ cch 31004 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-xp 5630 df-cnv 5632 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fv 6500 df-ov 7361 df-ch 31296 |
| This theorem is referenced by: chsssh 31300 chshii 31302 ch0 31303 chss 31304 choccl 31381 chjval 31427 chjcl 31432 pjhth 31468 pjhtheu 31469 pjpreeq 31473 pjpjpre 31494 ch0le 31516 chle0 31518 chslej 31573 chjcom 31581 chub1 31582 chlub 31584 chlej1 31585 chlej2 31586 spansnsh 31636 fh1 31693 fh2 31694 chscllem1 31712 chscllem2 31713 chscllem3 31714 chscllem4 31715 chscl 31716 pjorthi 31744 pjoi0 31792 hstoc 32297 hstnmoc 32298 ch1dle 32427 atomli 32457 chirredlem3 32467 sumdmdii 32490 |
| Copyright terms: Public domain | W3C validator |