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 27165 | . 2 class 0ℎ | |
2 | chil 27160 | . 2 class ℋ | |
3 | 1, 2 | wcel 1977 | 1 wff 0ℎ ∈ ℋ |
Colors of variables: wff setvar class |
This axiom is referenced by: ifhvhv0 27263 hvaddid2 27264 hvmul0 27265 hv2neg 27269 hvsub0 27317 hi01 27337 hi02 27338 norm0 27369 normneg 27385 norm3difi 27388 hilablo 27401 hilid 27402 hlim0 27476 helch 27484 hsn0elch 27489 elch0 27495 hhssnv 27505 ocsh 27526 shscli 27560 choc0 27569 shintcli 27572 pj0i 27936 df0op2 27995 hon0 28036 ho01i 28071 nmopsetn0 28108 nmfnsetn0 28121 dmadjrnb 28149 nmopge0 28154 nmfnge0 28170 bra0 28193 lnop0 28209 lnopmul 28210 0cnop 28222 nmop0 28229 nmfn0 28230 nmop0h 28234 nmcexi 28269 nmcopexi 28270 lnfn0i 28285 lnfnmuli 28287 nmcfnexi 28294 nlelshi 28303 riesz3i 28305 hmopidmchi 28394 |
Copyright terms: Public domain | W3C validator |