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 40822
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 40821 . 2 (𝜑𝑈 ∈ LVec)
5 lveclmod 21080 . 2 (𝑈 ∈ LVec → 𝑈 ∈ LMod)
64, 5syl 17 1 (𝜑𝑈 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  cfv 6546  LModclmod 20832  LVecclvec 21076  HLchlt 39061  LHypclh 39696  DVecHcdvh 40790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-riotaBAD 38664
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7995  df-2nd 7996  df-tpos 8233  df-undef 8280  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-er 8726  df-map 8849  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-n0 12519  df-z 12605  df-uz 12869  df-fz 13533  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-sca 17277  df-vsca 17278  df-0g 17451  df-proset 18315  df-poset 18333  df-plt 18350  df-lub 18366  df-glb 18367  df-join 18368  df-meet 18369  df-p0 18445  df-p1 18446  df-lat 18452  df-clat 18519  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-grp 18926  df-minusg 18927  df-cmn 19776  df-abl 19777  df-mgp 20114  df-rng 20132  df-ur 20161  df-ring 20214  df-oppr 20312  df-dvdsr 20335  df-unit 20336  df-invr 20366  df-dvr 20379  df-drng 20705  df-lmod 20834  df-lvec 21077  df-oposet 38887  df-ol 38889  df-oml 38890  df-covers 38977  df-ats 38978  df-atl 39009  df-cvlat 39033  df-hlat 39062  df-llines 39210  df-lplanes 39211  df-lvols 39212  df-lines 39213  df-psubsp 39215  df-pmap 39216  df-padd 39508  df-lhyp 39700  df-laut 39701  df-ldil 39816  df-ltrn 39817  df-trl 39871  df-tendo 40467  df-edring 40469  df-dvech 40791
This theorem is referenced by:  dvh0g  40823  dvhopellsm  40829  dib1dim2  40880  diclspsn  40906  cdlemn4a  40911  cdlemn5pre  40912  cdlemn11c  40921  dihjustlem  40928  dihord1  40930  dihord2a  40931  dihord2b  40932  dihord11c  40936  dihlsscpre  40946  dihvalcqat  40951  dihord6apre  40968  dihord5b  40971  dihord5apre  40974  dih0vbN  40994  dihglblem5  41010  dihjatc3  41025  dihmeetlem9N  41027  dihmeetlem13N  41031  dihmeetlem16N  41034  dihmeetlem19N  41037  dih1dimatlem  41041  dihlsprn  41043  dihlspsnat  41045  dihatlat  41046  dihatexv  41050  dihglblem6  41052  dochspss  41090  dochocsp  41091  dochspocN  41092  dochsncom  41094  dochsat  41095  dochshpncl  41096  dochlkr  41097  dochkrshp  41098  dochnoncon  41103  dochnel  41105  djhsumss  41119  djhunssN  41121  djhlsmcl  41126  dihjatcclem1  41130  dihjatcclem2  41131  dihjat  41135  dihprrnlem1N  41136  dihprrnlem2  41137  dihprrn  41138  djhlsmat  41139  dihjat1lem  41140  dihjat1  41141  dihsmsprn  41142  dihjat2  41143  dihsmatrn  41148  dvh3dimatN  41151  dvh2dimatN  41152  dvh1dim  41154  dvh4dimlem  41155  dvhdimlem  41156  dvh2dim  41157  dvh3dim  41158  dvh4dimN  41159  dvh3dim2  41160  dvh3dim3N  41161  dochsatshp  41163  dochsatshpb  41164  dochsnshp  41165  dochshpsat  41166  dochkrsat  41167  dochkrsat2  41168  dochkrsm  41170  dochexmidlem1  41172  dochexmidlem2  41173  dochexmidlem4  41175  dochexmidlem5  41176  dochexmidlem6  41177  dochexmidlem7  41178  dochexmidlem8  41179  dochexmid  41180  dochsnkrlem1  41181  dochsnkr  41184  dochsnkr2cl  41186  dochfl1  41188  dochfln0  41189  dochkr1  41190  dochkr1OLDN  41191  lcfl4N  41207  lcfl5  41208  lcfl6lem  41210  lcfl7lem  41211  lcfl6  41212  lcfl8  41214  lcfl8b  41216  lcfl9a  41217  lclkrlem1  41218  lclkrlem2a  41219  lclkrlem2b  41220  lclkrlem2c  41221  lclkrlem2e  41223  lclkrlem2f  41224  lclkrlem2h  41226  lclkrlem2j  41228  lclkrlem2k  41229  lclkrlem2o  41233  lclkrlem2p  41234  lclkrlem2r  41236  lclkrlem2s  41237  lclkrlem2u  41239  lclkrlem2v  41240  lclkrlem2  41244  lclkr  41245  lclkrslem1  41249  lclkrslem2  41250  lclkrs  41251  lcfrvalsnN  41253  lcfrlem4  41257  lcfrlem5  41258  lcfrlem6  41259  lcfrlem7  41260  lcfrlem9  41262  lcfrlem12N  41266  lcfrlem15  41269  lcfrlem16  41270  lcfrlem17  41271  lcfrlem19  41273  lcfrlem20  41274  lcfrlem21  41275  lcfrlem23  41277  lcfrlem25  41279  lcfrlem26  41280  lcfrlem28  41282  lcfrlem29  41283  lcfrlem30  41284  lcfrlem31  41285  lcfrlem33  41287  lcfrlem35  41289  lcfrlem36  41290  lcfrlem37  41291  lcfrlem40  41294  lcfrlem42  41296  lcfr  41297  lcdvbase  41305  lcdvbasecl  41308  lcdvaddval  41310  lcdsca  41311  lcdvsval  41316  lcd0v  41323  lcd0v2  41324  lcdvsubval  41330  lcdlss  41331  lcdlsp  41333  mapdval2N  41342  mapdordlem2  41349  mapdsn  41353  mapd1dim2lem1N  41356  mapdrvallem2  41357  mapdunirnN  41362  mapdcv  41372  mapdin  41374  mapdlsm  41376  mapd0  41377  mapdcnvatN  41378  mapdat  41379  mapdspex  41380  mapdn0  41381  mapdncol  41382  mapdindp  41383  mapdpglem1  41384  mapdpglem2  41385  mapdpglem2a  41386  mapdpglem3  41387  mapdpglem4N  41388  mapdpglem5N  41389  mapdpglem6  41390  mapdpglem8  41391  mapdpglem9  41392  mapdpglem12  41395  mapdpglem13  41396  mapdpglem14  41397  mapdpglem17N  41400  mapdpglem18  41401  mapdpglem19  41402  mapdpglem20  41403  mapdpglem21  41404  mapdpglem23  41406  mapdpglem30a  41407  mapdpglem30b  41408  mapdpglem29  41412  mapdpglem30  41414  mapdheq2  41441  mapdheq4lem  41443  mapdh6lem1N  41445  mapdh6lem2N  41446  mapdh6aN  41447  mapdh6b0N  41448  mapdh6bN  41449  mapdh6cN  41450  mapdh6dN  41451  mapdh6eN  41452  mapdh6gN  41454  mapdh6hN  41455  mapdh6iN  41456  mapdh8ab  41489  mapdh8ad  41491  mapdh8e  41496  mapdh9a  41501  mapdh9aOLDN  41502  hdmap1val0  41511  hdmap1l6lem1  41519  hdmap1l6lem2  41520  hdmap1l6a  41521  hdmap1l6b0N  41522  hdmap1l6b  41523  hdmap1l6c  41524  hdmap1l6d  41525  hdmap1l6e  41526  hdmap1l6g  41528  hdmap1l6h  41529  hdmap1l6i  41530  hdmap1eulem  41534  hdmap1eulemOLDN  41535  hdmapval0  41545  hdmapeveclem  41546  hdmapval3lemN  41549  hdmap10lem  41551  hdmap10  41552  hdmap11lem1  41553  hdmap11lem2  41554  hdmapeq0  41556  hdmapneg  41558  hdmapsub  41559  hdmap11  41560  hdmaprnlem1N  41561  hdmaprnlem3N  41562  hdmaprnlem3uN  41563  hdmaprnlem4tN  41564  hdmaprnlem4N  41565  hdmaprnlem6N  41566  hdmaprnlem8N  41568  hdmaprnlem9N  41569  hdmaprnlem3eN  41570  hdmaprnlem16N  41574  hdmaprnlem17N  41575  hdmap14lem1a  41578  hdmap14lem2a  41579  hdmap14lem2N  41581  hdmap14lem3  41582  hdmap14lem4a  41583  hdmap14lem6  41585  hdmap14lem8  41587  hdmap14lem9  41588  hdmap14lem10  41589  hdmap14lem11  41590  hdmap14lem13  41592  hgmapval0  41604  hgmapval1  41605  hgmapadd  41606  hgmapmul  41607  hgmaprnlem2N  41609  hgmaprnlem3N  41610  hgmap11  41614  hgmapeq0  41616  hdmapln1  41618  hdmaplna1  41619  hdmaplns1  41620  hdmaplnm1  41621  hdmapgln2  41624  hdmaplkr  41625  hdmapellkr  41626  hdmapip0  41627  hdmapinvlem1  41630  hdmapinvlem3  41632  hdmapinvlem4  41633  hdmapglem5  41634  hgmapvvlem1  41635  hgmapvvlem3  41637  hdmapglem7a  41639  hdmapglem7b  41640  hdmapglem7  41641  hdmapoc  41643  hlhilphllem  41675
  Copyright terms: Public domain W3C validator