![]() |
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 30681 | . 2 class ℋ | |
2 | cvv 3468 | . 2 class V | |
3 | 1, 2 | wcel 2098 | 1 wff ℋ ∈ V |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmulex 30773 hilablo 30922 hhph 30940 hcau 30946 hlimadd 30955 hhcms 30965 issh 30970 shex 30974 hlim0 30997 hhssva 31019 hhsssm 31020 hhssnm 31021 hhshsslem1 31029 hhsscms 31040 ocval 31042 spanval 31095 hsupval 31096 sshjval 31112 sshjval3 31116 pjhfval 31158 pjmfn 31477 pjmf1 31478 hosmval 31497 hommval 31498 hodmval 31499 hfsmval 31500 hfmmval 31501 nmopval 31618 elcnop 31619 ellnop 31620 elunop 31634 elhmop 31635 hmopex 31637 nmfnval 31638 nlfnval 31643 elcnfn 31644 ellnfn 31645 dmadjss 31649 dmadjop 31650 adjeu 31651 adjval 31652 eigvecval 31658 eigvalfval 31659 specval 31660 hhcno 31666 hhcnf 31667 adjeq 31697 brafval 31705 kbfval 31714 adjbdln 31845 rnbra 31869 bra11 31870 leoprf2 31889 ishst 31976 |
Copyright terms: Public domain | W3C validator |