Theorem dvhlvec 41569

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 2737	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		dvhlvec.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
4		eqid 2737	. . 3 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
5		eqid 2737	. . 3 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
6		dvhlvec.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		eqid 2737	. . 3 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
8		eqid 2737	. . 3 ⊢ (+g‘(Scalar‘𝑈)) = (+g‘(Scalar‘𝑈))
9		eqid 2737	. . 3 ⊢ (+g‘𝑈) = (+g‘𝑈)
10		eqid 2737	. . 3 ⊢ (0g‘(Scalar‘𝑈)) = (0g‘(Scalar‘𝑈))
11		eqid 2737	. . 3 ⊢ (invg‘(Scalar‘𝑈)) = (invg‘(Scalar‘𝑈))
12		eqid 2737	. . 3 ⊢ (.r‘(Scalar‘𝑈)) = (.r‘(Scalar‘𝑈))
13		eqid 2737	. . 3 ⊢ ( ·𝑠 ‘𝑈) = ( ·𝑠 ‘𝑈)
14	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	dvhlveclem 41568	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec)
15	1, 14	syl 17	1 ⊢ (𝜑 → 𝑈 ∈ LVec)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  Basecbs 17170  +_gcplusg 17211  ._rcmulr 17212  Scalarcsca 17214   ·_𝑠 cvsca 17215  0_gc0g 17393  inv_gcminusg 18901  LVecclvec 21089  HLchlt 39810  LHypclh 40444  LTrncltrn 40561  TEndoctendo 41212  DVecHcdvh 41538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-riotaBAD 39413

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  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 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-tpos 8169  df-undef 8216  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-er 8636  df-map 8768  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-n0 12429  df-z 12516  df-uz 12780  df-fz 13453  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-sca 17227  df-vsca 17228  df-0g 17395  df-proset 18251  df-poset 18270  df-plt 18285  df-lub 18301  df-glb 18302  df-join 18303  df-meet 18304  df-p0 18380  df-p1 18381  df-lat 18389  df-clat 18456  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903  df-minusg 18904  df-cmn 19748  df-abl 19749  df-mgp 20113  df-rng 20125  df-ur 20154  df-ring 20207  df-oppr 20308  df-dvdsr 20328  df-unit 20329  df-invr 20359  df-dvr 20372  df-drng 20699  df-lmod 20848  df-lvec 21090  df-oposet 39636  df-ol 39638  df-oml 39639  df-covers 39726  df-ats 39727  df-atl 39758  df-cvlat 39782  df-hlat 39811  df-llines 39958  df-lplanes 39959  df-lvols 39960  df-lines 39961  df-psubsp 39963  df-pmap 39964  df-padd 40256  df-lhyp 40448  df-laut 40449  df-ldil 40564  df-ltrn 40565  df-trl 40619  df-tendo 41215  df-edring 41217  df-dvech 41539

This theorem is referenced by:  dvhlmod  41570  dih1dimatlem  41789  dihlspsnssN  41792  dihlspsnat  41793  dihpN  41796  dihlatat  41797  dochsat  41843  dochshpncl  41844  dochlkr  41845  dochkrshp  41846  dochkrshp3  41848  dvh2dimatN  41900  dvh3dim3N  41909  dochsatshp  41911  dochsatshpb  41912  dochexmidat  41919  dochexmidlem3  41922  dochsnkr  41932  dochsnkr2  41933  dochflcl  41935  dochfl1  41936  dochkr1  41938  dochkr1OLDN  41939  lcfl6lem  41958  lcfl7lem  41959  lcfl9a  41965  lclkrlem1  41966  lclkrlem2a  41967  lclkrlem2e  41971  lclkrlem2g  41973  lclkrlem2h  41974  lclkrlem2o  41981  lclkrlem2p  41982  lclkrlem2q  41983  lclkrlem2s  41985  lclkrlem2v  41988  lclkrslem1  41997  lcfrvalsnN  42001  lcfrlem16  42018  lcfrlem20  42022  lcfrlem25  42027  lcfrlem29  42031  lcfrlem31  42033  lcfrlem33  42035  lcfrlem35  42037  lcdlvec  42051  lcdlkreqN  42082  lcdlkreq2N  42083  mapdordlem2  42097  mapdsn3  42103  mapdrvallem2  42105  mapdcnvatN  42126  mapdat  42127  mapdpglem10  42141  mapdpglem15  42146  mapdpglem17N  42148  mapdpglem18  42149  mapdpglem19  42150  mapdpglem21  42152  mapdpglem22  42153  mapdheq4lem  42191  mapdheq4  42192  mapdh6lem1N  42193  mapdh6lem2N  42194  mapdh6aN  42195  mapdh6b0N  42196  mapdh6bN  42197  mapdh6cN  42198  mapdh6dN  42199  mapdh6eN  42200  mapdh6fN  42201  mapdh6hN  42203  mapdh7eN  42208  mapdh7dN  42210  mapdh7fN  42211  mapdh75fN  42215  mapdh8aa  42236  mapdh8ab  42237  mapdh8ad  42239  mapdh8b  42240  mapdh8c  42241  mapdh8d0N  42242  mapdh8d  42243  mapdh8e  42244  mapdh9a  42249  mapdh9aOLDN  42250  hdmap1eq4N  42266  hdmap1l6lem1  42267  hdmap1l6lem2  42268  hdmap1l6a  42269  hdmap1l6b0N  42270  hdmap1l6b  42271  hdmap1l6c  42272  hdmap1l6d  42273  hdmap1l6e  42274  hdmap1l6f  42275  hdmap1l6h  42277  hdmap1eulemOLDN  42283  hdmapval0  42293  hdmapval3lemN  42297  hdmap10lem  42299  hdmap11lem1  42301  hdmap11lem2  42302  hdmaprnlem4N  42313  hdmaprnlem3eN  42318  hdmap14lem1a  42326  hdmap14lem4a  42331  hdmap14lem11  42338  hgmap11  42362  hdmaplkr  42373  hdmapip1  42376  hgmapvvlem1  42383  hgmapvvlem2  42384  hgmapvvlem3  42385  hlhillvec  42411