![]() |
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 30846 | . 2 class ℋ | |
2 | cvv 3462 | . 2 class V | |
3 | 1, 2 | wcel 2099 | 1 wff ℋ ∈ V |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmulex 30938 hilablo 31087 hhph 31105 hcau 31111 hlimadd 31120 hhcms 31130 issh 31135 shex 31139 hlim0 31162 hhssva 31184 hhsssm 31185 hhssnm 31186 hhshsslem1 31194 hhsscms 31205 ocval 31207 spanval 31260 hsupval 31261 sshjval 31277 sshjval3 31281 pjhfval 31323 pjmfn 31642 pjmf1 31643 hosmval 31662 hommval 31663 hodmval 31664 hfsmval 31665 hfmmval 31666 nmopval 31783 elcnop 31784 ellnop 31785 elunop 31799 elhmop 31800 hmopex 31802 nmfnval 31803 nlfnval 31808 elcnfn 31809 ellnfn 31810 dmadjss 31814 dmadjop 31815 adjeu 31816 adjval 31817 eigvecval 31823 eigvalfval 31824 specval 31825 hhcno 31831 hhcnf 31832 adjeq 31862 brafval 31870 kbfval 31879 adjbdln 32010 rnbra 32034 bra11 32035 leoprf2 32054 ishst 32141 |
Copyright terms: Public domain | W3C validator |