![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > HSE Home > Th. List > ax-hv0cl | Unicode version |
Description: The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-hv0cl |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0v 22384 |
. 2
![]() ![]() | |
2 | chil 22379 |
. 2
![]() ![]() | |
3 | 1, 2 | wcel 1721 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: hvaddid2 22482 hvmul0 22483 hv2neg 22487 hvsubsub4 22519 hvnegdi 22526 hvsubeq0 22527 hvaddcan 22529 hvsub0 22535 hvsubadd 22536 hi01 22555 hi02 22556 normlem9at 22580 norm0 22587 normsq 22593 normsub0 22595 norm-ii 22597 norm-iii 22599 normsub 22602 normneg 22603 normpyth 22604 norm3difi 22606 norm3dif 22609 norm3lemt 22611 norm3adifi 22612 normpar 22614 polid 22618 hilablo 22619 hilid 22620 bcs 22640 hlim0 22695 helch 22703 hsn0elch 22707 elch0 22713 hhssnv 22721 ocsh 22742 shscli 22776 choc0 22785 shintcli 22788 pjoc1 22893 pjoc2 22898 h1de2ci 23015 spansn 23018 elspansn 23025 elspansn2 23026 h1datom 23041 spansnj 23106 spansncv 23112 pjch1 23129 pjadji 23144 pjaddi 23145 pjinormi 23146 pjsubi 23147 pjmuli 23148 pjcjt2 23151 pj0i 23152 pjch 23153 pjopyth 23179 pjnorm 23183 pjpyth 23184 pjnel 23185 df0op2 23212 hon0 23253 ho01i 23288 eigre 23295 eigorth 23298 nmopsetn0 23325 nmfnsetn0 23338 dmadjrnb 23366 nmopge0 23371 nmfnge0 23387 bra0 23410 lnop0 23426 lnopmul 23427 0cnop 23439 nmop0 23446 nmfn0 23447 nmop0h 23451 lnopeq0lem2 23466 lnopunii 23472 lnophmi 23478 nmcexi 23486 nmcopexi 23487 lnfn0i 23502 lnfnmuli 23504 nmcfnexi 23511 nlelshi 23520 riesz3i 23522 hmopidmchi 23611 pjss2coi 23624 pjssmi 23625 pjssge0i 23626 pjdifnormi 23627 |
Copyright terms: Public domain | W3C validator |