Theorem h0elch 31170

Description: The zero subspace is a closed subspace. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
h0elch	⊢ 0ℋ ∈ Cℋ

Proof of Theorem h0elch

Step	Hyp	Ref	Expression
1		df-ch0 31168	. 2 ⊢ 0ℋ = {0ℎ}
2		hsn0elch 31163	. 2 ⊢ {0ℎ} ∈ Cℋ
3	1, 2	eqeltri 2829	1 ⊢ 0ℋ ∈ Cℋ

Syntax hints:   ∈ wcel 2107  {csn 4599  0_ℎc0v 30839   C_ℋ cch 30844  0_ℋc0h 30850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5247  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-cnex 11178  ax-resscn 11179  ax-1cn 11180  ax-icn 11181  ax-addcl 11182  ax-addrcl 11183  ax-mulcl 11184  ax-mulrcl 11185  ax-mulcom 11186  ax-addass 11187  ax-mulass 11188  ax-distr 11189  ax-i2m1 11190  ax-1ne0 11191  ax-1rid 11192  ax-rnegex 11193  ax-rrecex 11194  ax-cnre 11195  ax-pre-lttri 11196  ax-pre-lttrn 11197  ax-pre-ltadd 11198  ax-pre-mulgt0 11199  ax-pre-sup 11200  ax-addf 11201  ax-mulf 11202  ax-hilex 30914  ax-hfvadd 30915  ax-hvcom 30916  ax-hvass 30917  ax-hv0cl 30918  ax-hvaddid 30919  ax-hfvmul 30920  ax-hvmulid 30921  ax-hvmulass 30922  ax-hvdistr1 30923  ax-hvdistr2 30924  ax-hvmul0 30925  ax-hfi 30994  ax-his1 30997  ax-his2 30998  ax-his3 30999  ax-his4 31000

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-iun 4967  df-br 5118  df-opab 5180  df-mpt 5200  df-tr 5228  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6288  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7857  df-1st 7983  df-2nd 7984  df-frecs 8275  df-wrecs 8306  df-recs 8380  df-rdg 8419  df-er 8714  df-map 8837  df-pm 8838  df-en 8955  df-dom 8956  df-sdom 8957  df-sup 9449  df-inf 9450  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268  df-sub 11461  df-neg 11462  df-div 11888  df-nn 12234  df-2 12296  df-3 12297  df-4 12298  df-n0 12495  df-z 12582  df-uz 12846  df-q 12958  df-rp 13002  df-xneg 13121  df-xadd 13122  df-xmul 13123  df-icc 13361  df-seq 14010  df-exp 14070  df-cj 15107  df-re 15108  df-im 15109  df-sqrt 15243  df-abs 15244  df-topgen 17444  df-psmet 21294  df-xmet 21295  df-met 21296  df-bl 21297  df-mopn 21298  df-top 22819  df-topon 22836  df-bases 22871  df-lm 23154  df-haus 23240  df-grpo 30408  df-gid 30409  df-ginv 30410  df-gdiv 30411  df-ablo 30460  df-vc 30474  df-nv 30507  df-va 30510  df-ba 30511  df-sm 30512  df-0v 30513  df-vs 30514  df-nmcv 30515  df-ims 30516  df-hnorm 30883  df-hvsub 30886  df-hlim 30887  df-sh 31122  df-ch 31136  df-ch0 31168

This theorem is referenced by:  h0elsh  31171  chintcl  31247  omlsi  31319  pjoml  31351  pjoc2  31354  chj0i  31370  chj00i  31402  chm0  31406  chne0  31409  chocin  31410  chj0  31412  chlejb1  31427  chnle  31429  ledi  31455  chsup0  31463  h1datom  31497  cmbr3  31523  cm0  31524  pjoml2  31526  cmcm  31529  cmcm3  31530  lecm  31532  qlaxr3i  31551  nonbooli  31566  pjige0  31606  pjhfo  31621  pj11  31629  ho0f  31666  pjhmop  32065  pjidmco  32096  hst0  32148  largei  32182  mdslmd1lem3  32242  mdslmd1lem4  32243  csmdsymi  32249  elat2  32255  atcveq0  32263  hatomic  32275  atcv0eq  32294  atoml2i  32298  atordi  32299  atord  32303  atcvat2  32304  chirred  32310