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

Theorem shatomici 23781
 Description: The lattice of Hilbert subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
Hypothesis
Ref Expression
shatomic.1
Assertion
Ref Expression
shatomici HAtoms
Distinct variable group:   ,

Proof of Theorem shatomici
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 shatomic.1 . . 3
21shne0i 22870 . 2
31sheli 22636 . . . . 5
4 h1da 23772 . . . . 5 HAtoms
53, 4sylan 458 . . . 4 HAtoms
6 sh1dle 23774 . . . . . 6
71, 6mpan 652 . . . . 5
87adantr 452 . . . 4
9 sseq1 3326 . . . . 5
109rspcev 3009 . . . 4 HAtoms HAtoms
115, 8, 10syl2anc 643 . . 3 HAtoms
1211rexlimiva 2782 . 2 HAtoms
132, 12sylbi 188 1 HAtoms
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   wcel 1721   wne 2564  wrex 2664   wss 3277  csn 3771  cfv 5408  chil 22342  c0v 22347  csh 22351  cort 22353  c0h 22358  HAtomscat 22388 This theorem is referenced by:  hatomici  23782 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-inf2 7543  ax-cc 8262  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014  ax-pre-sup 9015  ax-addf 9016  ax-mulf 9017  ax-hilex 22422  ax-hfvadd 22423  ax-hvcom 22424  ax-hvass 22425  ax-hv0cl 22426  ax-hvaddid 22427  ax-hfvmul 22428  ax-hvmulid 22429  ax-hvmulass 22430  ax-hvdistr1 22431  ax-hvdistr2 22432  ax-hvmul0 22433  ax-hfi 22501  ax-his1 22504  ax-his2 22505  ax-his3 22506  ax-his4 22507  ax-hcompl 22624 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-iin 4052  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-se 4497  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-of 6258  df-1st 6302  df-2nd 6303  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-2o 6675  df-oadd 6678  df-omul 6679  df-er 6855  df-map 6970  df-pm 6971  df-ixp 7014  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-fi 7365  df-sup 7395  df-oi 7426  df-card 7773  df-acn 7776  df-cda 7995  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-div 9624  df-nn 9947  df-2 10004  df-3 10005  df-4 10006  df-5 10007  df-6 10008  df-7 10009  df-8 10010  df-9 10011  df-10 10012  df-n0 10168  df-z 10229  df-dec 10329  df-uz 10435  df-q 10521  df-rp 10559  df-xneg 10656  df-xadd 10657  df-xmul 10658  df-ioo 10866  df-ico 10868  df-icc 10869  df-fz 10990  df-fzo 11080  df-fl 11143  df-seq 11265  df-exp 11324  df-hash 11560  df-cj 11845  df-re 11846  df-im 11847  df-sqr 11981  df-abs 11982  df-clim 12223  df-rlim 12224  df-sum 12421  df-struct 13412  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-ress 13417  df-plusg 13483  df-mulr 13484  df-starv 13485  df-sca 13486  df-vsca 13487  df-tset 13489  df-ple 13490  df-ds 13492  df-unif 13493  df-hom 13494  df-cco 13495  df-rest 13591  df-topn 13592  df-topgen 13608  df-pt 13609  df-prds 13612  df-xrs 13667  df-0g 13668  df-gsum 13669  df-qtop 13674  df-imas 13675  df-xps 13677  df-mre 13752  df-mrc 13753  df-acs 13755  df-mnd 14631  df-submnd 14680  df-mulg 14756  df-cntz 15057  df-cmn 15355  df-psmet 16635  df-xmet 16636  df-met 16637  df-bl 16638  df-mopn 16639  df-fbas 16640  df-fg 16641  df-cnfld 16645  df-top 16904  df-bases 16906  df-topon 16907  df-topsp 16908  df-cld 17024  df-ntr 17025  df-cls 17026  df-nei 17103  df-cn 17231  df-cnp 17232  df-lm 17233  df-haus 17319  df-tx 17533  df-hmeo 17726  df-fil 17817  df-fm 17909  df-flim 17910  df-flf 17911  df-xms 18289  df-ms 18290  df-tms 18291  df-cfil 19147  df-cau 19148  df-cmet 19149  df-grpo 21699  df-gid 21700  df-ginv 21701  df-gdiv 21702  df-ablo 21790  df-subgo 21810  df-vc 21945  df-nv 21991  df-va 21994  df-ba 21995  df-sm 21996  df-0v 21997  df-vs 21998  df-nmcv 21999  df-ims 22000  df-dip 22117  df-ssp 22141  df-ph 22234  df-cbn 22285  df-hnorm 22391  df-hba 22392  df-hvsub 22394  df-hlim 22395  df-hcau 22396  df-sh 22629  df-ch 22644  df-oc 22674  df-ch0 22675  df-span 22731  df-cv 23702  df-at 23761
 Copyright terms: Public domain W3C validator