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 41112
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 41111 . 2 (𝜑𝑈 ∈ LVec)
5 lveclmod 21105 . 2 (𝑈 ∈ LVec → 𝑈 ∈ LMod)
64, 5syl 17 1 (𝜑𝑈 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  cfv 6561  LModclmod 20858  LVecclvec 21101  HLchlt 39351  LHypclh 39986  DVecHcdvh 41080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-riotaBAD 38954
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-tpos 8251  df-undef 8298  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-0g 17486  df-proset 18340  df-poset 18359  df-plt 18375  df-lub 18391  df-glb 18392  df-join 18393  df-meet 18394  df-p0 18470  df-p1 18471  df-lat 18477  df-clat 18544  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954  df-minusg 18955  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-oppr 20334  df-dvdsr 20357  df-unit 20358  df-invr 20388  df-dvr 20401  df-drng 20731  df-lmod 20860  df-lvec 21102  df-oposet 39177  df-ol 39179  df-oml 39180  df-covers 39267  df-ats 39268  df-atl 39299  df-cvlat 39323  df-hlat 39352  df-llines 39500  df-lplanes 39501  df-lvols 39502  df-lines 39503  df-psubsp 39505  df-pmap 39506  df-padd 39798  df-lhyp 39990  df-laut 39991  df-ldil 40106  df-ltrn 40107  df-trl 40161  df-tendo 40757  df-edring 40759  df-dvech 41081
This theorem is referenced by:  dvh0g  41113  dvhopellsm  41119  dib1dim2  41170  diclspsn  41196  cdlemn4a  41201  cdlemn5pre  41202  cdlemn11c  41211  dihjustlem  41218  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord11c  41226  dihlsscpre  41236  dihvalcqat  41241  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dih0vbN  41284  dihglblem5  41300  dihjatc3  41315  dihmeetlem9N  41317  dihmeetlem13N  41321  dihmeetlem16N  41324  dihmeetlem19N  41327  dih1dimatlem  41331  dihlsprn  41333  dihlspsnat  41335  dihatlat  41336  dihatexv  41340  dihglblem6  41342  dochspss  41380  dochocsp  41381  dochspocN  41382  dochsncom  41384  dochsat  41385  dochshpncl  41386  dochlkr  41387  dochkrshp  41388  dochnoncon  41393  dochnel  41395  djhsumss  41409  djhunssN  41411  djhlsmcl  41416  dihjatcclem1  41420  dihjatcclem2  41421  dihjat  41425  dihprrnlem1N  41426  dihprrnlem2  41427  dihprrn  41428  djhlsmat  41429  dihjat1lem  41430  dihjat1  41431  dihsmsprn  41432  dihjat2  41433  dihsmatrn  41438  dvh3dimatN  41441  dvh2dimatN  41442  dvh1dim  41444  dvh4dimlem  41445  dvhdimlem  41446  dvh2dim  41447  dvh3dim  41448  dvh4dimN  41449  dvh3dim2  41450  dvh3dim3N  41451  dochsatshp  41453  dochsatshpb  41454  dochsnshp  41455  dochshpsat  41456  dochkrsat  41457  dochkrsat2  41458  dochkrsm  41460  dochexmidlem1  41462  dochexmidlem2  41463  dochexmidlem4  41465  dochexmidlem5  41466  dochexmidlem6  41467  dochexmidlem7  41468  dochexmidlem8  41469  dochexmid  41470  dochsnkrlem1  41471  dochsnkr  41474  dochsnkr2cl  41476  dochfl1  41478  dochfln0  41479  dochkr1  41480  dochkr1OLDN  41481  lcfl4N  41497  lcfl5  41498  lcfl6lem  41500  lcfl7lem  41501  lcfl6  41502  lcfl8  41504  lcfl8b  41506  lcfl9a  41507  lclkrlem1  41508  lclkrlem2a  41509  lclkrlem2b  41510  lclkrlem2c  41511  lclkrlem2e  41513  lclkrlem2f  41514  lclkrlem2h  41516  lclkrlem2j  41518  lclkrlem2k  41519  lclkrlem2o  41523  lclkrlem2p  41524  lclkrlem2r  41526  lclkrlem2s  41527  lclkrlem2u  41529  lclkrlem2v  41530  lclkrlem2  41534  lclkr  41535  lclkrslem1  41539  lclkrslem2  41540  lclkrs  41541  lcfrvalsnN  41543  lcfrlem4  41547  lcfrlem5  41548  lcfrlem6  41549  lcfrlem7  41550  lcfrlem9  41552  lcfrlem12N  41556  lcfrlem15  41559  lcfrlem16  41560  lcfrlem17  41561  lcfrlem19  41563  lcfrlem20  41564  lcfrlem21  41565  lcfrlem23  41567  lcfrlem25  41569  lcfrlem26  41570  lcfrlem28  41572  lcfrlem29  41573  lcfrlem30  41574  lcfrlem31  41575  lcfrlem33  41577  lcfrlem35  41579  lcfrlem36  41580  lcfrlem37  41581  lcfrlem40  41584  lcfrlem42  41586  lcfr  41587  lcdvbase  41595  lcdvbasecl  41598  lcdvaddval  41600  lcdsca  41601  lcdvsval  41606  lcd0v  41613  lcd0v2  41614  lcdvsubval  41620  lcdlss  41621  lcdlsp  41623  mapdval2N  41632  mapdordlem2  41639  mapdsn  41643  mapd1dim2lem1N  41646  mapdrvallem2  41647  mapdunirnN  41652  mapdcv  41662  mapdin  41664  mapdlsm  41666  mapd0  41667  mapdcnvatN  41668  mapdat  41669  mapdspex  41670  mapdn0  41671  mapdncol  41672  mapdindp  41673  mapdpglem1  41674  mapdpglem2  41675  mapdpglem2a  41676  mapdpglem3  41677  mapdpglem4N  41678  mapdpglem5N  41679  mapdpglem6  41680  mapdpglem8  41681  mapdpglem9  41682  mapdpglem12  41685  mapdpglem13  41686  mapdpglem14  41687  mapdpglem17N  41690  mapdpglem18  41691  mapdpglem19  41692  mapdpglem20  41693  mapdpglem21  41694  mapdpglem23  41696  mapdpglem30a  41697  mapdpglem30b  41698  mapdpglem29  41702  mapdpglem30  41704  mapdheq2  41731  mapdheq4lem  41733  mapdh6lem1N  41735  mapdh6lem2N  41736  mapdh6aN  41737  mapdh6b0N  41738  mapdh6bN  41739  mapdh6cN  41740  mapdh6dN  41741  mapdh6eN  41742  mapdh6gN  41744  mapdh6hN  41745  mapdh6iN  41746  mapdh8ab  41779  mapdh8ad  41781  mapdh8e  41786  mapdh9a  41791  mapdh9aOLDN  41792  hdmap1val0  41801  hdmap1l6lem1  41809  hdmap1l6lem2  41810  hdmap1l6a  41811  hdmap1l6b0N  41812  hdmap1l6b  41813  hdmap1l6c  41814  hdmap1l6d  41815  hdmap1l6e  41816  hdmap1l6g  41818  hdmap1l6h  41819  hdmap1l6i  41820  hdmap1eulem  41824  hdmap1eulemOLDN  41825  hdmapval0  41835  hdmapeveclem  41836  hdmapval3lemN  41839  hdmap10lem  41841  hdmap10  41842  hdmap11lem1  41843  hdmap11lem2  41844  hdmapeq0  41846  hdmapneg  41848  hdmapsub  41849  hdmap11  41850  hdmaprnlem1N  41851  hdmaprnlem3N  41852  hdmaprnlem3uN  41853  hdmaprnlem4tN  41854  hdmaprnlem4N  41855  hdmaprnlem6N  41856  hdmaprnlem8N  41858  hdmaprnlem9N  41859  hdmaprnlem3eN  41860  hdmaprnlem16N  41864  hdmaprnlem17N  41865  hdmap14lem1a  41868  hdmap14lem2a  41869  hdmap14lem2N  41871  hdmap14lem3  41872  hdmap14lem4a  41873  hdmap14lem6  41875  hdmap14lem8  41877  hdmap14lem9  41878  hdmap14lem10  41879  hdmap14lem11  41880  hdmap14lem13  41882  hgmapval0  41894  hgmapval1  41895  hgmapadd  41896  hgmapmul  41897  hgmaprnlem2N  41899  hgmaprnlem3N  41900  hgmap11  41904  hgmapeq0  41906  hdmapln1  41908  hdmaplna1  41909  hdmaplns1  41910  hdmaplnm1  41911  hdmapgln2  41914  hdmaplkr  41915  hdmapellkr  41916  hdmapip0  41917  hdmapinvlem1  41920  hdmapinvlem3  41922  hdmapinvlem4  41923  hdmapglem5  41924  hgmapvvlem1  41925  hgmapvvlem3  41927  hdmapglem7a  41929  hdmapglem7b  41930  hdmapglem7  41931  hdmapoc  41933  hlhilphllem  41965
  Copyright terms: Public domain W3C validator