Theorem dvhlvec 38678

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ‘cfv 6336  Basecbs 16534  +_gcplusg 16616  ._rcmulr 16617  Scalarcsca 16619   ·_𝑠 cvsca 16620  0_gc0g 16764  inv_gcminusg 18163  LVecclvec 19935  HLchlt 36919  LHypclh 37553  LTrncltrn 37670  TEndoctendo 38321  DVecHcdvh 38647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10624  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645  ax-riotaBAD 36522

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-1st 7694  df-2nd 7695  df-tpos 7903  df-undef 7950  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-oadd 8117  df-er 8300  df-map 8419  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-nn 11668  df-2 11730  df-3 11731  df-4 11732  df-5 11733  df-6 11734  df-n0 11928  df-z 12014  df-uz 12276  df-fz 12933  df-struct 16536  df-ndx 16537  df-slot 16538  df-base 16540  df-sets 16541  df-ress 16542  df-plusg 16629  df-mulr 16630  df-sca 16632  df-vsca 16633  df-0g 16766  df-proset 17597  df-poset 17615  df-plt 17627  df-lub 17643  df-glb 17644  df-join 17645  df-meet 17646  df-p0 17708  df-p1 17709  df-lat 17715  df-clat 17777  df-mgm 17911  df-sgrp 17960  df-mnd 17971  df-grp 18165  df-minusg 18166  df-mgp 19301  df-ur 19313  df-ring 19360  df-oppr 19437  df-dvdsr 19455  df-unit 19456  df-invr 19486  df-dvr 19497  df-drng 19565  df-lmod 19697  df-lvec 19936  df-oposet 36745  df-ol 36747  df-oml 36748  df-covers 36835  df-ats 36836  df-atl 36867  df-cvlat 36891  df-hlat 36920  df-llines 37067  df-lplanes 37068  df-lvols 37069  df-lines 37070  df-psubsp 37072  df-pmap 37073  df-padd 37365  df-lhyp 37557  df-laut 37558  df-ldil 37673  df-ltrn 37674  df-trl 37728  df-tendo 38324  df-edring 38326  df-dvech 38648

This theorem is referenced by:  dvhlmod  38679  dih1dimatlem  38898  dihlspsnssN  38901  dihlspsnat  38902  dihpN  38905  dihlatat  38906  dochsat  38952  dochshpncl  38953  dochlkr  38954  dochkrshp  38955  dochkrshp3  38957  dvh2dimatN  39009  dvh3dim3N  39018  dochsatshp  39020  dochsatshpb  39021  dochexmidat  39028  dochexmidlem3  39031  dochsnkr  39041  dochsnkr2  39042  dochflcl  39044  dochfl1  39045  dochkr1  39047  dochkr1OLDN  39048  lcfl6lem  39067  lcfl7lem  39068  lcfl9a  39074  lclkrlem1  39075  lclkrlem2a  39076  lclkrlem2e  39080  lclkrlem2g  39082  lclkrlem2h  39083  lclkrlem2o  39090  lclkrlem2p  39091  lclkrlem2q  39092  lclkrlem2s  39094  lclkrlem2v  39097  lclkrslem1  39106  lcfrvalsnN  39110  lcfrlem16  39127  lcfrlem20  39131  lcfrlem25  39136  lcfrlem29  39140  lcfrlem31  39142  lcfrlem33  39144  lcfrlem35  39146  lcdlvec  39160  lcdlkreqN  39191  lcdlkreq2N  39192  mapdordlem2  39206  mapdsn3  39212  mapdrvallem2  39214  mapdcnvatN  39235  mapdat  39236  mapdpglem10  39250  mapdpglem15  39255  mapdpglem17N  39257  mapdpglem18  39258  mapdpglem19  39259  mapdpglem21  39261  mapdpglem22  39262  mapdheq4lem  39300  mapdheq4  39301  mapdh6lem1N  39302  mapdh6lem2N  39303  mapdh6aN  39304  mapdh6b0N  39305  mapdh6bN  39306  mapdh6cN  39307  mapdh6dN  39308  mapdh6eN  39309  mapdh6fN  39310  mapdh6hN  39312  mapdh7eN  39317  mapdh7dN  39319  mapdh7fN  39320  mapdh75fN  39324  mapdh8aa  39345  mapdh8ab  39346  mapdh8ad  39348  mapdh8b  39349  mapdh8c  39350  mapdh8d0N  39351  mapdh8d  39352  mapdh8e  39353  mapdh9a  39358  mapdh9aOLDN  39359  hdmap1eq4N  39375  hdmap1l6lem1  39376  hdmap1l6lem2  39377  hdmap1l6a  39378  hdmap1l6b0N  39379  hdmap1l6b  39380  hdmap1l6c  39381  hdmap1l6d  39382  hdmap1l6e  39383  hdmap1l6f  39384  hdmap1l6h  39386  hdmap1eulemOLDN  39392  hdmapval0  39402  hdmapval3lemN  39406  hdmap10lem  39408  hdmap11lem1  39410  hdmap11lem2  39411  hdmaprnlem4N  39422  hdmaprnlem3eN  39427  hdmap14lem1a  39435  hdmap14lem4a  39440  hdmap14lem11  39447  hgmap11  39471  hdmaplkr  39482  hdmapip1  39485  hgmapvvlem1  39492  hgmapvvlem2  39493  hgmapvvlem3  39494  hlhillvec  39520