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

Theorem dvhlmod 36539
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 36538 . 2  |-  ( ph  ->  U  e.  LVec )
5 lveclmod 17620 . 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 1381    e. wcel 1802   ` cfv 5574   LModclmod 17380   LVecclvec 17616   HLchlt 34777   LHypclh 35410   DVecHcdvh 36507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-riotaBAD 34386
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-iin 4314  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-1st 6781  df-2nd 6782  df-tpos 6953  df-undef 7000  df-recs 7040  df-rdg 7074  df-1o 7128  df-oadd 7132  df-er 7309  df-map 7420  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-n0 10797  df-z 10866  df-uz 11086  df-fz 11677  df-struct 14506  df-ndx 14507  df-slot 14508  df-base 14509  df-sets 14510  df-ress 14511  df-plusg 14582  df-mulr 14583  df-sca 14585  df-vsca 14586  df-0g 14711  df-preset 15426  df-poset 15444  df-plt 15457  df-lub 15473  df-glb 15474  df-join 15475  df-meet 15476  df-p0 15538  df-p1 15539  df-lat 15545  df-clat 15607  df-mgm 15741  df-sgrp 15780  df-mnd 15790  df-grp 15926  df-minusg 15927  df-mgp 17010  df-ur 17022  df-ring 17068  df-oppr 17140  df-dvdsr 17158  df-unit 17159  df-invr 17189  df-dvr 17200  df-drng 17266  df-lmod 17382  df-lvec 17617  df-oposet 34603  df-ol 34605  df-oml 34606  df-covers 34693  df-ats 34694  df-atl 34725  df-cvlat 34749  df-hlat 34778  df-llines 34924  df-lplanes 34925  df-lvols 34926  df-lines 34927  df-psubsp 34929  df-pmap 34930  df-padd 35222  df-lhyp 35414  df-laut 35415  df-ldil 35530  df-ltrn 35531  df-trl 35586  df-tendo 36183  df-edring 36185  df-dvech 36508
This theorem is referenced by:  dvh0g  36540  dvhopellsm  36546  dib1dim2  36597  diclspsn  36623  cdlemn4a  36628  cdlemn5pre  36629  cdlemn11c  36638  dihjustlem  36645  dihord1  36647  dihord2a  36648  dihord2b  36649  dihord11c  36653  dihlsscpre  36663  dihvalcqat  36668  dihord6apre  36685  dihord5b  36688  dihord5apre  36691  dih0vbN  36711  dihglblem5  36727  dihjatc3  36742  dihmeetlem9N  36744  dihmeetlem13N  36748  dihmeetlem16N  36751  dihmeetlem19N  36754  dih1dimatlem  36758  dihlsprn  36760  dihlspsnat  36762  dihatlat  36763  dihatexv  36767  dihglblem6  36769  dochspss  36807  dochocsp  36808  dochspocN  36809  dochsncom  36811  dochsat  36812  dochshpncl  36813  dochlkr  36814  dochkrshp  36815  dochnoncon  36820  dochnel  36822  djhsumss  36836  djhunssN  36838  djhlsmcl  36843  dihjatcclem1  36847  dihjatcclem2  36848  dihjat  36852  dihprrnlem1N  36853  dihprrnlem2  36854  dihprrn  36855  djhlsmat  36856  dihjat1lem  36857  dihjat1  36858  dihsmsprn  36859  dihjat2  36860  dihsmatrn  36865  dvh3dimatN  36868  dvh2dimatN  36869  dvh1dim  36871  dvh4dimlem  36872  dvhdimlem  36873  dvh2dim  36874  dvh3dim  36875  dvh4dimN  36876  dvh3dim2  36877  dvh3dim3N  36878  dochsatshp  36880  dochsatshpb  36881  dochsnshp  36882  dochshpsat  36883  dochkrsat  36884  dochkrsat2  36885  dochkrsm  36887  dochexmidlem1  36889  dochexmidlem2  36890  dochexmidlem4  36892  dochexmidlem5  36893  dochexmidlem6  36894  dochexmidlem7  36895  dochexmidlem8  36896  dochexmid  36897  dochsnkrlem1  36898  dochsnkr  36901  dochsnkr2cl  36903  dochfl1  36905  dochfln0  36906  dochkr1  36907  dochkr1OLDN  36908  lcfl4N  36924  lcfl5  36925  lcfl6lem  36927  lcfl7lem  36928  lcfl6  36929  lcfl8  36931  lcfl8b  36933  lcfl9a  36934  lclkrlem1  36935  lclkrlem2a  36936  lclkrlem2b  36937  lclkrlem2c  36938  lclkrlem2e  36940  lclkrlem2f  36941  lclkrlem2h  36943  lclkrlem2j  36945  lclkrlem2k  36946  lclkrlem2o  36950  lclkrlem2p  36951  lclkrlem2r  36953  lclkrlem2s  36954  lclkrlem2u  36956  lclkrlem2v  36957  lclkrlem2  36961  lclkr  36962  lclkrslem1  36966  lclkrslem2  36967  lclkrs  36968  lcfrvalsnN  36970  lcfrlem4  36974  lcfrlem5  36975  lcfrlem6  36976  lcfrlem7  36977  lcfrlem9  36979  lcfrlem12N  36983  lcfrlem15  36986  lcfrlem16  36987  lcfrlem17  36988  lcfrlem19  36990  lcfrlem20  36991  lcfrlem21  36992  lcfrlem23  36994  lcfrlem25  36996  lcfrlem26  36997  lcfrlem28  36999  lcfrlem29  37000  lcfrlem30  37001  lcfrlem31  37002  lcfrlem33  37004  lcfrlem35  37006  lcfrlem36  37007  lcfrlem37  37008  lcfrlem40  37011  lcfrlem42  37013  lcfr  37014  lcdvbase  37022  lcdvbasecl  37025  lcdvaddval  37027  lcdsca  37028  lcdvsval  37033  lcd0v  37040  lcd0v2  37041  lcdvsubval  37047  lcdlss  37048  lcdlsp  37050  mapdval2N  37059  mapdordlem2  37066  mapdsn  37070  mapd1dim2lem1N  37073  mapdrvallem2  37074  mapdunirnN  37079  mapdcv  37089  mapdin  37091  mapdlsm  37093  mapd0  37094  mapdcnvatN  37095  mapdat  37096  mapdspex  37097  mapdn0  37098  mapdncol  37099  mapdindp  37100  mapdpglem1  37101  mapdpglem2  37102  mapdpglem2a  37103  mapdpglem3  37104  mapdpglem4N  37105  mapdpglem5N  37106  mapdpglem6  37107  mapdpglem8  37108  mapdpglem9  37109  mapdpglem12  37112  mapdpglem13  37113  mapdpglem14  37114  mapdpglem17N  37117  mapdpglem18  37118  mapdpglem19  37119  mapdpglem20  37120  mapdpglem21  37121  mapdpglem23  37123  mapdpglem30a  37124  mapdpglem30b  37125  mapdpglem29  37129  mapdpglem30  37131  mapdheq2  37158  mapdheq4lem  37160  mapdh6lem1N  37162  mapdh6lem2N  37163  mapdh6aN  37164  mapdh6b0N  37165  mapdh6bN  37166  mapdh6cN  37167  mapdh6dN  37168  mapdh6eN  37169  mapdh6gN  37171  mapdh6hN  37172  mapdh6iN  37173  mapdh8ab  37206  mapdh8ad  37208  mapdh8e  37213  mapdh9a  37219  mapdh9aOLDN  37220  hdmap1val0  37229  hdmap1l6lem1  37237  hdmap1l6lem2  37238  hdmap1l6a  37239  hdmap1l6b0N  37240  hdmap1l6b  37241  hdmap1l6c  37242  hdmap1l6d  37243  hdmap1l6e  37244  hdmap1l6g  37246  hdmap1l6h  37247  hdmap1l6i  37248  hdmap1eulem  37253  hdmap1eulemOLDN  37254  hdmap1neglem1N  37257  hdmapval0  37265  hdmapeveclem  37266  hdmapval3lemN  37269  hdmap10lem  37271  hdmap10  37272  hdmap11lem1  37273  hdmap11lem2  37274  hdmapeq0  37276  hdmapneg  37278  hdmapsub  37279  hdmap11  37280  hdmaprnlem1N  37281  hdmaprnlem3N  37282  hdmaprnlem3uN  37283  hdmaprnlem4tN  37284  hdmaprnlem4N  37285  hdmaprnlem6N  37286  hdmaprnlem8N  37288  hdmaprnlem9N  37289  hdmaprnlem3eN  37290  hdmaprnlem16N  37294  hdmaprnlem17N  37295  hdmap14lem1a  37298  hdmap14lem2a  37299  hdmap14lem2N  37301  hdmap14lem3  37302  hdmap14lem4a  37303  hdmap14lem6  37305  hdmap14lem8  37307  hdmap14lem9  37308  hdmap14lem10  37309  hdmap14lem11  37310  hdmap14lem13  37312  hgmapval0  37324  hgmapval1  37325  hgmapadd  37326  hgmapmul  37327  hgmaprnlem2N  37329  hgmaprnlem3N  37330  hgmap11  37334  hgmapeq0  37336  hdmapln1  37338  hdmaplna1  37339  hdmaplns1  37340  hdmaplnm1  37341  hdmapgln2  37344  hdmaplkr  37345  hdmapellkr  37346  hdmapip0  37347  hdmapinvlem1  37350  hdmapinvlem3  37352  hdmapinvlem4  37353  hdmapglem5  37354  hgmapvvlem1  37355  hgmapvvlem3  37357  hdmapglem7a  37359  hdmapglem7b  37360  hdmapglem7  37361  hdmapoc  37363  hlhilphllem  37391
  Copyright terms: Public domain W3C validator