![]() |
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 28370 | . 2 class 0ℎ | |
2 | chba 28365 | . 2 class ℋ | |
3 | 1, 2 | wcel 2107 | 1 wff 0ℎ ∈ ℋ |
Colors of variables: wff setvar class |
This axiom is referenced by: ifhvhv0 28468 hvaddid2 28469 hvmul0 28470 hv2neg 28474 hvsub0 28522 hi01 28542 hi02 28543 norm0 28574 normneg 28590 norm3difi 28593 hilablo 28606 hilid 28607 hlim0 28681 helch 28689 hsn0elch 28694 elch0 28700 hhssnv 28710 ocsh 28731 shscli 28765 choc0 28774 shintcli 28777 pj0i 29141 df0op2 29200 hon0 29241 ho01i 29276 nmopsetn0 29313 nmfnsetn0 29326 dmadjrnb 29354 nmopge0 29359 nmfnge0 29375 bra0 29398 lnop0 29414 lnopmul 29415 0cnop 29427 nmop0 29434 nmfn0 29435 nmop0h 29439 nmcexi 29474 nmcopexi 29475 lnfn0i 29490 lnfnmuli 29492 nmcfnexi 29499 nlelshi 29508 riesz3i 29510 hmopidmchi 29599 |
Copyright terms: Public domain | W3C validator |