![]() |
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 28121 | . 2 class 0ℎ | |
2 | chil 28116 | . 2 class ℋ | |
3 | 1, 2 | wcel 2145 | 1 wff 0ℎ ∈ ℋ |
Colors of variables: wff setvar class |
This axiom is referenced by: ifhvhv0 28219 hvaddid2 28220 hvmul0 28221 hv2neg 28225 hvsub0 28273 hi01 28293 hi02 28294 norm0 28325 normneg 28341 norm3difi 28344 hilablo 28357 hilid 28358 hlim0 28432 helch 28440 hsn0elch 28445 elch0 28451 hhssnv 28461 ocsh 28482 shscli 28516 choc0 28525 shintcli 28528 pj0i 28892 df0op2 28951 hon0 28992 ho01i 29027 nmopsetn0 29064 nmfnsetn0 29077 dmadjrnb 29105 nmopge0 29110 nmfnge0 29126 bra0 29149 lnop0 29165 lnopmul 29166 0cnop 29178 nmop0 29185 nmfn0 29186 nmop0h 29190 nmcexi 29225 nmcopexi 29226 lnfn0i 29241 lnfnmuli 29243 nmcfnexi 29250 nlelshi 29259 riesz3i 29261 hmopidmchi 29350 |
Copyright terms: Public domain | W3C validator |