HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  h0elch Structured version   Unicode version

Theorem h0elch 26600
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  |-  0H  e.  CH

Proof of Theorem h0elch
StepHypRef Expression
1 df-ch0 26598 . 2  |-  0H  =  { 0h }
2 hsn0elch 26593 . 2  |-  { 0h }  e.  CH
31, 2eqeltri 2488 1  |-  0H  e.  CH
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1844   {csn 3974   0hc0v 26268   CHcch 26273   0Hc0h 26279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-cnex 9580  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-mulcom 9588  ax-addass 9589  ax-mulass 9590  ax-distr 9591  ax-i2m1 9592  ax-1ne0 9593  ax-1rid 9594  ax-rnegex 9595  ax-rrecex 9596  ax-cnre 9597  ax-pre-lttri 9598  ax-pre-lttrn 9599  ax-pre-ltadd 9600  ax-pre-mulgt0 9601  ax-pre-sup 9602  ax-addf 9603  ax-mulf 9604  ax-hilex 26343  ax-hfvadd 26344  ax-hvcom 26345  ax-hvass 26346  ax-hv0cl 26347  ax-hvaddid 26348  ax-hfvmul 26349  ax-hvmulid 26350  ax-hvmulass 26351  ax-hvdistr1 26352  ax-hvdistr2 26353  ax-hvmul0 26354  ax-hfi 26423  ax-his1 26426  ax-his2 26427  ax-his3 26428  ax-his4 26429
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-nel 2603  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-riota 6242  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-om 6686  df-1st 6786  df-2nd 6787  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-er 7350  df-map 7461  df-pm 7462  df-en 7557  df-dom 7558  df-sdom 7559  df-sup 7937  df-pnf 9662  df-mnf 9663  df-xr 9664  df-ltxr 9665  df-le 9666  df-sub 9845  df-neg 9846  df-div 10250  df-nn 10579  df-2 10637  df-3 10638  df-4 10639  df-n0 10839  df-z 10908  df-uz 11130  df-q 11230  df-rp 11268  df-xneg 11373  df-xadd 11374  df-xmul 11375  df-icc 11591  df-seq 12154  df-exp 12213  df-cj 13083  df-re 13084  df-im 13085  df-sqrt 13219  df-abs 13220  df-topgen 15060  df-psmet 18733  df-xmet 18734  df-met 18735  df-bl 18736  df-mopn 18737  df-top 19693  df-bases 19695  df-topon 19696  df-lm 20025  df-haus 20111  df-grpo 25620  df-gid 25621  df-ginv 25622  df-gdiv 25623  df-ablo 25711  df-vc 25866  df-nv 25912  df-va 25915  df-ba 25916  df-sm 25917  df-0v 25918  df-vs 25919  df-nmcv 25920  df-ims 25921  df-hnorm 26312  df-hvsub 26315  df-hlim 26316  df-sh 26551  df-ch 26566  df-ch0 26598
This theorem is referenced by:  h0elsh  26601  chintcl  26677  omlsi  26749  pjoml  26781  pjoc2  26784  chj0i  26800  chj00i  26832  chm0  26836  chne0  26839  chocin  26840  chj0  26842  chlejb1  26857  chnle  26859  ledi  26885  chsup0  26893  h1datom  26927  cmbr3  26953  cm0  26954  pjoml2  26956  cmcm  26959  cmcm3  26960  lecm  26962  qlaxr3i  26981  nonbooli  26996  pjige0  27036  pjhfo  27051  pj11  27059  ho0f  27096  pjhmop  27495  pjidmco  27526  hst0  27578  largei  27612  mdslmd1lem3  27672  mdslmd1lem4  27673  csmdsymi  27679  elat2  27685  atcveq0  27693  hatomic  27705  atcv0eq  27724  atoml2i  27728  atordi  27729  atord  27733  atcvat2  27734  chirred  27740
  Copyright terms: Public domain W3C validator