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 42259

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 2760	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		dvhlvec.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
4		eqid 2760	. . 3 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
5		eqid 2760	. . 3 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
6		dvhlvec.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		eqid 2760	. . 3 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
8		eqid 2760	. . 3 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
9		eqid 2760	. . 3 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
10		eqid 2760	. . 3 ⊢ (0_g‘(Scalar‘𝑈)) = (0_g‘(Scalar‘𝑈))
11		eqid 2760	. . 3 ⊢ (inv_g‘(Scalar‘𝑈)) = (inv_g‘(Scalar‘𝑈))
12		eqid 2760	. . 3 ⊢ (._r‘(Scalar‘𝑈)) = (._r‘(Scalar‘𝑈))
13		eqid 2760	. . 3 ⊢ ( ·_𝑠 ‘𝑈) = ( ·_𝑠 ‘𝑈)
14	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	dvhlveclem 42258	. 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 1569 ∈ wcel 2144 ‘cfv 6538 Basecbs 17392 +_gcplusg 17433 ._rcmulr 17434 Scalarcsca 17436 ·_𝑠 cvsca 17437 0_gc0g 17615 inv_gcminusg 19150 LVecclvec 21382 HLchlt 40500 LHypclh 41134 LTrncltrn 41251 TEndoctendo 41902 DVecHcdvh 42228

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-riotaBAD 40103

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-tpos 8246 df-undef 8293 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-er 8720 df-map 8852 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-5 12411 df-6 12412 df-n0 12610 df-z 12697 df-uz 12969 df-fz 13643 df-struct 17330 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-ress 17414 df-plusg 17446 df-mulr 17447 df-sca 17449 df-vsca 17450 df-0g 17617 df-proset 18473 df-poset 18492 df-plt 18507 df-lub 18523 df-glb 18524 df-join 18525 df-meet 18526 df-p0 18602 df-p1 18603 df-lat 18611 df-clat 18678 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-grp 19152 df-minusg 19153 df-cmn 20001 df-abl 20002 df-mgp 20366 df-rng 20380 df-ur 20413 df-ring 20466 df-oppr 20572 df-dvdsr 20592 df-unit 20593 df-invr 20623 df-dvr 20636 df-drng 20987 df-lmod 21142 df-lvec 21383 df-oposet 40326 df-ol 40328 df-oml 40329 df-covers 40416 df-ats 40417 df-atl 40448 df-cvlat 40472 df-hlat 40501 df-llines 40648 df-lplanes 40649 df-lvols 40650 df-lines 40651 df-psubsp 40653 df-pmap 40654 df-padd 40946 df-lhyp 41138 df-laut 41139 df-ldil 41254 df-ltrn 41255 df-trl 41309 df-tendo 41905 df-edring 41907 df-dvech 42229

This theorem is used by: dvhlmod 42260 dih1dimatlem 42479 dihlspsnssN 42482 dihlspsnat 42483 dihpN 42486 dihlatat 42487 dochsat 42533 dochshpncl 42534 dochlkr 42535 dochkrshp 42536 dochkrshp3 42538 dvh2dimatN 42590 dvh3dim3N 42599 dochsatshp 42601 dochsatshpb 42602 dochexmidat 42609 dochexmidlem3 42612 dochsnkr 42622 dochsnkr2 42623 dochflcl 42625 dochfl1 42626 dochkr1 42628 dochkr1OLDN 42629 lcfl6lem 42648 lcfl7lem 42649 lcfl9a 42655 lclkrlem1 42656 lclkrlem2a 42657 lclkrlem2e 42661 lclkrlem2g 42663 lclkrlem2h 42664 lclkrlem2o 42671 lclkrlem2p 42672 lclkrlem2q 42673 lclkrlem2s 42675 lclkrlem2v 42678 lclkrslem1 42687 lcfrvalsnN 42691 lcfrlem16 42708 lcfrlem20 42712 lcfrlem25 42717 lcfrlem29 42721 lcfrlem31 42723 lcfrlem33 42725 lcfrlem35 42727 lcdlvec 42741 lcdlkreqN 42772 lcdlkreq2N 42773 mapdordlem2 42787 mapdsn3 42793 mapdrvallem2 42795 mapdcnvatN 42816 mapdat 42817 mapdpglem10 42831 mapdpglem15 42836 mapdpglem17N 42838 mapdpglem18 42839 mapdpglem19 42840 mapdpglem21 42842 mapdpglem22 42843 mapdheq4lem 42881 mapdheq4 42882 mapdh6lem1N 42883 mapdh6lem2N 42884 mapdh6aN 42885 mapdh6b0N 42886 mapdh6bN 42887 mapdh6cN 42888 mapdh6dN 42889 mapdh6eN 42890 mapdh6fN 42891 mapdh6hN 42893 mapdh7eN 42898 mapdh7dN 42900 mapdh7fN 42901 mapdh75fN 42905 mapdh8aa 42926 mapdh8ab 42927 mapdh8ad 42929 mapdh8b 42930 mapdh8c 42931 mapdh8d0N 42932 mapdh8d 42933 mapdh8e 42934 mapdh9a 42939 mapdh9aOLDN 42940 hdmap1eq4N 42956 hdmap1l6lem1 42957 hdmap1l6lem2 42958 hdmap1l6a 42959 hdmap1l6b0N 42960 hdmap1l6b 42961 hdmap1l6c 42962 hdmap1l6d 42963 hdmap1l6e 42964 hdmap1l6f 42965 hdmap1l6h 42967 hdmap1eulemOLDN 42973 hdmapval0 42983 hdmapval3lemN 42987 hdmap10lem 42989 hdmap11lem1 42991 hdmap11lem2 42992 hdmaprnlem4N 43003 hdmaprnlem3eN 43008 hdmap14lem1a 43016 hdmap14lem4a 43021 hdmap14lem11 43028 hgmap11 43052 hdmaplkr 43063 hdmapip1 43066 hgmapvvlem1 43073 hgmapvvlem2 43074 hgmapvvlem3 43075 hlhillvec 43101

W3C validator