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 37185
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 37184 . 2 (𝜑𝑈 ∈ LVec)
5 lveclmod 19465 . 2 (𝑈 ∈ LVec → 𝑈 ∈ LMod)
64, 5syl 17 1 (𝜑𝑈 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  wcel 2166  cfv 6123  LModclmod 19219  LVecclvec 19461  HLchlt 35425  LHypclh 36059  DVecHcdvh 37153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-riotaBAD 35028
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-iin 4743  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-tpos 7617  df-undef 7664  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-oadd 7830  df-er 8009  df-map 8124  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-n0 11619  df-z 11705  df-uz 11969  df-fz 12620  df-struct 16224  df-ndx 16225  df-slot 16226  df-base 16228  df-sets 16229  df-ress 16230  df-plusg 16318  df-mulr 16319  df-sca 16321  df-vsca 16322  df-0g 16455  df-proset 17281  df-poset 17299  df-plt 17311  df-lub 17327  df-glb 17328  df-join 17329  df-meet 17330  df-p0 17392  df-p1 17393  df-lat 17399  df-clat 17461  df-mgm 17595  df-sgrp 17637  df-mnd 17648  df-grp 17779  df-minusg 17780  df-mgp 18844  df-ur 18856  df-ring 18903  df-oppr 18977  df-dvdsr 18995  df-unit 18996  df-invr 19026  df-dvr 19037  df-drng 19105  df-lmod 19221  df-lvec 19462  df-oposet 35251  df-ol 35253  df-oml 35254  df-covers 35341  df-ats 35342  df-atl 35373  df-cvlat 35397  df-hlat 35426  df-llines 35573  df-lplanes 35574  df-lvols 35575  df-lines 35576  df-psubsp 35578  df-pmap 35579  df-padd 35871  df-lhyp 36063  df-laut 36064  df-ldil 36179  df-ltrn 36180  df-trl 36234  df-tendo 36830  df-edring 36832  df-dvech 37154
This theorem is referenced by:  dvh0g  37186  dvhopellsm  37192  dib1dim2  37243  diclspsn  37269  cdlemn4a  37274  cdlemn5pre  37275  cdlemn11c  37284  dihjustlem  37291  dihord1  37293  dihord2a  37294  dihord2b  37295  dihord11c  37299  dihlsscpre  37309  dihvalcqat  37314  dihord6apre  37331  dihord5b  37334  dihord5apre  37337  dih0vbN  37357  dihglblem5  37373  dihjatc3  37388  dihmeetlem9N  37390  dihmeetlem13N  37394  dihmeetlem16N  37397  dihmeetlem19N  37400  dih1dimatlem  37404  dihlsprn  37406  dihlspsnat  37408  dihatlat  37409  dihatexv  37413  dihglblem6  37415  dochspss  37453  dochocsp  37454  dochspocN  37455  dochsncom  37457  dochsat  37458  dochshpncl  37459  dochlkr  37460  dochkrshp  37461  dochnoncon  37466  dochnel  37468  djhsumss  37482  djhunssN  37484  djhlsmcl  37489  dihjatcclem1  37493  dihjatcclem2  37494  dihjat  37498  dihprrnlem1N  37499  dihprrnlem2  37500  dihprrn  37501  djhlsmat  37502  dihjat1lem  37503  dihjat1  37504  dihsmsprn  37505  dihjat2  37506  dihsmatrn  37511  dvh3dimatN  37514  dvh2dimatN  37515  dvh1dim  37517  dvh4dimlem  37518  dvhdimlem  37519  dvh2dim  37520  dvh3dim  37521  dvh4dimN  37522  dvh3dim2  37523  dvh3dim3N  37524  dochsatshp  37526  dochsatshpb  37527  dochsnshp  37528  dochshpsat  37529  dochkrsat  37530  dochkrsat2  37531  dochkrsm  37533  dochexmidlem1  37535  dochexmidlem2  37536  dochexmidlem4  37538  dochexmidlem5  37539  dochexmidlem6  37540  dochexmidlem7  37541  dochexmidlem8  37542  dochexmid  37543  dochsnkrlem1  37544  dochsnkr  37547  dochsnkr2cl  37549  dochfl1  37551  dochfln0  37552  dochkr1  37553  dochkr1OLDN  37554  lcfl4N  37570  lcfl5  37571  lcfl6lem  37573  lcfl7lem  37574  lcfl6  37575  lcfl8  37577  lcfl8b  37579  lcfl9a  37580  lclkrlem1  37581  lclkrlem2a  37582  lclkrlem2b  37583  lclkrlem2c  37584  lclkrlem2e  37586  lclkrlem2f  37587  lclkrlem2h  37589  lclkrlem2j  37591  lclkrlem2k  37592  lclkrlem2o  37596  lclkrlem2p  37597  lclkrlem2r  37599  lclkrlem2s  37600  lclkrlem2u  37602  lclkrlem2v  37603  lclkrlem2  37607  lclkr  37608  lclkrslem1  37612  lclkrslem2  37613  lclkrs  37614  lcfrvalsnN  37616  lcfrlem4  37620  lcfrlem5  37621  lcfrlem6  37622  lcfrlem7  37623  lcfrlem9  37625  lcfrlem12N  37629  lcfrlem15  37632  lcfrlem16  37633  lcfrlem17  37634  lcfrlem19  37636  lcfrlem20  37637  lcfrlem21  37638  lcfrlem23  37640  lcfrlem25  37642  lcfrlem26  37643  lcfrlem28  37645  lcfrlem29  37646  lcfrlem30  37647  lcfrlem31  37648  lcfrlem33  37650  lcfrlem35  37652  lcfrlem36  37653  lcfrlem37  37654  lcfrlem40  37657  lcfrlem42  37659  lcfr  37660  lcdvbase  37668  lcdvbasecl  37671  lcdvaddval  37673  lcdsca  37674  lcdvsval  37679  lcd0v  37686  lcd0v2  37687  lcdvsubval  37693  lcdlss  37694  lcdlsp  37696  mapdval2N  37705  mapdordlem2  37712  mapdsn  37716  mapd1dim2lem1N  37719  mapdrvallem2  37720  mapdunirnN  37725  mapdcv  37735  mapdin  37737  mapdlsm  37739  mapd0  37740  mapdcnvatN  37741  mapdat  37742  mapdspex  37743  mapdn0  37744  mapdncol  37745  mapdindp  37746  mapdpglem1  37747  mapdpglem2  37748  mapdpglem2a  37749  mapdpglem3  37750  mapdpglem4N  37751  mapdpglem5N  37752  mapdpglem6  37753  mapdpglem8  37754  mapdpglem9  37755  mapdpglem12  37758  mapdpglem13  37759  mapdpglem14  37760  mapdpglem17N  37763  mapdpglem18  37764  mapdpglem19  37765  mapdpglem20  37766  mapdpglem21  37767  mapdpglem23  37769  mapdpglem30a  37770  mapdpglem30b  37771  mapdpglem29  37775  mapdpglem30  37777  mapdheq2  37804  mapdheq4lem  37806  mapdh6lem1N  37808  mapdh6lem2N  37809  mapdh6aN  37810  mapdh6b0N  37811  mapdh6bN  37812  mapdh6cN  37813  mapdh6dN  37814  mapdh6eN  37815  mapdh6gN  37817  mapdh6hN  37818  mapdh6iN  37819  mapdh8ab  37852  mapdh8ad  37854  mapdh8e  37859  mapdh9a  37864  mapdh9aOLDN  37865  hdmap1val0  37874  hdmap1l6lem1  37882  hdmap1l6lem2  37883  hdmap1l6a  37884  hdmap1l6b0N  37885  hdmap1l6b  37886  hdmap1l6c  37887  hdmap1l6d  37888  hdmap1l6e  37889  hdmap1l6g  37891  hdmap1l6h  37892  hdmap1l6i  37893  hdmap1eulem  37897  hdmap1eulemOLDN  37898  hdmapval0  37908  hdmapeveclem  37909  hdmapval3lemN  37912  hdmap10lem  37914  hdmap10  37915  hdmap11lem1  37916  hdmap11lem2  37917  hdmapeq0  37919  hdmapneg  37921  hdmapsub  37922  hdmap11  37923  hdmaprnlem1N  37924  hdmaprnlem3N  37925  hdmaprnlem3uN  37926  hdmaprnlem4tN  37927  hdmaprnlem4N  37928  hdmaprnlem6N  37929  hdmaprnlem8N  37931  hdmaprnlem9N  37932  hdmaprnlem3eN  37933  hdmaprnlem16N  37937  hdmaprnlem17N  37938  hdmap14lem1a  37941  hdmap14lem2a  37942  hdmap14lem2N  37944  hdmap14lem3  37945  hdmap14lem4a  37946  hdmap14lem6  37948  hdmap14lem8  37950  hdmap14lem9  37951  hdmap14lem10  37952  hdmap14lem11  37953  hdmap14lem13  37955  hgmapval0  37967  hgmapval1  37968  hgmapadd  37969  hgmapmul  37970  hgmaprnlem2N  37972  hgmaprnlem3N  37973  hgmap11  37977  hgmapeq0  37979  hdmapln1  37981  hdmaplna1  37982  hdmaplns1  37983  hdmaplnm1  37984  hdmapgln2  37987  hdmaplkr  37988  hdmapellkr  37989  hdmapip0  37990  hdmapinvlem1  37993  hdmapinvlem3  37995  hdmapinvlem4  37996  hdmapglem5  37997  hgmapvvlem1  37998  hgmapvvlem3  38000  hdmapglem7a  38002  hdmapglem7b  38003  hdmapglem7  38004  hdmapoc  38006  hlhilphllem  38034
  Copyright terms: Public domain W3C validator