| 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 31217 | . 2 class 0ℎ | |
| 2 | chba 31212 | . 2 class ℋ | |
| 3 | 1, 2 | wcel 2149 | 1 wff 0ℎ ∈ ℋ |
| Colors of variables: wff setvar class |
| This axiom is referenced by: ifhvhv0 31315 hvaddlid 31316 hvmul0 31317 hv2neg 31321 hvsub0 31369 hi01 31389 hi02 31390 norm0 31421 normneg 31437 norm3difi 31440 hilablo 31453 hilid 31454 hlim0 31528 helch 31536 hsn0elch 31541 elch0 31547 hhssnv 31557 ocsh 31576 shscli 31610 choc0 31619 shintcli 31622 pj0i 31986 df0op2 32045 hon0 32086 ho01i 32121 nmopsetn0 32158 nmfnsetn0 32171 dmadjrnb 32199 nmopge0 32204 nmfnge0 32220 bra0 32243 lnop0 32259 lnopmul 32260 0cnop 32272 nmop0 32279 nmfn0 32280 nmop0h 32284 nmcexi 32319 nmcopexi 32320 lnfn0i 32335 lnfnmuli 32337 nmcfnexi 32344 nlelshi 32353 riesz3i 32355 hmopidmchi 32444 |
| Copyright terms: Public domain | W3C validator |