Theorem dvhlvec 41608

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 41607	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec)
15	1, 14	syl 17	1 ⊢ (𝜑 → 𝑈 ∈ LVec)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  Basecbs 17177  +_gcplusg 17218  ._rcmulr 17219  Scalarcsca 17221   ·_𝑠 cvsca 17222  0_gc0g 17400  inv_gcminusg 18908  LVecclvec 21099  HLchlt 39849  LHypclh 40483  LTrncltrn 40600  TEndoctendo 41251  DVecHcdvh 41577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113  ax-riotaBAD 39452

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-iun 4930  df-iin 4931  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-1st 7938  df-2nd 7939  df-tpos 8173  df-undef 8220  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-er 8640  df-map 8772  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-2 12242  df-3 12243  df-4 12244  df-5 12245  df-6 12246  df-n0 12436  df-z 12523  df-uz 12787  df-fz 13460  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-ress 17199  df-plusg 17231  df-mulr 17232  df-sca 17234  df-vsca 17235  df-0g 17402  df-proset 18258  df-poset 18277  df-plt 18292  df-lub 18308  df-glb 18309  df-join 18310  df-meet 18311  df-p0 18387  df-p1 18388  df-lat 18396  df-clat 18463  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-grp 18910  df-minusg 18911  df-cmn 19755  df-abl 19756  df-mgp 20120  df-rng 20132  df-ur 20161  df-ring 20214  df-oppr 20315  df-dvdsr 20335  df-unit 20336  df-invr 20366  df-dvr 20379  df-drng 20710  df-lmod 20859  df-lvec 21100  df-oposet 39675  df-ol 39677  df-oml 39678  df-covers 39765  df-ats 39766  df-atl 39797  df-cvlat 39821  df-hlat 39850  df-llines 39997  df-lplanes 39998  df-lvols 39999  df-lines 40000  df-psubsp 40002  df-pmap 40003  df-padd 40295  df-lhyp 40487  df-laut 40488  df-ldil 40603  df-ltrn 40604  df-trl 40658  df-tendo 41254  df-edring 41256  df-dvech 41578

This theorem is referenced by:  dvhlmod  41609  dih1dimatlem  41828  dihlspsnssN  41831  dihlspsnat  41832  dihpN  41835  dihlatat  41836  dochsat  41882  dochshpncl  41883  dochlkr  41884  dochkrshp  41885  dochkrshp3  41887  dvh2dimatN  41939  dvh3dim3N  41948  dochsatshp  41950  dochsatshpb  41951  dochexmidat  41958  dochexmidlem3  41961  dochsnkr  41971  dochsnkr2  41972  dochflcl  41974  dochfl1  41975  dochkr1  41977  dochkr1OLDN  41978  lcfl6lem  41997  lcfl7lem  41998  lcfl9a  42004  lclkrlem1  42005  lclkrlem2a  42006  lclkrlem2e  42010  lclkrlem2g  42012  lclkrlem2h  42013  lclkrlem2o  42020  lclkrlem2p  42021  lclkrlem2q  42022  lclkrlem2s  42024  lclkrlem2v  42027  lclkrslem1  42036  lcfrvalsnN  42040  lcfrlem16  42057  lcfrlem20  42061  lcfrlem25  42066  lcfrlem29  42070  lcfrlem31  42072  lcfrlem33  42074  lcfrlem35  42076  lcdlvec  42090  lcdlkreqN  42121  lcdlkreq2N  42122  mapdordlem2  42136  mapdsn3  42142  mapdrvallem2  42144  mapdcnvatN  42165  mapdat  42166  mapdpglem10  42180  mapdpglem15  42185  mapdpglem17N  42187  mapdpglem18  42188  mapdpglem19  42189  mapdpglem21  42191  mapdpglem22  42192  mapdheq4lem  42230  mapdheq4  42231  mapdh6lem1N  42232  mapdh6lem2N  42233  mapdh6aN  42234  mapdh6b0N  42235  mapdh6bN  42236  mapdh6cN  42237  mapdh6dN  42238  mapdh6eN  42239  mapdh6fN  42240  mapdh6hN  42242  mapdh7eN  42247  mapdh7dN  42249  mapdh7fN  42250  mapdh75fN  42254  mapdh8aa  42275  mapdh8ab  42276  mapdh8ad  42278  mapdh8b  42279  mapdh8c  42280  mapdh8d0N  42281  mapdh8d  42282  mapdh8e  42283  mapdh9a  42288  mapdh9aOLDN  42289  hdmap1eq4N  42305  hdmap1l6lem1  42306  hdmap1l6lem2  42307  hdmap1l6a  42308  hdmap1l6b0N  42309  hdmap1l6b  42310  hdmap1l6c  42311  hdmap1l6d  42312  hdmap1l6e  42313  hdmap1l6f  42314  hdmap1l6h  42316  hdmap1eulemOLDN  42322  hdmapval0  42332  hdmapval3lemN  42336  hdmap10lem  42338  hdmap11lem1  42340  hdmap11lem2  42341  hdmaprnlem4N  42352  hdmaprnlem3eN  42357  hdmap14lem1a  42365  hdmap14lem4a  42370  hdmap14lem11  42377  hgmap11  42401  hdmaplkr  42412  hdmapip1  42415  hgmapvvlem1  42422  hgmapvvlem2  42423  hgmapvvlem3  42424  hlhillvec  42450