| 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 30982 | . 2 class 0ℎ | |
| 2 | chba 30977 | . 2 class ℋ | |
| 3 | 1, 2 | wcel 2114 | 1 wff 0ℎ ∈ ℋ |
| Colors of variables: wff setvar class |
| This axiom is referenced by: ifhvhv0 31080 hvaddlid 31081 hvmul0 31082 hv2neg 31086 hvsub0 31134 hi01 31154 hi02 31155 norm0 31186 normneg 31202 norm3difi 31205 hilablo 31218 hilid 31219 hlim0 31293 helch 31301 hsn0elch 31306 elch0 31312 hhssnv 31322 ocsh 31341 shscli 31375 choc0 31384 shintcli 31387 pj0i 31751 df0op2 31810 hon0 31851 ho01i 31886 nmopsetn0 31923 nmfnsetn0 31936 dmadjrnb 31964 nmopge0 31969 nmfnge0 31985 bra0 32008 lnop0 32024 lnopmul 32025 0cnop 32037 nmop0 32044 nmfn0 32045 nmop0h 32049 nmcexi 32084 nmcopexi 32085 lnfn0i 32100 lnfnmuli 32102 nmcfnexi 32109 nlelshi 32118 riesz3i 32120 hmopidmchi 32209 |
| Copyright terms: Public domain | W3C validator |