![]() |
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 28348 | . 2 class ℋ | |
2 | cvv 3397 | . 2 class V | |
3 | 1, 2 | wcel 2106 | 1 wff ℋ ∈ V |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmulex 28440 hilablo 28589 hhph 28607 hcau 28613 hlimadd 28622 hhcms 28632 issh 28637 shex 28641 hlim0 28664 hhssva 28686 hhsssm 28687 hhssnm 28688 hhshsslem1 28696 hhsscms 28708 ocval 28711 spanval 28764 hsupval 28765 sshjval 28781 sshjval3 28785 pjhfval 28827 pjmfn 29146 pjmf1 29147 hosmval 29166 hommval 29167 hodmval 29168 hfsmval 29169 hfmmval 29170 nmopval 29287 elcnop 29288 ellnop 29289 elunop 29303 elhmop 29304 hmopex 29306 nmfnval 29307 nlfnval 29312 elcnfn 29313 ellnfn 29314 dmadjss 29318 dmadjop 29319 adjeu 29320 adjval 29321 eigvecval 29327 eigvalfval 29328 specval 29329 hhcno 29335 hhcnf 29336 adjeq 29366 brafval 29374 kbfval 29383 adjbdln 29514 rnbra 29538 bra11 29539 leoprf2 29558 ishst 29645 |
Copyright terms: Public domain | W3C validator |