Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > ax-hilex | Structured version Visualization version Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chil 27776 | . 2 | |
2 | cvv 3200 | . 2 | |
3 | 1, 2 | wcel 1990 | 1 |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmulex 27868 hilablo 28017 hhph 28035 hcau 28041 hlimadd 28050 hhcms 28060 issh 28065 shex 28069 hlim0 28092 hhssva 28114 hhsssm 28115 hhssnm 28116 hhshsslem1 28124 hhsscms 28136 ocval 28139 spanval 28192 hsupval 28193 sshjval 28209 sshjval3 28213 pjhfval 28255 pjmfn 28574 pjmf1 28575 hosmval 28594 hommval 28595 hodmval 28596 hfsmval 28597 hfmmval 28598 nmopval 28715 elcnop 28716 ellnop 28717 elunop 28731 elhmop 28732 hmopex 28734 nmfnval 28735 nlfnval 28740 elcnfn 28741 ellnfn 28742 dmadjss 28746 dmadjop 28747 adjeu 28748 adjval 28749 eigvecval 28755 eigvalfval 28756 specval 28757 hhcno 28763 hhcnf 28764 adjeq 28794 brafval 28802 kbfval 28811 adjbdln 28942 rnbra 28966 bra11 28967 leoprf2 28986 ishst 29073 |
Copyright terms: Public domain | W3C validator |