![]() |
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 28598 | . 2 ⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐻 ∈ Sℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 Sℋ csh 28302 Cℋ cch 28303 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-rex 3093 df-rab 3096 df-v 3385 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-xp 5316 df-cnv 5318 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-iota 6062 df-fv 6107 df-ov 6879 df-ch 28595 |
This theorem is referenced by: chssii 28605 helsh 28619 h0elsh 28630 hhsscms 28653 hhssbnOLD 28654 hhsshlOLD 28655 chocunii 28677 shsleji 28746 shjshcli 28752 pjhthlem1 28767 pjhthlem2 28768 omlsii 28779 ococi 28781 pjoc1i 28807 chne0i 28829 chocini 28830 chjcli 28833 chsleji 28834 chseli 28835 chunssji 28843 chjcomi 28844 chub1i 28845 chlubi 28847 chlej1i 28849 chlej2i 28850 h1de2bi 28930 h1de2ctlem 28931 spansnpji 28954 spanunsni 28955 h1datomi 28957 pjoml2i 28961 qlaxr3i 29012 osumi 29018 osumcor2i 29020 spansnji 29022 spansnm0i 29026 nonbooli 29027 spansncvi 29028 5oai 29037 3oalem2 29039 3oalem5 29042 3oalem6 29043 pjaddii 29051 pjmulii 29053 pjss2i 29056 pjssmii 29057 pj0i 29069 pjocini 29074 pjjsi 29076 pjpythi 29098 mayete3i 29104 pjnmopi 29524 pjimai 29552 pjclem4 29575 pj3si 29583 sto1i 29612 stlei 29616 strlem1 29626 hatomici 29735 hatomistici 29738 atomli 29758 chirredlem3 29768 sumdmdii 29791 sumdmdlem 29794 sumdmdlem2 29795 |
Copyright terms: Public domain | W3C validator |