Theorem dvhlvec 41111

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  Basecbs 17247  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  0_gc0g 17484  inv_gcminusg 18952  LVecclvec 21101  HLchlt 39351  LHypclh 39986  LTrncltrn 40103  TEndoctendo 40754  DVecHcdvh 41080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-riotaBAD 38954

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-tpos 8251  df-undef 8298  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-0g 17486  df-proset 18340  df-poset 18359  df-plt 18375  df-lub 18391  df-glb 18392  df-join 18393  df-meet 18394  df-p0 18470  df-p1 18471  df-lat 18477  df-clat 18544  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954  df-minusg 18955  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-oppr 20334  df-dvdsr 20357  df-unit 20358  df-invr 20388  df-dvr 20401  df-drng 20731  df-lmod 20860  df-lvec 21102  df-oposet 39177  df-ol 39179  df-oml 39180  df-covers 39267  df-ats 39268  df-atl 39299  df-cvlat 39323  df-hlat 39352  df-llines 39500  df-lplanes 39501  df-lvols 39502  df-lines 39503  df-psubsp 39505  df-pmap 39506  df-padd 39798  df-lhyp 39990  df-laut 39991  df-ldil 40106  df-ltrn 40107  df-trl 40161  df-tendo 40757  df-edring 40759  df-dvech 41081

This theorem is referenced by:  dvhlmod  41112  dih1dimatlem  41331  dihlspsnssN  41334  dihlspsnat  41335  dihpN  41338  dihlatat  41339  dochsat  41385  dochshpncl  41386  dochlkr  41387  dochkrshp  41388  dochkrshp3  41390  dvh2dimatN  41442  dvh3dim3N  41451  dochsatshp  41453  dochsatshpb  41454  dochexmidat  41461  dochexmidlem3  41464  dochsnkr  41474  dochsnkr2  41475  dochflcl  41477  dochfl1  41478  dochkr1  41480  dochkr1OLDN  41481  lcfl6lem  41500  lcfl7lem  41501  lcfl9a  41507  lclkrlem1  41508  lclkrlem2a  41509  lclkrlem2e  41513  lclkrlem2g  41515  lclkrlem2h  41516  lclkrlem2o  41523  lclkrlem2p  41524  lclkrlem2q  41525  lclkrlem2s  41527  lclkrlem2v  41530  lclkrslem1  41539  lcfrvalsnN  41543  lcfrlem16  41560  lcfrlem20  41564  lcfrlem25  41569  lcfrlem29  41573  lcfrlem31  41575  lcfrlem33  41577  lcfrlem35  41579  lcdlvec  41593  lcdlkreqN  41624  lcdlkreq2N  41625  mapdordlem2  41639  mapdsn3  41645  mapdrvallem2  41647  mapdcnvatN  41668  mapdat  41669  mapdpglem10  41683  mapdpglem15  41688  mapdpglem17N  41690  mapdpglem18  41691  mapdpglem19  41692  mapdpglem21  41694  mapdpglem22  41695  mapdheq4lem  41733  mapdheq4  41734  mapdh6lem1N  41735  mapdh6lem2N  41736  mapdh6aN  41737  mapdh6b0N  41738  mapdh6bN  41739  mapdh6cN  41740  mapdh6dN  41741  mapdh6eN  41742  mapdh6fN  41743  mapdh6hN  41745  mapdh7eN  41750  mapdh7dN  41752  mapdh7fN  41753  mapdh75fN  41757  mapdh8aa  41778  mapdh8ab  41779  mapdh8ad  41781  mapdh8b  41782  mapdh8c  41783  mapdh8d0N  41784  mapdh8d  41785  mapdh8e  41786  mapdh9a  41791  mapdh9aOLDN  41792  hdmap1eq4N  41808  hdmap1l6lem1  41809  hdmap1l6lem2  41810  hdmap1l6a  41811  hdmap1l6b0N  41812  hdmap1l6b  41813  hdmap1l6c  41814  hdmap1l6d  41815  hdmap1l6e  41816  hdmap1l6f  41817  hdmap1l6h  41819  hdmap1eulemOLDN  41825  hdmapval0  41835  hdmapval3lemN  41839  hdmap10lem  41841  hdmap11lem1  41843  hdmap11lem2  41844  hdmaprnlem4N  41855  hdmaprnlem3eN  41860  hdmap14lem1a  41868  hdmap14lem4a  41873  hdmap14lem11  41880  hgmap11  41904  hdmaplkr  41915  hdmapip1  41918  hgmapvvlem1  41925  hgmapvvlem2  41926  hgmapvvlem3  41927  hlhillvec  41957