![]() |
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 | chil 28115 | . 2 class ℋ | |
2 | cvv 3351 | . 2 class V | |
3 | 1, 2 | wcel 2145 | 1 wff ℋ ∈ V |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmulex 28207 hilablo 28356 hhph 28374 hcau 28380 hlimadd 28389 hhcms 28399 issh 28404 shex 28408 hlim0 28431 hhssva 28453 hhsssm 28454 hhssnm 28455 hhshsslem1 28463 hhsscms 28475 ocval 28478 spanval 28531 hsupval 28532 sshjval 28548 sshjval3 28552 pjhfval 28594 pjmfn 28913 pjmf1 28914 hosmval 28933 hommval 28934 hodmval 28935 hfsmval 28936 hfmmval 28937 nmopval 29054 elcnop 29055 ellnop 29056 elunop 29070 elhmop 29071 hmopex 29073 nmfnval 29074 nlfnval 29079 elcnfn 29080 ellnfn 29081 dmadjss 29085 dmadjop 29086 adjeu 29087 adjval 29088 eigvecval 29094 eigvalfval 29095 specval 29096 hhcno 29102 hhcnf 29103 adjeq 29133 brafval 29141 kbfval 29150 adjbdln 29281 rnbra 29305 bra11 29306 leoprf2 29325 ishst 29412 |
Copyright terms: Public domain | W3C validator |