Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvhlmod Structured version   Visualization version   GIF version

Theorem dvhlmod 36919
Description: The full vector space 𝑈 constructed from a Hilbert lattice 𝐾 (given a fiducial hyperplane 𝑊) is a left module. (Contributed by NM, 23-May-2015.)
Hypotheses
Ref Expression
dvhlvec.h 𝐻 = (LHyp‘𝐾)
dvhlvec.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dvhlvec.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
Assertion
Ref Expression
dvhlmod (𝜑𝑈 ∈ LMod)

Proof of Theorem dvhlmod
StepHypRef Expression
1 dvhlvec.h . . 3 𝐻 = (LHyp‘𝐾)
2 dvhlvec.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 dvhlvec.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
41, 2, 3dvhlvec 36918 . 2 (𝜑𝑈 ∈ LVec)
5 lveclmod 19328 . 2 (𝑈 ∈ LVec → 𝑈 ∈ LMod)
64, 5syl 17 1 (𝜑𝑈 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2139  cfv 6049  LModclmod 19085  LVecclvec 19324  HLchlt 35158  LHypclh 35791  DVecHcdvh 36887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-riotaBAD 34760
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-tpos 7522  df-undef 7569  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-er 7913  df-map 8027  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-n0 11505  df-z 11590  df-uz 11900  df-fz 12540  df-struct 16081  df-ndx 16082  df-slot 16083  df-base 16085  df-sets 16086  df-ress 16087  df-plusg 16176  df-mulr 16177  df-sca 16179  df-vsca 16180  df-0g 16324  df-preset 17149  df-poset 17167  df-plt 17179  df-lub 17195  df-glb 17196  df-join 17197  df-meet 17198  df-p0 17260  df-p1 17261  df-lat 17267  df-clat 17329  df-mgm 17463  df-sgrp 17505  df-mnd 17516  df-grp 17646  df-minusg 17647  df-mgp 18710  df-ur 18722  df-ring 18769  df-oppr 18843  df-dvdsr 18861  df-unit 18862  df-invr 18892  df-dvr 18903  df-drng 18971  df-lmod 19087  df-lvec 19325  df-oposet 34984  df-ol 34986  df-oml 34987  df-covers 35074  df-ats 35075  df-atl 35106  df-cvlat 35130  df-hlat 35159  df-llines 35305  df-lplanes 35306  df-lvols 35307  df-lines 35308  df-psubsp 35310  df-pmap 35311  df-padd 35603  df-lhyp 35795  df-laut 35796  df-ldil 35911  df-ltrn 35912  df-trl 35967  df-tendo 36563  df-edring 36565  df-dvech 36888
This theorem is referenced by:  dvh0g  36920  dvhopellsm  36926  dib1dim2  36977  diclspsn  37003  cdlemn4a  37008  cdlemn5pre  37009  cdlemn11c  37018  dihjustlem  37025  dihord1  37027  dihord2a  37028  dihord2b  37029  dihord11c  37033  dihlsscpre  37043  dihvalcqat  37048  dihord6apre  37065  dihord5b  37068  dihord5apre  37071  dih0vbN  37091  dihglblem5  37107  dihjatc3  37122  dihmeetlem9N  37124  dihmeetlem13N  37128  dihmeetlem16N  37131  dihmeetlem19N  37134  dih1dimatlem  37138  dihlsprn  37140  dihlspsnat  37142  dihatlat  37143  dihatexv  37147  dihglblem6  37149  dochspss  37187  dochocsp  37188  dochspocN  37189  dochsncom  37191  dochsat  37192  dochshpncl  37193  dochlkr  37194  dochkrshp  37195  dochnoncon  37200  dochnel  37202  djhsumss  37216  djhunssN  37218  djhlsmcl  37223  dihjatcclem1  37227  dihjatcclem2  37228  dihjat  37232  dihprrnlem1N  37233  dihprrnlem2  37234  dihprrn  37235  djhlsmat  37236  dihjat1lem  37237  dihjat1  37238  dihsmsprn  37239  dihjat2  37240  dihsmatrn  37245  dvh3dimatN  37248  dvh2dimatN  37249  dvh1dim  37251  dvh4dimlem  37252  dvhdimlem  37253  dvh2dim  37254  dvh3dim  37255  dvh4dimN  37256  dvh3dim2  37257  dvh3dim3N  37258  dochsatshp  37260  dochsatshpb  37261  dochsnshp  37262  dochshpsat  37263  dochkrsat  37264  dochkrsat2  37265  dochkrsm  37267  dochexmidlem1  37269  dochexmidlem2  37270  dochexmidlem4  37272  dochexmidlem5  37273  dochexmidlem6  37274  dochexmidlem7  37275  dochexmidlem8  37276  dochexmid  37277  dochsnkrlem1  37278  dochsnkr  37281  dochsnkr2cl  37283  dochfl1  37285  dochfln0  37286  dochkr1  37287  dochkr1OLDN  37288  lcfl4N  37304  lcfl5  37305  lcfl6lem  37307  lcfl7lem  37308  lcfl6  37309  lcfl8  37311  lcfl8b  37313  lcfl9a  37314  lclkrlem1  37315  lclkrlem2a  37316  lclkrlem2b  37317  lclkrlem2c  37318  lclkrlem2e  37320  lclkrlem2f  37321  lclkrlem2h  37323  lclkrlem2j  37325  lclkrlem2k  37326  lclkrlem2o  37330  lclkrlem2p  37331  lclkrlem2r  37333  lclkrlem2s  37334  lclkrlem2u  37336  lclkrlem2v  37337  lclkrlem2  37341  lclkr  37342  lclkrslem1  37346  lclkrslem2  37347  lclkrs  37348  lcfrvalsnN  37350  lcfrlem4  37354  lcfrlem5  37355  lcfrlem6  37356  lcfrlem7  37357  lcfrlem9  37359  lcfrlem12N  37363  lcfrlem15  37366  lcfrlem16  37367  lcfrlem17  37368  lcfrlem19  37370  lcfrlem20  37371  lcfrlem21  37372  lcfrlem23  37374  lcfrlem25  37376  lcfrlem26  37377  lcfrlem28  37379  lcfrlem29  37380  lcfrlem30  37381  lcfrlem31  37382  lcfrlem33  37384  lcfrlem35  37386  lcfrlem36  37387  lcfrlem37  37388  lcfrlem40  37391  lcfrlem42  37393  lcfr  37394  lcdvbase  37402  lcdvbasecl  37405  lcdvaddval  37407  lcdsca  37408  lcdvsval  37413  lcd0v  37420  lcd0v2  37421  lcdvsubval  37427  lcdlss  37428  lcdlsp  37430  mapdval2N  37439  mapdordlem2  37446  mapdsn  37450  mapd1dim2lem1N  37453  mapdrvallem2  37454  mapdunirnN  37459  mapdcv  37469  mapdin  37471  mapdlsm  37473  mapd0  37474  mapdcnvatN  37475  mapdat  37476  mapdspex  37477  mapdn0  37478  mapdncol  37479  mapdindp  37480  mapdpglem1  37481  mapdpglem2  37482  mapdpglem2a  37483  mapdpglem3  37484  mapdpglem4N  37485  mapdpglem5N  37486  mapdpglem6  37487  mapdpglem8  37488  mapdpglem9  37489  mapdpglem12  37492  mapdpglem13  37493  mapdpglem14  37494  mapdpglem17N  37497  mapdpglem18  37498  mapdpglem19  37499  mapdpglem20  37500  mapdpglem21  37501  mapdpglem23  37503  mapdpglem30a  37504  mapdpglem30b  37505  mapdpglem29  37509  mapdpglem30  37511  mapdheq2  37538  mapdheq4lem  37540  mapdh6lem1N  37542  mapdh6lem2N  37543  mapdh6aN  37544  mapdh6b0N  37545  mapdh6bN  37546  mapdh6cN  37547  mapdh6dN  37548  mapdh6eN  37549  mapdh6gN  37551  mapdh6hN  37552  mapdh6iN  37553  mapdh8ab  37586  mapdh8ad  37588  mapdh8e  37593  mapdh9a  37599  mapdh9aOLDN  37600  hdmap1val0  37609  hdmap1l6lem1  37617  hdmap1l6lem2  37618  hdmap1l6a  37619  hdmap1l6b0N  37620  hdmap1l6b  37621  hdmap1l6c  37622  hdmap1l6d  37623  hdmap1l6e  37624  hdmap1l6g  37626  hdmap1l6h  37627  hdmap1l6i  37628  hdmap1eulem  37633  hdmap1eulemOLDN  37634  hdmap1neglem1N  37637  hdmapval0  37645  hdmapeveclem  37646  hdmapval3lemN  37649  hdmap10lem  37651  hdmap10  37652  hdmap11lem1  37653  hdmap11lem2  37654  hdmapeq0  37656  hdmapneg  37658  hdmapsub  37659  hdmap11  37660  hdmaprnlem1N  37661  hdmaprnlem3N  37662  hdmaprnlem3uN  37663  hdmaprnlem4tN  37664  hdmaprnlem4N  37665  hdmaprnlem6N  37666  hdmaprnlem8N  37668  hdmaprnlem9N  37669  hdmaprnlem3eN  37670  hdmaprnlem16N  37674  hdmaprnlem17N  37675  hdmap14lem1a  37678  hdmap14lem2a  37679  hdmap14lem2N  37681  hdmap14lem3  37682  hdmap14lem4a  37683  hdmap14lem6  37685  hdmap14lem8  37687  hdmap14lem9  37688  hdmap14lem10  37689  hdmap14lem11  37690  hdmap14lem13  37692  hgmapval0  37704  hgmapval1  37705  hgmapadd  37706  hgmapmul  37707  hgmaprnlem2N  37709  hgmaprnlem3N  37710  hgmap11  37714  hgmapeq0  37716  hdmapln1  37718  hdmaplna1  37719  hdmaplns1  37720  hdmaplnm1  37721  hdmapgln2  37724  hdmaplkr  37725  hdmapellkr  37726  hdmapip0  37727  hdmapinvlem1  37730  hdmapinvlem3  37732  hdmapinvlem4  37733  hdmapglem5  37734  hgmapvvlem1  37735  hgmapvvlem3  37737  hdmapglem7a  37739  hdmapglem7b  37740  hdmapglem7  37741  hdmapoc  37743  hlhilphllem  37771
  Copyright terms: Public domain W3C validator