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

Theorem dvhlmod 36980
Description: The full vector space  U constructed from a Hilbert lattice  K (given a fiducial hyperplane 
W) is a left module. (Contributed by NM, 23-May-2015.)
Hypotheses
Ref Expression
dvhlvec.h  |-  H  =  ( LHyp `  K
)
dvhlvec.u  |-  U  =  ( ( DVecH `  K
) `  W )
dvhlvec.k  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
Assertion
Ref Expression
dvhlmod  |-  ( ph  ->  U  e.  LMod )

Proof of Theorem dvhlmod
StepHypRef Expression
1 dvhlvec.h . . 3  |-  H  =  ( LHyp `  K
)
2 dvhlvec.u . . 3  |-  U  =  ( ( DVecH `  K
) `  W )
3 dvhlvec.k . . 3  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
41, 2, 3dvhlvec 36979 . 2  |-  ( ph  ->  U  e.  LVec )
5 lveclmod 17879 . 2  |-  ( U  e.  LVec  ->  U  e. 
LMod )
64, 5syl 16 1  |-  ( ph  ->  U  e.  LMod )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395    e. wcel 1819   ` cfv 5594   LModclmod 17639   LVecclvec 17875   HLchlt 35218   LHypclh 35851   DVecHcdvh 36948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-riotaBAD 34827
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-iin 4335  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-tpos 6973  df-undef 7020  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-map 7440  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-n0 10817  df-z 10886  df-uz 11107  df-fz 11698  df-struct 14646  df-ndx 14647  df-slot 14648  df-base 14649  df-sets 14650  df-ress 14651  df-plusg 14725  df-mulr 14726  df-sca 14728  df-vsca 14729  df-0g 14859  df-preset 15684  df-poset 15702  df-plt 15715  df-lub 15731  df-glb 15732  df-join 15733  df-meet 15734  df-p0 15796  df-p1 15797  df-lat 15803  df-clat 15865  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-grp 16184  df-minusg 16185  df-mgp 17269  df-ur 17281  df-ring 17327  df-oppr 17399  df-dvdsr 17417  df-unit 17418  df-invr 17448  df-dvr 17459  df-drng 17525  df-lmod 17641  df-lvec 17876  df-oposet 35044  df-ol 35046  df-oml 35047  df-covers 35134  df-ats 35135  df-atl 35166  df-cvlat 35190  df-hlat 35219  df-llines 35365  df-lplanes 35366  df-lvols 35367  df-lines 35368  df-psubsp 35370  df-pmap 35371  df-padd 35663  df-lhyp 35855  df-laut 35856  df-ldil 35971  df-ltrn 35972  df-trl 36027  df-tendo 36624  df-edring 36626  df-dvech 36949
This theorem is referenced by:  dvh0g  36981  dvhopellsm  36987  dib1dim2  37038  diclspsn  37064  cdlemn4a  37069  cdlemn5pre  37070  cdlemn11c  37079  dihjustlem  37086  dihord1  37088  dihord2a  37089  dihord2b  37090  dihord11c  37094  dihlsscpre  37104  dihvalcqat  37109  dihord6apre  37126  dihord5b  37129  dihord5apre  37132  dih0vbN  37152  dihglblem5  37168  dihjatc3  37183  dihmeetlem9N  37185  dihmeetlem13N  37189  dihmeetlem16N  37192  dihmeetlem19N  37195  dih1dimatlem  37199  dihlsprn  37201  dihlspsnat  37203  dihatlat  37204  dihatexv  37208  dihglblem6  37210  dochspss  37248  dochocsp  37249  dochspocN  37250  dochsncom  37252  dochsat  37253  dochshpncl  37254  dochlkr  37255  dochkrshp  37256  dochnoncon  37261  dochnel  37263  djhsumss  37277  djhunssN  37279  djhlsmcl  37284  dihjatcclem1  37288  dihjatcclem2  37289  dihjat  37293  dihprrnlem1N  37294  dihprrnlem2  37295  dihprrn  37296  djhlsmat  37297  dihjat1lem  37298  dihjat1  37299  dihsmsprn  37300  dihjat2  37301  dihsmatrn  37306  dvh3dimatN  37309  dvh2dimatN  37310  dvh1dim  37312  dvh4dimlem  37313  dvhdimlem  37314  dvh2dim  37315  dvh3dim  37316  dvh4dimN  37317  dvh3dim2  37318  dvh3dim3N  37319  dochsatshp  37321  dochsatshpb  37322  dochsnshp  37323  dochshpsat  37324  dochkrsat  37325  dochkrsat2  37326  dochkrsm  37328  dochexmidlem1  37330  dochexmidlem2  37331  dochexmidlem4  37333  dochexmidlem5  37334  dochexmidlem6  37335  dochexmidlem7  37336  dochexmidlem8  37337  dochexmid  37338  dochsnkrlem1  37339  dochsnkr  37342  dochsnkr2cl  37344  dochfl1  37346  dochfln0  37347  dochkr1  37348  dochkr1OLDN  37349  lcfl4N  37365  lcfl5  37366  lcfl6lem  37368  lcfl7lem  37369  lcfl6  37370  lcfl8  37372  lcfl8b  37374  lcfl9a  37375  lclkrlem1  37376  lclkrlem2a  37377  lclkrlem2b  37378  lclkrlem2c  37379  lclkrlem2e  37381  lclkrlem2f  37382  lclkrlem2h  37384  lclkrlem2j  37386  lclkrlem2k  37387  lclkrlem2o  37391  lclkrlem2p  37392  lclkrlem2r  37394  lclkrlem2s  37395  lclkrlem2u  37397  lclkrlem2v  37398  lclkrlem2  37402  lclkr  37403  lclkrslem1  37407  lclkrslem2  37408  lclkrs  37409  lcfrvalsnN  37411  lcfrlem4  37415  lcfrlem5  37416  lcfrlem6  37417  lcfrlem7  37418  lcfrlem9  37420  lcfrlem12N  37424  lcfrlem15  37427  lcfrlem16  37428  lcfrlem17  37429  lcfrlem19  37431  lcfrlem20  37432  lcfrlem21  37433  lcfrlem23  37435  lcfrlem25  37437  lcfrlem26  37438  lcfrlem28  37440  lcfrlem29  37441  lcfrlem30  37442  lcfrlem31  37443  lcfrlem33  37445  lcfrlem35  37447  lcfrlem36  37448  lcfrlem37  37449  lcfrlem40  37452  lcfrlem42  37454  lcfr  37455  lcdvbase  37463  lcdvbasecl  37466  lcdvaddval  37468  lcdsca  37469  lcdvsval  37474  lcd0v  37481  lcd0v2  37482  lcdvsubval  37488  lcdlss  37489  lcdlsp  37491  mapdval2N  37500  mapdordlem2  37507  mapdsn  37511  mapd1dim2lem1N  37514  mapdrvallem2  37515  mapdunirnN  37520  mapdcv  37530  mapdin  37532  mapdlsm  37534  mapd0  37535  mapdcnvatN  37536  mapdat  37537  mapdspex  37538  mapdn0  37539  mapdncol  37540  mapdindp  37541  mapdpglem1  37542  mapdpglem2  37543  mapdpglem2a  37544  mapdpglem3  37545  mapdpglem4N  37546  mapdpglem5N  37547  mapdpglem6  37548  mapdpglem8  37549  mapdpglem9  37550  mapdpglem12  37553  mapdpglem13  37554  mapdpglem14  37555  mapdpglem17N  37558  mapdpglem18  37559  mapdpglem19  37560  mapdpglem20  37561  mapdpglem21  37562  mapdpglem23  37564  mapdpglem30a  37565  mapdpglem30b  37566  mapdpglem29  37570  mapdpglem30  37572  mapdheq2  37599  mapdheq4lem  37601  mapdh6lem1N  37603  mapdh6lem2N  37604  mapdh6aN  37605  mapdh6b0N  37606  mapdh6bN  37607  mapdh6cN  37608  mapdh6dN  37609  mapdh6eN  37610  mapdh6gN  37612  mapdh6hN  37613  mapdh6iN  37614  mapdh8ab  37647  mapdh8ad  37649  mapdh8e  37654  mapdh9a  37660  mapdh9aOLDN  37661  hdmap1val0  37670  hdmap1l6lem1  37678  hdmap1l6lem2  37679  hdmap1l6a  37680  hdmap1l6b0N  37681  hdmap1l6b  37682  hdmap1l6c  37683  hdmap1l6d  37684  hdmap1l6e  37685  hdmap1l6g  37687  hdmap1l6h  37688  hdmap1l6i  37689  hdmap1eulem  37694  hdmap1eulemOLDN  37695  hdmap1neglem1N  37698  hdmapval0  37706  hdmapeveclem  37707  hdmapval3lemN  37710  hdmap10lem  37712  hdmap10  37713  hdmap11lem1  37714  hdmap11lem2  37715  hdmapeq0  37717  hdmapneg  37719  hdmapsub  37720  hdmap11  37721  hdmaprnlem1N  37722  hdmaprnlem3N  37723  hdmaprnlem3uN  37724  hdmaprnlem4tN  37725  hdmaprnlem4N  37726  hdmaprnlem6N  37727  hdmaprnlem8N  37729  hdmaprnlem9N  37730  hdmaprnlem3eN  37731  hdmaprnlem16N  37735  hdmaprnlem17N  37736  hdmap14lem1a  37739  hdmap14lem2a  37740  hdmap14lem2N  37742  hdmap14lem3  37743  hdmap14lem4a  37744  hdmap14lem6  37746  hdmap14lem8  37748  hdmap14lem9  37749  hdmap14lem10  37750  hdmap14lem11  37751  hdmap14lem13  37753  hgmapval0  37765  hgmapval1  37766  hgmapadd  37767  hgmapmul  37768  hgmaprnlem2N  37770  hgmaprnlem3N  37771  hgmap11  37775  hgmapeq0  37777  hdmapln1  37779  hdmaplna1  37780  hdmaplns1  37781  hdmaplnm1  37782  hdmapgln2  37785  hdmaplkr  37786  hdmapellkr  37787  hdmapip0  37788  hdmapinvlem1  37791  hdmapinvlem3  37793  hdmapinvlem4  37794  hdmapglem5  37795  hgmapvvlem1  37796  hgmapvvlem3  37798  hdmapglem7a  37800  hdmapglem7b  37801  hdmapglem7  37802  hdmapoc  37804  hlhilphllem  37832
  Copyright terms: Public domain W3C validator