| 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 30855 | . 2 class 0ℎ | |
| 2 | chba 30850 | . 2 class ℋ | |
| 3 | 1, 2 | wcel 2109 | 1 wff 0ℎ ∈ ℋ |
| Colors of variables: wff setvar class |
| This axiom is referenced by: ifhvhv0 30953 hvaddlid 30954 hvmul0 30955 hv2neg 30959 hvsub0 31007 hi01 31027 hi02 31028 norm0 31059 normneg 31075 norm3difi 31078 hilablo 31091 hilid 31092 hlim0 31166 helch 31174 hsn0elch 31179 elch0 31185 hhssnv 31195 ocsh 31214 shscli 31248 choc0 31257 shintcli 31260 pj0i 31624 df0op2 31683 hon0 31724 ho01i 31759 nmopsetn0 31796 nmfnsetn0 31809 dmadjrnb 31837 nmopge0 31842 nmfnge0 31858 bra0 31881 lnop0 31897 lnopmul 31898 0cnop 31910 nmop0 31917 nmfn0 31918 nmop0h 31922 nmcexi 31957 nmcopexi 31958 lnfn0i 31973 lnfnmuli 31975 nmcfnexi 31982 nlelshi 31991 riesz3i 31993 hmopidmchi 32082 |
| Copyright terms: Public domain | W3C validator |