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 28629 | . 2 class 0ℎ | |
2 | chba 28624 | . 2 class ℋ | |
3 | 1, 2 | wcel 2105 | 1 wff 0ℎ ∈ ℋ |
Colors of variables: wff setvar class |
This axiom is referenced by: ifhvhv0 28727 hvaddid2 28728 hvmul0 28729 hv2neg 28733 hvsub0 28781 hi01 28801 hi02 28802 norm0 28833 normneg 28849 norm3difi 28852 hilablo 28865 hilid 28866 hlim0 28940 helch 28948 hsn0elch 28953 elch0 28959 hhssnv 28969 ocsh 28988 shscli 29022 choc0 29031 shintcli 29034 pj0i 29398 df0op2 29457 hon0 29498 ho01i 29533 nmopsetn0 29570 nmfnsetn0 29583 dmadjrnb 29611 nmopge0 29616 nmfnge0 29632 bra0 29655 lnop0 29671 lnopmul 29672 0cnop 29684 nmop0 29691 nmfn0 29692 nmop0h 29696 nmcexi 29731 nmcopexi 29732 lnfn0i 29747 lnfnmuli 29749 nmcfnexi 29756 nlelshi 29765 riesz3i 29767 hmopidmchi 29856 |
Copyright terms: Public domain | W3C validator |