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

Theorem dvhlmod 31846
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 31845 . 2  |-  ( ph  ->  U  e.  LVec )
5 lveclmod 16171 . 2  |-  ( U  e.  LVec  ->  U  e. 
LMod )
64, 5syl 16 1  |-  ( ph  ->  U  e.  LMod )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   ` cfv 5447   LModclmod 15943   LVecclvec 16167   HLchlt 30086   LHypclh 30719   DVecHcdvh 31814
This theorem is referenced by:  dvh0g  31847  dvhopellsm  31853  dib1dim2  31904  diclspsn  31930  cdlemn4a  31935  cdlemn5pre  31936  cdlemn11c  31945  dihjustlem  31952  dihord1  31954  dihord2a  31955  dihord2b  31956  dihord11c  31960  dihlsscpre  31970  dihvalcqat  31975  dihord6apre  31992  dihord5b  31995  dihord5apre  31998  dih0vbN  32018  dihglblem5  32034  dihjatc3  32049  dihmeetlem9N  32051  dihmeetlem13N  32055  dihmeetlem16N  32058  dihmeetlem19N  32061  dih1dimatlem  32065  dihlsprn  32067  dihlspsnat  32069  dihatlat  32070  dihatexv  32074  dihglblem6  32076  dochspss  32114  dochocsp  32115  dochspocN  32116  dochsncom  32118  dochsat  32119  dochshpncl  32120  dochlkr  32121  dochkrshp  32122  dochnoncon  32127  dochnel  32129  djhsumss  32143  djhunssN  32145  djhlsmcl  32150  dihjatcclem1  32154  dihjatcclem2  32155  dihjat  32159  dihprrnlem1N  32160  dihprrnlem2  32161  dihprrn  32162  djhlsmat  32163  dihjat1lem  32164  dihjat1  32165  dihsmsprn  32166  dihjat2  32167  dihsmatrn  32172  dvh3dimatN  32175  dvh2dimatN  32176  dvh1dim  32178  dvh4dimlem  32179  dvhdimlem  32180  dvh2dim  32181  dvh3dim  32182  dvh4dimN  32183  dvh3dim2  32184  dvh3dim3N  32185  dochsatshp  32187  dochsatshpb  32188  dochsnshp  32189  dochshpsat  32190  dochkrsat  32191  dochkrsat2  32192  dochkrsm  32194  dochexmidlem1  32196  dochexmidlem2  32197  dochexmidlem4  32199  dochexmidlem5  32200  dochexmidlem6  32201  dochexmidlem7  32202  dochexmidlem8  32203  dochexmid  32204  dochsnkrlem1  32205  dochsnkr  32208  dochsnkr2cl  32210  dochfl1  32212  dochfln0  32213  dochkr1  32214  dochkr1OLDN  32215  lcfl4N  32231  lcfl5  32232  lcfl6lem  32234  lcfl7lem  32235  lcfl6  32236  lcfl8  32238  lcfl8b  32240  lcfl9a  32241  lclkrlem1  32242  lclkrlem2a  32243  lclkrlem2b  32244  lclkrlem2c  32245  lclkrlem2e  32247  lclkrlem2f  32248  lclkrlem2h  32250  lclkrlem2j  32252  lclkrlem2k  32253  lclkrlem2o  32257  lclkrlem2p  32258  lclkrlem2r  32260  lclkrlem2s  32261  lclkrlem2u  32263  lclkrlem2v  32264  lclkrlem2  32268  lclkr  32269  lclkrslem1  32273  lclkrslem2  32274  lclkrs  32275  lcfrvalsnN  32277  lcfrlem4  32281  lcfrlem5  32282  lcfrlem6  32283  lcfrlem7  32284  lcfrlem9  32286  lcfrlem12N  32290  lcfrlem15  32293  lcfrlem16  32294  lcfrlem17  32295  lcfrlem19  32297  lcfrlem20  32298  lcfrlem21  32299  lcfrlem23  32301  lcfrlem25  32303  lcfrlem26  32304  lcfrlem28  32306  lcfrlem29  32307  lcfrlem30  32308  lcfrlem31  32309  lcfrlem33  32311  lcfrlem35  32313  lcfrlem36  32314  lcfrlem37  32315  lcfrlem40  32318  lcfrlem42  32320  lcfr  32321  lcdvbase  32329  lcdvbasecl  32332  lcdvaddval  32334  lcdsca  32335  lcdvsval  32340  lcd0v  32347  lcd0v2  32348  lcdvsubval  32354  lcdlss  32355  lcdlsp  32357  mapdval2N  32366  mapdordlem2  32373  mapdsn  32377  mapd1dim2lem1N  32380  mapdrvallem2  32381  mapdunirnN  32386  mapdcv  32396  mapdin  32398  mapdlsm  32400  mapd0  32401  mapdcnvatN  32402  mapdat  32403  mapdspex  32404  mapdn0  32405  mapdncol  32406  mapdindp  32407  mapdpglem1  32408  mapdpglem2  32409  mapdpglem2a  32410  mapdpglem3  32411  mapdpglem4N  32412  mapdpglem5N  32413  mapdpglem6  32414  mapdpglem8  32415  mapdpglem9  32416  mapdpglem12  32419  mapdpglem13  32420  mapdpglem14  32421  mapdpglem17N  32424  mapdpglem18  32425  mapdpglem19  32426  mapdpglem20  32427  mapdpglem21  32428  mapdpglem23  32430  mapdpglem30a  32431  mapdpglem30b  32432  mapdpglem29  32436  mapdpglem30  32438  mapdheq2  32465  mapdheq4lem  32467  mapdh6lem1N  32469  mapdh6lem2N  32470  mapdh6aN  32471  mapdh6b0N  32472  mapdh6bN  32473  mapdh6cN  32474  mapdh6dN  32475  mapdh6eN  32476  mapdh6gN  32478  mapdh6hN  32479  mapdh6iN  32480  mapdh8ab  32513  mapdh8ad  32515  mapdh8e  32520  mapdh9a  32526  mapdh9aOLDN  32527  hdmap1val0  32536  hdmap1l6lem1  32544  hdmap1l6lem2  32545  hdmap1l6a  32546  hdmap1l6b0N  32547  hdmap1l6b  32548  hdmap1l6c  32549  hdmap1l6d  32550  hdmap1l6e  32551  hdmap1l6g  32553  hdmap1l6h  32554  hdmap1l6i  32555  hdmap1eulem  32560  hdmap1eulemOLDN  32561  hdmap1neglem1N  32564  hdmapval0  32572  hdmapeveclem  32573  hdmapval3lemN  32576  hdmap10lem  32578  hdmap10  32579  hdmap11lem1  32580  hdmap11lem2  32581  hdmapeq0  32583  hdmapneg  32585  hdmapsub  32586  hdmap11  32587  hdmaprnlem1N  32588  hdmaprnlem3N  32589  hdmaprnlem3uN  32590  hdmaprnlem4tN  32591  hdmaprnlem4N  32592  hdmaprnlem6N  32593  hdmaprnlem8N  32595  hdmaprnlem9N  32596  hdmaprnlem3eN  32597  hdmaprnlem16N  32601  hdmaprnlem17N  32602  hdmap14lem1a  32605  hdmap14lem2a  32606  hdmap14lem2N  32608  hdmap14lem3  32609  hdmap14lem4a  32610  hdmap14lem6  32612  hdmap14lem8  32614  hdmap14lem9  32615  hdmap14lem10  32616  hdmap14lem11  32617  hdmap14lem13  32619  hgmapval0  32631  hgmapval1  32632  hgmapadd  32633  hgmapmul  32634  hgmaprnlem2N  32636  hgmaprnlem3N  32637  hgmap11  32641  hgmapeq0  32643  hdmapln1  32645  hdmaplna1  32646  hdmaplns1  32647  hdmaplnm1  32648  hdmapgln2  32651  hdmaplkr  32652  hdmapellkr  32653  hdmapip0  32654  hdmapinvlem1  32657  hdmapinvlem3  32659  hdmapinvlem4  32660  hdmapglem5  32661  hgmapvvlem1  32662  hgmapvvlem3  32664  hdmapglem7a  32666  hdmapglem7b  32667  hdmapglem7  32668  hdmapoc  32670  hlhilphllem  32698
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4313  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396  ax-un 4694  ax-cnex 9039  ax-resscn 9040  ax-1cn 9041  ax-icn 9042  ax-addcl 9043  ax-addrcl 9044  ax-mulcl 9045  ax-mulrcl 9046  ax-mulcom 9047  ax-addass 9048  ax-mulass 9049  ax-distr 9050  ax-i2m1 9051  ax-1ne0 9052  ax-1rid 9053  ax-rnegex 9054  ax-rrecex 9055  ax-cnre 9056  ax-pre-lttri 9057  ax-pre-lttrn 9058  ax-pre-ltadd 9059  ax-pre-mulgt0 9060
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-fal 1329  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2703  df-rex 2704  df-reu 2705  df-rmo 2706  df-rab 2707  df-v 2951  df-sbc 3155  df-csb 3245  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-tp 3815  df-op 3816  df-uni 4009  df-int 4044  df-iun 4088  df-iin 4089  df-br 4206  df-opab 4260  df-mpt 4261  df-tr 4296  df-eprel 4487  df-id 4491  df-po 4496  df-so 4497  df-fr 4534  df-we 4536  df-ord 4577  df-on 4578  df-lim 4579  df-suc 4580  df-om 4839  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-f1 5452  df-fo 5453  df-f1o 5454  df-fv 5455  df-ov 6077  df-oprab 6078  df-mpt2 6079  df-1st 6342  df-2nd 6343  df-tpos 6472  df-undef 6536  df-riota 6542  df-recs 6626  df-rdg 6661  df-1o 6717  df-oadd 6721  df-er 6898  df-map 7013  df-en 7103  df-dom 7104  df-sdom 7105  df-fin 7106  df-pnf 9115  df-mnf 9116  df-xr 9117  df-ltxr 9118  df-le 9119  df-sub 9286  df-neg 9287  df-nn 9994  df-2 10051  df-3 10052  df-4 10053  df-5 10054  df-6 10055  df-n0 10215  df-z 10276  df-uz 10482  df-fz 11037  df-struct 13464  df-ndx 13465  df-slot 13466  df-base 13467  df-sets 13468  df-ress 13469  df-plusg 13535  df-mulr 13536  df-sca 13538  df-vsca 13539  df-0g 13720  df-poset 14396  df-plt 14408  df-lub 14424  df-glb 14425  df-join 14426  df-meet 14427  df-p0 14461  df-p1 14462  df-lat 14468  df-clat 14530  df-mnd 14683  df-grp 14805  df-minusg 14806  df-mgp 15642  df-rng 15656  df-ur 15658  df-oppr 15721  df-dvdsr 15739  df-unit 15740  df-invr 15770  df-dvr 15781  df-drng 15830  df-lmod 15945  df-lvec 16168  df-oposet 29912  df-ol 29914  df-oml 29915  df-covers 30002  df-ats 30003  df-atl 30034  df-cvlat 30058  df-hlat 30087  df-llines 30233  df-lplanes 30234  df-lvols 30235  df-lines 30236  df-psubsp 30238  df-pmap 30239  df-padd 30531  df-lhyp 30723  df-laut 30724  df-ldil 30839  df-ltrn 30840  df-trl 30894  df-tendo 31490  df-edring 31492  df-dvech 31815
  Copyright terms: Public domain W3C validator