Theorem dvhlvec 41066

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
dvhlvec	⊢ (𝜑 → 𝑈 ∈ LVec)

Proof of Theorem dvhlvec

Step	Hyp	Ref	Expression
1		dvhlvec.k	. 2 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		eqid 2740	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		dvhlvec.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
4		eqid 2740	. . 3 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
5		eqid 2740	. . 3 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
6		dvhlvec.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		eqid 2740	. . 3 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
8		eqid 2740	. . 3 ⊢ (+g‘(Scalar‘𝑈)) = (+g‘(Scalar‘𝑈))
9		eqid 2740	. . 3 ⊢ (+g‘𝑈) = (+g‘𝑈)
10		eqid 2740	. . 3 ⊢ (0g‘(Scalar‘𝑈)) = (0g‘(Scalar‘𝑈))
11		eqid 2740	. . 3 ⊢ (invg‘(Scalar‘𝑈)) = (invg‘(Scalar‘𝑈))
12		eqid 2740	. . 3 ⊢ (.r‘(Scalar‘𝑈)) = (.r‘(Scalar‘𝑈))
13		eqid 2740	. . 3 ⊢ ( ·𝑠 ‘𝑈) = ( ·𝑠 ‘𝑈)
14	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	dvhlveclem 41065	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec)
15	1, 14	syl 17	1 ⊢ (𝜑 → 𝑈 ∈ LVec)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  Basecbs 17258  +_gcplusg 17311  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  0_gc0g 17499  inv_gcminusg 18974  LVecclvec 21124  HLchlt 39306  LHypclh 39941  LTrncltrn 40058  TEndoctendo 40709  DVecHcdvh 41035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-riotaBAD 38909

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-tpos 8267  df-undef 8314  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-n0 12554  df-z 12640  df-uz 12904  df-fz 13568  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-sca 17327  df-vsca 17328  df-0g 17501  df-proset 18365  df-poset 18383  df-plt 18400  df-lub 18416  df-glb 18417  df-join 18418  df-meet 18419  df-p0 18495  df-p1 18496  df-lat 18502  df-clat 18569  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976  df-minusg 18977  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-ring 20262  df-oppr 20360  df-dvdsr 20383  df-unit 20384  df-invr 20414  df-dvr 20427  df-drng 20753  df-lmod 20882  df-lvec 21125  df-oposet 39132  df-ol 39134  df-oml 39135  df-covers 39222  df-ats 39223  df-atl 39254  df-cvlat 39278  df-hlat 39307  df-llines 39455  df-lplanes 39456  df-lvols 39457  df-lines 39458  df-psubsp 39460  df-pmap 39461  df-padd 39753  df-lhyp 39945  df-laut 39946  df-ldil 40061  df-ltrn 40062  df-trl 40116  df-tendo 40712  df-edring 40714  df-dvech 41036

This theorem is referenced by:  dvhlmod  41067  dih1dimatlem  41286  dihlspsnssN  41289  dihlspsnat  41290  dihpN  41293  dihlatat  41294  dochsat  41340  dochshpncl  41341  dochlkr  41342  dochkrshp  41343  dochkrshp3  41345  dvh2dimatN  41397  dvh3dim3N  41406  dochsatshp  41408  dochsatshpb  41409  dochexmidat  41416  dochexmidlem3  41419  dochsnkr  41429  dochsnkr2  41430  dochflcl  41432  dochfl1  41433  dochkr1  41435  dochkr1OLDN  41436  lcfl6lem  41455  lcfl7lem  41456  lcfl9a  41462  lclkrlem1  41463  lclkrlem2a  41464  lclkrlem2e  41468  lclkrlem2g  41470  lclkrlem2h  41471  lclkrlem2o  41478  lclkrlem2p  41479  lclkrlem2q  41480  lclkrlem2s  41482  lclkrlem2v  41485  lclkrslem1  41494  lcfrvalsnN  41498  lcfrlem16  41515  lcfrlem20  41519  lcfrlem25  41524  lcfrlem29  41528  lcfrlem31  41530  lcfrlem33  41532  lcfrlem35  41534  lcdlvec  41548  lcdlkreqN  41579  lcdlkreq2N  41580  mapdordlem2  41594  mapdsn3  41600  mapdrvallem2  41602  mapdcnvatN  41623  mapdat  41624  mapdpglem10  41638  mapdpglem15  41643  mapdpglem17N  41645  mapdpglem18  41646  mapdpglem19  41647  mapdpglem21  41649  mapdpglem22  41650  mapdheq4lem  41688  mapdheq4  41689  mapdh6lem1N  41690  mapdh6lem2N  41691  mapdh6aN  41692  mapdh6b0N  41693  mapdh6bN  41694  mapdh6cN  41695  mapdh6dN  41696  mapdh6eN  41697  mapdh6fN  41698  mapdh6hN  41700  mapdh7eN  41705  mapdh7dN  41707  mapdh7fN  41708  mapdh75fN  41712  mapdh8aa  41733  mapdh8ab  41734  mapdh8ad  41736  mapdh8b  41737  mapdh8c  41738  mapdh8d0N  41739  mapdh8d  41740  mapdh8e  41741  mapdh9a  41746  mapdh9aOLDN  41747  hdmap1eq4N  41763  hdmap1l6lem1  41764  hdmap1l6lem2  41765  hdmap1l6a  41766  hdmap1l6b0N  41767  hdmap1l6b  41768  hdmap1l6c  41769  hdmap1l6d  41770  hdmap1l6e  41771  hdmap1l6f  41772  hdmap1l6h  41774  hdmap1eulemOLDN  41780  hdmapval0  41790  hdmapval3lemN  41794  hdmap10lem  41796  hdmap11lem1  41798  hdmap11lem2  41799  hdmaprnlem4N  41810  hdmaprnlem3eN  41815  hdmap14lem1a  41823  hdmap14lem4a  41828  hdmap14lem11  41835  hgmap11  41859  hdmaplkr  41870  hdmapip1  41873  hgmapvvlem1  41880  hgmapvvlem2  41881  hgmapvvlem3  41882  hlhillvec  41912