![]() |
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 28352 | . 2 class ℋ | |
2 | cvv 3398 | . 2 class V | |
3 | 1, 2 | wcel 2107 | 1 wff ℋ ∈ V |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmulex 28444 hilablo 28593 hhph 28611 hcau 28617 hlimadd 28626 hhcms 28636 issh 28641 shex 28645 hlim0 28668 hhssva 28690 hhsssm 28691 hhssnm 28692 hhshsslem1 28700 hhsscms 28712 ocval 28715 spanval 28768 hsupval 28769 sshjval 28785 sshjval3 28789 pjhfval 28831 pjmfn 29150 pjmf1 29151 hosmval 29170 hommval 29171 hodmval 29172 hfsmval 29173 hfmmval 29174 nmopval 29291 elcnop 29292 ellnop 29293 elunop 29307 elhmop 29308 hmopex 29310 nmfnval 29311 nlfnval 29316 elcnfn 29317 ellnfn 29318 dmadjss 29322 dmadjop 29323 adjeu 29324 adjval 29325 eigvecval 29331 eigvalfval 29332 specval 29333 hhcno 29339 hhcnf 29340 adjeq 29370 brafval 29378 kbfval 29387 adjbdln 29518 rnbra 29542 bra11 29543 leoprf2 29562 ishst 29649 |
Copyright terms: Public domain | W3C validator |