| 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 30943 | . 2 class 0ℎ | |
| 2 | chba 30938 | . 2 class ℋ | |
| 3 | 1, 2 | wcel 2108 | 1 wff 0ℎ ∈ ℋ |
| Colors of variables: wff setvar class |
| This axiom is referenced by: ifhvhv0 31041 hvaddlid 31042 hvmul0 31043 hv2neg 31047 hvsub0 31095 hi01 31115 hi02 31116 norm0 31147 normneg 31163 norm3difi 31166 hilablo 31179 hilid 31180 hlim0 31254 helch 31262 hsn0elch 31267 elch0 31273 hhssnv 31283 ocsh 31302 shscli 31336 choc0 31345 shintcli 31348 pj0i 31712 df0op2 31771 hon0 31812 ho01i 31847 nmopsetn0 31884 nmfnsetn0 31897 dmadjrnb 31925 nmopge0 31930 nmfnge0 31946 bra0 31969 lnop0 31985 lnopmul 31986 0cnop 31998 nmop0 32005 nmfn0 32006 nmop0h 32010 nmcexi 32045 nmcopexi 32046 lnfn0i 32061 lnfnmuli 32063 nmcfnexi 32070 nlelshi 32079 riesz3i 32081 hmopidmchi 32170 |
| Copyright terms: Public domain | W3C validator |