![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > chshii | Structured version Visualization version GIF version |
Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
chshi.1 | ⊢ 𝐻 ∈ Cℋ |
Ref | Expression |
---|---|
chshii | ⊢ 𝐻 ∈ Sℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chshi.1 | . 2 ⊢ 𝐻 ∈ Cℋ | |
2 | chsh 28421 | . 2 ⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐻 ∈ Sℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2145 Sℋ csh 28125 Cℋ cch 28126 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4576 df-br 4788 df-opab 4848 df-xp 5256 df-cnv 5258 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-iota 5993 df-fv 6038 df-ov 6799 df-ch 28418 |
This theorem is referenced by: chssii 28428 helsh 28442 h0elsh 28453 hhsscms 28476 hhssbn 28477 hhsshl 28478 chocunii 28500 shsleji 28569 shjshcli 28575 pjhthlem1 28590 pjhthlem2 28591 omlsii 28602 ococi 28604 pjoc1i 28630 chne0i 28652 chocini 28653 chjcli 28656 chsleji 28657 chseli 28658 chunssji 28666 chjcomi 28667 chub1i 28668 chlubi 28670 chlej1i 28672 chlej2i 28673 h1de2bi 28753 h1de2ctlem 28754 spansnpji 28777 spanunsni 28778 h1datomi 28780 pjoml2i 28784 qlaxr3i 28835 osumi 28841 osumcor2i 28843 spansnji 28845 spansnm0i 28849 nonbooli 28850 spansncvi 28851 5oai 28860 3oalem2 28862 3oalem5 28865 3oalem6 28866 pjaddii 28874 pjmulii 28876 pjss2i 28879 pjssmii 28880 pj0i 28892 pjocini 28897 pjjsi 28899 pjpythi 28921 mayete3i 28927 pjnmopi 29347 pjimai 29375 pjclem4 29398 pj3si 29406 sto1i 29435 stlei 29439 strlem1 29449 hatomici 29558 hatomistici 29561 atomli 29581 chirredlem3 29591 sumdmdii 29614 sumdmdlem 29617 sumdmdlem2 29618 |
Copyright terms: Public domain | W3C validator |