dvhlvec - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvhlvec		Structured version Visualization version GIF version

Theorem dvhlvec 42134

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ‘cfv 6531 Basecbs 17367 +_gcplusg 17408 ._rcmulr 17409 Scalarcsca 17411 ·_𝑠 cvsca 17412 0_gc0g 17590 inv_gcminusg 19125 LVecclvec 21357 HLchlt 40375 LHypclh 41009 LTrncltrn 41126 TEndoctendo 41777 DVecHcdvh 42103

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-riotaBAD 39978

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-tpos 8227 df-undef 8274 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-er 8701 df-map 8833 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-n0 12588 df-z 12675 df-uz 12947 df-fz 13621 df-struct 17305 df-sets 17322 df-slot 17340 df-ndx 17352 df-base 17368 df-ress 17389 df-plusg 17421 df-mulr 17422 df-sca 17424 df-vsca 17425 df-0g 17592 df-proset 18448 df-poset 18467 df-plt 18482 df-lub 18498 df-glb 18499 df-join 18500 df-meet 18501 df-p0 18577 df-p1 18578 df-lat 18586 df-clat 18653 df-mgm 18796 df-sgrp 18888 df-mnd 18904 df-grp 19127 df-minusg 19128 df-cmn 19976 df-abl 19977 df-mgp 20341 df-rng 20355 df-ur 20388 df-ring 20441 df-oppr 20547 df-dvdsr 20567 df-unit 20568 df-invr 20598 df-dvr 20611 df-drng 20962 df-lmod 21117 df-lvec 21358 df-oposet 40201 df-ol 40203 df-oml 40204 df-covers 40291 df-ats 40292 df-atl 40323 df-cvlat 40347 df-hlat 40376 df-llines 40523 df-lplanes 40524 df-lvols 40525 df-lines 40526 df-psubsp 40528 df-pmap 40529 df-padd 40821 df-lhyp 41013 df-laut 41014 df-ldil 41129 df-ltrn 41130 df-trl 41184 df-tendo 41780 df-edring 41782 df-dvech 42104

This theorem is used by: dvhlmod 42135 dih1dimatlem 42354 dihlspsnssN 42357 dihlspsnat 42358 dihpN 42361 dihlatat 42362 dochsat 42408 dochshpncl 42409 dochlkr 42410 dochkrshp 42411 dochkrshp3 42413 dvh2dimatN 42465 dvh3dim3N 42474 dochsatshp 42476 dochsatshpb 42477 dochexmidat 42484 dochexmidlem3 42487 dochsnkr 42497 dochsnkr2 42498 dochflcl 42500 dochfl1 42501 dochkr1 42503 dochkr1OLDN 42504 lcfl6lem 42523 lcfl7lem 42524 lcfl9a 42530 lclkrlem1 42531 lclkrlem2a 42532 lclkrlem2e 42536 lclkrlem2g 42538 lclkrlem2h 42539 lclkrlem2o 42546 lclkrlem2p 42547 lclkrlem2q 42548 lclkrlem2s 42550 lclkrlem2v 42553 lclkrslem1 42562 lcfrvalsnN 42566 lcfrlem16 42583 lcfrlem20 42587 lcfrlem25 42592 lcfrlem29 42596 lcfrlem31 42598 lcfrlem33 42600 lcfrlem35 42602 lcdlvec 42616 lcdlkreqN 42647 lcdlkreq2N 42648 mapdordlem2 42662 mapdsn3 42668 mapdrvallem2 42670 mapdcnvatN 42691 mapdat 42692 mapdpglem10 42706 mapdpglem15 42711 mapdpglem17N 42713 mapdpglem18 42714 mapdpglem19 42715 mapdpglem21 42717 mapdpglem22 42718 mapdheq4lem 42756 mapdheq4 42757 mapdh6lem1N 42758 mapdh6lem2N 42759 mapdh6aN 42760 mapdh6b0N 42761 mapdh6bN 42762 mapdh6cN 42763 mapdh6dN 42764 mapdh6eN 42765 mapdh6fN 42766 mapdh6hN 42768 mapdh7eN 42773 mapdh7dN 42775 mapdh7fN 42776 mapdh75fN 42780 mapdh8aa 42801 mapdh8ab 42802 mapdh8ad 42804 mapdh8b 42805 mapdh8c 42806 mapdh8d0N 42807 mapdh8d 42808 mapdh8e 42809 mapdh9a 42814 mapdh9aOLDN 42815 hdmap1eq4N 42831 hdmap1l6lem1 42832 hdmap1l6lem2 42833 hdmap1l6a 42834 hdmap1l6b0N 42835 hdmap1l6b 42836 hdmap1l6c 42837 hdmap1l6d 42838 hdmap1l6e 42839 hdmap1l6f 42840 hdmap1l6h 42842 hdmap1eulemOLDN 42848 hdmapval0 42858 hdmapval3lemN 42862 hdmap10lem 42864 hdmap11lem1 42866 hdmap11lem2 42867 hdmaprnlem4N 42878 hdmaprnlem3eN 42883 hdmap14lem1a 42891 hdmap14lem4a 42896 hdmap14lem11 42903 hgmap11 42927 hdmaplkr 42938 hdmapip1 42941 hgmapvvlem1 42948 hgmapvvlem2 42949 hgmapvvlem3 42950 hlhillvec 42976

W3C validator