Home
Hilbert Space Explorer
< Previous
Next >
Related theorems
Unicode version
Axiom
ax-hv0cl
8956
Description:
The zero vector is in the vector space.
Assertion
Ref
Expression
ax-hv0cl
Detailed syntax breakdown of Axiom
ax-hv0cl
Step
Hyp
Ref
Expression
1
c0v
8874
. 2
2
chil
8871
. 2
3
1, 2
wcel
999
1
Colors of variables:
wff
set
class
This axiom is referenced by:
hvaddid2
8975
hvmul0
8976
hv2neg
8980
hvsubsub4
9010
hvnegdi
9017
hvsubeq0
9018
hvaddcan
9020
hvsub0
9026
hvsubadd
9027
hi01
9045
hi02
9046
normlem9at
9070
norm0
9078
normsq
9084
normsub0
9086
norm-ii
9088
norm-iii
9090
normsub
9093
normneg
9094
normpyth
9095
norm3difi
9097
norm3dif
9100
norm3lemt
9102
norm3adifi
9103
normpar
9105
polid
9109
hilabl
9110
hilid
9111
bcs
9131
hlim0
9188
hlimcaui
9190
hlimunii
9192
helch
9199
hsn0elch
9203
elch0
9209
hhssnv
9217
ocsh
9239
occllem2
9257
occllem8
9263
projlem8
9276
pjthlem13
9314
pjth
9317
axpjpj
9339
pjoc1
9350
pjoc2
9355
shscli
9364
choc0
9373
shintcli
9376
h1de2ci
9562
spansn
9565
elspansn
9572
elspansn2
9573
h1datom
9588
spansnj
9675
spansncv
9681
pjch1
9698
pjadji
9713
pjaddi
9714
pjinormi
9715
pjsubi
9716
pjmuli
9717
pjcjt2
9720
pj0i
9721
pjch
9722
pjopyth
9748
pjnorm
9752
pjpyth
9753
pjnel
9754
df0op2
9761
hon0
9802
ho01i
9837
eigre
9844
eigorth
9847
nmopsetn0
9875
nmfnsetn0
9888
dmadjrnb
9913
nmopge0
9918
nmfnge0
9934
bra0
9957
lnop0
9973
lnopmul
9974
0cnop
9986
nmop0
9993
nmfn0
9994
nmop0h
9999
lnopeq0lem2
10014
lnopunii
10020
lnophmi
10026
nmcopexlem2
10035
lnfn0i
10054
lnfnmuli
10056
nmcfnexlem2
10064
nlelshi
10076
riesz3i
10078
hmopidmchi
10162
pjss2coi
10175
pjssmi
10176
pjssge0i
10177
pjdifnormi
10178
Copyright terms:
Public domain