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 39969
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 39968 . 2 (πœ‘ β†’ π‘ˆ ∈ LVec)
5 lveclmod 20709 . 2 (π‘ˆ ∈ LVec β†’ π‘ˆ ∈ LMod)
64, 5syl 17 1 (πœ‘ β†’ π‘ˆ ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  β€˜cfv 6540  LModclmod 20463  LVecclvec 20705  HLchlt 38208  LHypclh 38843  DVecHcdvh 39937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-riotaBAD 37811
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-tpos 8207  df-undef 8254  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-sca 17209  df-vsca 17210  df-0g 17383  df-proset 18244  df-poset 18262  df-plt 18279  df-lub 18295  df-glb 18296  df-join 18297  df-meet 18298  df-p0 18374  df-p1 18375  df-lat 18381  df-clat 18448  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-grp 18818  df-minusg 18819  df-mgp 19982  df-ur 19999  df-ring 20051  df-oppr 20142  df-dvdsr 20163  df-unit 20164  df-invr 20194  df-dvr 20207  df-drng 20309  df-lmod 20465  df-lvec 20706  df-oposet 38034  df-ol 38036  df-oml 38037  df-covers 38124  df-ats 38125  df-atl 38156  df-cvlat 38180  df-hlat 38209  df-llines 38357  df-lplanes 38358  df-lvols 38359  df-lines 38360  df-psubsp 38362  df-pmap 38363  df-padd 38655  df-lhyp 38847  df-laut 38848  df-ldil 38963  df-ltrn 38964  df-trl 39018  df-tendo 39614  df-edring 39616  df-dvech 39938
This theorem is referenced by:  dvh0g  39970  dvhopellsm  39976  dib1dim2  40027  diclspsn  40053  cdlemn4a  40058  cdlemn5pre  40059  cdlemn11c  40068  dihjustlem  40075  dihord1  40077  dihord2a  40078  dihord2b  40079  dihord11c  40083  dihlsscpre  40093  dihvalcqat  40098  dihord6apre  40115  dihord5b  40118  dihord5apre  40121  dih0vbN  40141  dihglblem5  40157  dihjatc3  40172  dihmeetlem9N  40174  dihmeetlem13N  40178  dihmeetlem16N  40181  dihmeetlem19N  40184  dih1dimatlem  40188  dihlsprn  40190  dihlspsnat  40192  dihatlat  40193  dihatexv  40197  dihglblem6  40199  dochspss  40237  dochocsp  40238  dochspocN  40239  dochsncom  40241  dochsat  40242  dochshpncl  40243  dochlkr  40244  dochkrshp  40245  dochnoncon  40250  dochnel  40252  djhsumss  40266  djhunssN  40268  djhlsmcl  40273  dihjatcclem1  40277  dihjatcclem2  40278  dihjat  40282  dihprrnlem1N  40283  dihprrnlem2  40284  dihprrn  40285  djhlsmat  40286  dihjat1lem  40287  dihjat1  40288  dihsmsprn  40289  dihjat2  40290  dihsmatrn  40295  dvh3dimatN  40298  dvh2dimatN  40299  dvh1dim  40301  dvh4dimlem  40302  dvhdimlem  40303  dvh2dim  40304  dvh3dim  40305  dvh4dimN  40306  dvh3dim2  40307  dvh3dim3N  40308  dochsatshp  40310  dochsatshpb  40311  dochsnshp  40312  dochshpsat  40313  dochkrsat  40314  dochkrsat2  40315  dochkrsm  40317  dochexmidlem1  40319  dochexmidlem2  40320  dochexmidlem4  40322  dochexmidlem5  40323  dochexmidlem6  40324  dochexmidlem7  40325  dochexmidlem8  40326  dochexmid  40327  dochsnkrlem1  40328  dochsnkr  40331  dochsnkr2cl  40333  dochfl1  40335  dochfln0  40336  dochkr1  40337  dochkr1OLDN  40338  lcfl4N  40354  lcfl5  40355  lcfl6lem  40357  lcfl7lem  40358  lcfl6  40359  lcfl8  40361  lcfl8b  40363  lcfl9a  40364  lclkrlem1  40365  lclkrlem2a  40366  lclkrlem2b  40367  lclkrlem2c  40368  lclkrlem2e  40370  lclkrlem2f  40371  lclkrlem2h  40373  lclkrlem2j  40375  lclkrlem2k  40376  lclkrlem2o  40380  lclkrlem2p  40381  lclkrlem2r  40383  lclkrlem2s  40384  lclkrlem2u  40386  lclkrlem2v  40387  lclkrlem2  40391  lclkr  40392  lclkrslem1  40396  lclkrslem2  40397  lclkrs  40398  lcfrvalsnN  40400  lcfrlem4  40404  lcfrlem5  40405  lcfrlem6  40406  lcfrlem7  40407  lcfrlem9  40409  lcfrlem12N  40413  lcfrlem15  40416  lcfrlem16  40417  lcfrlem17  40418  lcfrlem19  40420  lcfrlem20  40421  lcfrlem21  40422  lcfrlem23  40424  lcfrlem25  40426  lcfrlem26  40427  lcfrlem28  40429  lcfrlem29  40430  lcfrlem30  40431  lcfrlem31  40432  lcfrlem33  40434  lcfrlem35  40436  lcfrlem36  40437  lcfrlem37  40438  lcfrlem40  40441  lcfrlem42  40443  lcfr  40444  lcdvbase  40452  lcdvbasecl  40455  lcdvaddval  40457  lcdsca  40458  lcdvsval  40463  lcd0v  40470  lcd0v2  40471  lcdvsubval  40477  lcdlss  40478  lcdlsp  40480  mapdval2N  40489  mapdordlem2  40496  mapdsn  40500  mapd1dim2lem1N  40503  mapdrvallem2  40504  mapdunirnN  40509  mapdcv  40519  mapdin  40521  mapdlsm  40523  mapd0  40524  mapdcnvatN  40525  mapdat  40526  mapdspex  40527  mapdn0  40528  mapdncol  40529  mapdindp  40530  mapdpglem1  40531  mapdpglem2  40532  mapdpglem2a  40533  mapdpglem3  40534  mapdpglem4N  40535  mapdpglem5N  40536  mapdpglem6  40537  mapdpglem8  40538  mapdpglem9  40539  mapdpglem12  40542  mapdpglem13  40543  mapdpglem14  40544  mapdpglem17N  40547  mapdpglem18  40548  mapdpglem19  40549  mapdpglem20  40550  mapdpglem21  40551  mapdpglem23  40553  mapdpglem30a  40554  mapdpglem30b  40555  mapdpglem29  40559  mapdpglem30  40561  mapdheq2  40588  mapdheq4lem  40590  mapdh6lem1N  40592  mapdh6lem2N  40593  mapdh6aN  40594  mapdh6b0N  40595  mapdh6bN  40596  mapdh6cN  40597  mapdh6dN  40598  mapdh6eN  40599  mapdh6gN  40601  mapdh6hN  40602  mapdh6iN  40603  mapdh8ab  40636  mapdh8ad  40638  mapdh8e  40643  mapdh9a  40648  mapdh9aOLDN  40649  hdmap1val0  40658  hdmap1l6lem1  40666  hdmap1l6lem2  40667  hdmap1l6a  40668  hdmap1l6b0N  40669  hdmap1l6b  40670  hdmap1l6c  40671  hdmap1l6d  40672  hdmap1l6e  40673  hdmap1l6g  40675  hdmap1l6h  40676  hdmap1l6i  40677  hdmap1eulem  40681  hdmap1eulemOLDN  40682  hdmapval0  40692  hdmapeveclem  40693  hdmapval3lemN  40696  hdmap10lem  40698  hdmap10  40699  hdmap11lem1  40700  hdmap11lem2  40701  hdmapeq0  40703  hdmapneg  40705  hdmapsub  40706  hdmap11  40707  hdmaprnlem1N  40708  hdmaprnlem3N  40709  hdmaprnlem3uN  40710  hdmaprnlem4tN  40711  hdmaprnlem4N  40712  hdmaprnlem6N  40713  hdmaprnlem8N  40715  hdmaprnlem9N  40716  hdmaprnlem3eN  40717  hdmaprnlem16N  40721  hdmaprnlem17N  40722  hdmap14lem1a  40725  hdmap14lem2a  40726  hdmap14lem2N  40728  hdmap14lem3  40729  hdmap14lem4a  40730  hdmap14lem6  40732  hdmap14lem8  40734  hdmap14lem9  40735  hdmap14lem10  40736  hdmap14lem11  40737  hdmap14lem13  40739  hgmapval0  40751  hgmapval1  40752  hgmapadd  40753  hgmapmul  40754  hgmaprnlem2N  40756  hgmaprnlem3N  40757  hgmap11  40761  hgmapeq0  40763  hdmapln1  40765  hdmaplna1  40766  hdmaplns1  40767  hdmaplnm1  40768  hdmapgln2  40771  hdmaplkr  40772  hdmapellkr  40773  hdmapip0  40774  hdmapinvlem1  40777  hdmapinvlem3  40779  hdmapinvlem4  40780  hdmapglem5  40781  hgmapvvlem1  40782  hgmapvvlem3  40784  hdmapglem7a  40786  hdmapglem7b  40787  hdmapglem7  40788  hdmapoc  40790  hlhilphllem  40822
  Copyright terms: Public domain W3C validator