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 28624 | . 2 class ℋ | |
2 | cvv 3495 | . 2 class V | |
3 | 1, 2 | wcel 2105 | 1 wff ℋ ∈ V |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmulex 28716 hilablo 28865 hhph 28883 hcau 28889 hlimadd 28898 hhcms 28908 issh 28913 shex 28917 hlim0 28940 hhssva 28962 hhsssm 28963 hhssnm 28964 hhshsslem1 28972 hhsscms 28983 ocval 28985 spanval 29038 hsupval 29039 sshjval 29055 sshjval3 29059 pjhfval 29101 pjmfn 29420 pjmf1 29421 hosmval 29440 hommval 29441 hodmval 29442 hfsmval 29443 hfmmval 29444 nmopval 29561 elcnop 29562 ellnop 29563 elunop 29577 elhmop 29578 hmopex 29580 nmfnval 29581 nlfnval 29586 elcnfn 29587 ellnfn 29588 dmadjss 29592 dmadjop 29593 adjeu 29594 adjval 29595 eigvecval 29601 eigvalfval 29602 specval 29603 hhcno 29609 hhcnf 29610 adjeq 29640 brafval 29648 kbfval 29657 adjbdln 29788 rnbra 29812 bra11 29813 leoprf2 29832 ishst 29919 |
Copyright terms: Public domain | W3C validator |