| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > ax-hilex | Structured version Visualization version GIF version | ||
| Description: This is our first axiom for a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. We assume that there exists a primitive class, ℋ, which contains objects called vectors. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax-hilex | ⊢ ℋ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | chba 30938 | . 2 class ℋ | |
| 2 | cvv 3480 | . 2 class V | |
| 3 | 1, 2 | wcel 2108 | 1 wff ℋ ∈ V |
| Colors of variables: wff setvar class |
| This axiom is referenced by: hvmulex 31030 hilablo 31179 hhph 31197 hcau 31203 hlimadd 31212 hhcms 31222 issh 31227 shex 31231 hlim0 31254 hhssva 31276 hhsssm 31277 hhssnm 31278 hhshsslem1 31286 hhsscms 31297 ocval 31299 spanval 31352 hsupval 31353 sshjval 31369 sshjval3 31373 pjhfval 31415 pjmfn 31734 pjmf1 31735 hosmval 31754 hommval 31755 hodmval 31756 hfsmval 31757 hfmmval 31758 nmopval 31875 elcnop 31876 ellnop 31877 elunop 31891 elhmop 31892 hmopex 31894 nmfnval 31895 nlfnval 31900 elcnfn 31901 ellnfn 31902 dmadjss 31906 dmadjop 31907 adjeu 31908 adjval 31909 eigvecval 31915 eigvalfval 31916 specval 31917 hhcno 31923 hhcnf 31924 adjeq 31954 brafval 31962 kbfval 31971 adjbdln 32102 rnbra 32126 bra11 32127 leoprf2 32146 ishst 32233 |
| Copyright terms: Public domain | W3C validator |