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 41924

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 2766	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		dvhlvec.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
4		eqid 2766	. . 3 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
5		eqid 2766	. . 3 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
6		dvhlvec.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		eqid 2766	. . 3 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
8		eqid 2766	. . 3 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
9		eqid 2766	. . 3 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
10		eqid 2766	. . 3 ⊢ (0_g‘(Scalar‘𝑈)) = (0_g‘(Scalar‘𝑈))
11		eqid 2766	. . 3 ⊢ (inv_g‘(Scalar‘𝑈)) = (inv_g‘(Scalar‘𝑈))
12		eqid 2766	. . 3 ⊢ (._r‘(Scalar‘𝑈)) = (._r‘(Scalar‘𝑈))
13		eqid 2766	. . 3 ⊢ ( ·_𝑠 ‘𝑈) = ( ·_𝑠 ‘𝑈)
14	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	dvhlveclem 41923	. 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 2146 ‘cfv 6543 Basecbs 17294 +_gcplusg 17335 ._rcmulr 17336 Scalarcsca 17338 ·_𝑠 cvsca 17339 0_gc0g 17517 inv_gcminusg 19032 LVecclvec 21260 HLchlt 40165 LHypclh 40799 LTrncltrn 40916 TEndoctendo 41567 DVecHcdvh 41893

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-riotaBAD 39768

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4878 df-iun 4963 df-iin 4964 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-tpos 8231 df-undef 8278 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8703 df-map 8835 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-nn 12252 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-n0 12523 df-z 12610 df-uz 12881 df-fz 13554 df-struct 17232 df-sets 17249 df-slot 17267 df-ndx 17279 df-base 17295 df-ress 17316 df-plusg 17348 df-mulr 17349 df-sca 17351 df-vsca 17352 df-0g 17519 df-proset 18375 df-poset 18394 df-plt 18409 df-lub 18425 df-glb 18426 df-join 18427 df-meet 18428 df-p0 18504 df-p1 18505 df-lat 18513 df-clat 18580 df-mgm 18723 df-sgrp 18806 df-mnd 18822 df-grp 19034 df-minusg 19035 df-cmn 19883 df-abl 19884 df-mgp 20248 df-rng 20262 df-ur 20295 df-ring 20348 df-oppr 20452 df-dvdsr 20472 df-unit 20473 df-invr 20503 df-dvr 20516 df-drng 20866 df-lmod 21020 df-lvec 21261 df-oposet 39991 df-ol 39993 df-oml 39994 df-covers 40081 df-ats 40082 df-atl 40113 df-cvlat 40137 df-hlat 40166 df-llines 40313 df-lplanes 40314 df-lvols 40315 df-lines 40316 df-psubsp 40318 df-pmap 40319 df-padd 40611 df-lhyp 40803 df-laut 40804 df-ldil 40919 df-ltrn 40920 df-trl 40974 df-tendo 41570 df-edring 41572 df-dvech 41894

This theorem is used by: dvhlmod 41925 dih1dimatlem 42144 dihlspsnssN 42147 dihlspsnat 42148 dihpN 42151 dihlatat 42152 dochsat 42198 dochshpncl 42199 dochlkr 42200 dochkrshp 42201 dochkrshp3 42203 dvh2dimatN 42255 dvh3dim3N 42264 dochsatshp 42266 dochsatshpb 42267 dochexmidat 42274 dochexmidlem3 42277 dochsnkr 42287 dochsnkr2 42288 dochflcl 42290 dochfl1 42291 dochkr1 42293 dochkr1OLDN 42294 lcfl6lem 42313 lcfl7lem 42314 lcfl9a 42320 lclkrlem1 42321 lclkrlem2a 42322 lclkrlem2e 42326 lclkrlem2g 42328 lclkrlem2h 42329 lclkrlem2o 42336 lclkrlem2p 42337 lclkrlem2q 42338 lclkrlem2s 42340 lclkrlem2v 42343 lclkrslem1 42352 lcfrvalsnN 42356 lcfrlem16 42373 lcfrlem20 42377 lcfrlem25 42382 lcfrlem29 42386 lcfrlem31 42388 lcfrlem33 42390 lcfrlem35 42392 lcdlvec 42406 lcdlkreqN 42437 lcdlkreq2N 42438 mapdordlem2 42452 mapdsn3 42458 mapdrvallem2 42460 mapdcnvatN 42481 mapdat 42482 mapdpglem10 42496 mapdpglem15 42501 mapdpglem17N 42503 mapdpglem18 42504 mapdpglem19 42505 mapdpglem21 42507 mapdpglem22 42508 mapdheq4lem 42546 mapdheq4 42547 mapdh6lem1N 42548 mapdh6lem2N 42549 mapdh6aN 42550 mapdh6b0N 42551 mapdh6bN 42552 mapdh6cN 42553 mapdh6dN 42554 mapdh6eN 42555 mapdh6fN 42556 mapdh6hN 42558 mapdh7eN 42563 mapdh7dN 42565 mapdh7fN 42566 mapdh75fN 42570 mapdh8aa 42591 mapdh8ab 42592 mapdh8ad 42594 mapdh8b 42595 mapdh8c 42596 mapdh8d0N 42597 mapdh8d 42598 mapdh8e 42599 mapdh9a 42604 mapdh9aOLDN 42605 hdmap1eq4N 42621 hdmap1l6lem1 42622 hdmap1l6lem2 42623 hdmap1l6a 42624 hdmap1l6b0N 42625 hdmap1l6b 42626 hdmap1l6c 42627 hdmap1l6d 42628 hdmap1l6e 42629 hdmap1l6f 42630 hdmap1l6h 42632 hdmap1eulemOLDN 42638 hdmapval0 42648 hdmapval3lemN 42652 hdmap10lem 42654 hdmap11lem1 42656 hdmap11lem2 42657 hdmaprnlem4N 42668 hdmaprnlem3eN 42673 hdmap14lem1a 42681 hdmap14lem4a 42686 hdmap14lem11 42693 hgmap11 42717 hdmaplkr 42728 hdmapip1 42731 hgmapvvlem1 42738 hgmapvvlem2 42739 hgmapvvlem3 42740 hlhillvec 42766

W3C validator