![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > ax-hv0cl | Structured version Visualization version GIF version |
Description: The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-hv0cl | ⊢ 0ℎ ∈ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0v 29695 | . 2 class 0ℎ | |
2 | chba 29690 | . 2 class ℋ | |
3 | 1, 2 | wcel 2106 | 1 wff 0ℎ ∈ ℋ |
Colors of variables: wff setvar class |
This axiom is referenced by: ifhvhv0 29793 hvaddid2 29794 hvmul0 29795 hv2neg 29799 hvsub0 29847 hi01 29867 hi02 29868 norm0 29899 normneg 29915 norm3difi 29918 hilablo 29931 hilid 29932 hlim0 30006 helch 30014 hsn0elch 30019 elch0 30025 hhssnv 30035 ocsh 30054 shscli 30088 choc0 30097 shintcli 30100 pj0i 30464 df0op2 30523 hon0 30564 ho01i 30599 nmopsetn0 30636 nmfnsetn0 30649 dmadjrnb 30677 nmopge0 30682 nmfnge0 30698 bra0 30721 lnop0 30737 lnopmul 30738 0cnop 30750 nmop0 30757 nmfn0 30758 nmop0h 30762 nmcexi 30797 nmcopexi 30798 lnfn0i 30813 lnfnmuli 30815 nmcfnexi 30822 nlelshi 30831 riesz3i 30833 hmopidmchi 30922 |
Copyright terms: Public domain | W3C validator |