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 41990

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 2762	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		dvhlvec.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
4		eqid 2762	. . 3 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
5		eqid 2762	. . 3 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
6		dvhlvec.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		eqid 2762	. . 3 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
8		eqid 2762	. . 3 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
9		eqid 2762	. . 3 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
10		eqid 2762	. . 3 ⊢ (0_g‘(Scalar‘𝑈)) = (0_g‘(Scalar‘𝑈))
11		eqid 2762	. . 3 ⊢ (inv_g‘(Scalar‘𝑈)) = (inv_g‘(Scalar‘𝑈))
12		eqid 2762	. . 3 ⊢ (._r‘(Scalar‘𝑈)) = (._r‘(Scalar‘𝑈))
13		eqid 2762	. . 3 ⊢ ( ·_𝑠 ‘𝑈) = ( ·_𝑠 ‘𝑈)
14	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	dvhlveclem 41989	. 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 6537 Basecbs 17307 +_gcplusg 17348 ._rcmulr 17349 Scalarcsca 17351 ·_𝑠 cvsca 17352 0_gc0g 17530 inv_gcminusg 19064 LVecclvec 21292 HLchlt 40231 LHypclh 40865 LTrncltrn 40982 TEndoctendo 41633 DVecHcdvh 41959

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 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-riotaBAD 39834

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-tpos 8228 df-undef 8275 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-map 8832 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-n0 12533 df-z 12620 df-uz 12892 df-fz 13566 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-sca 17364 df-vsca 17365 df-0g 17532 df-proset 18388 df-poset 18407 df-plt 18422 df-lub 18438 df-glb 18439 df-join 18440 df-meet 18441 df-p0 18517 df-p1 18518 df-lat 18526 df-clat 18593 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-grp 19066 df-minusg 19067 df-cmn 19915 df-abl 19916 df-mgp 20280 df-rng 20294 df-ur 20327 df-ring 20380 df-oppr 20484 df-dvdsr 20504 df-unit 20505 df-invr 20535 df-dvr 20548 df-drng 20898 df-lmod 21052 df-lvec 21293 df-oposet 40057 df-ol 40059 df-oml 40060 df-covers 40147 df-ats 40148 df-atl 40179 df-cvlat 40203 df-hlat 40232 df-llines 40379 df-lplanes 40380 df-lvols 40381 df-lines 40382 df-psubsp 40384 df-pmap 40385 df-padd 40677 df-lhyp 40869 df-laut 40870 df-ldil 40985 df-ltrn 40986 df-trl 41040 df-tendo 41636 df-edring 41638 df-dvech 41960

This theorem is used by: dvhlmod 41991 dih1dimatlem 42210 dihlspsnssN 42213 dihlspsnat 42214 dihpN 42217 dihlatat 42218 dochsat 42264 dochshpncl 42265 dochlkr 42266 dochkrshp 42267 dochkrshp3 42269 dvh2dimatN 42321 dvh3dim3N 42330 dochsatshp 42332 dochsatshpb 42333 dochexmidat 42340 dochexmidlem3 42343 dochsnkr 42353 dochsnkr2 42354 dochflcl 42356 dochfl1 42357 dochkr1 42359 dochkr1OLDN 42360 lcfl6lem 42379 lcfl7lem 42380 lcfl9a 42386 lclkrlem1 42387 lclkrlem2a 42388 lclkrlem2e 42392 lclkrlem2g 42394 lclkrlem2h 42395 lclkrlem2o 42402 lclkrlem2p 42403 lclkrlem2q 42404 lclkrlem2s 42406 lclkrlem2v 42409 lclkrslem1 42418 lcfrvalsnN 42422 lcfrlem16 42439 lcfrlem20 42443 lcfrlem25 42448 lcfrlem29 42452 lcfrlem31 42454 lcfrlem33 42456 lcfrlem35 42458 lcdlvec 42472 lcdlkreqN 42503 lcdlkreq2N 42504 mapdordlem2 42518 mapdsn3 42524 mapdrvallem2 42526 mapdcnvatN 42547 mapdat 42548 mapdpglem10 42562 mapdpglem15 42567 mapdpglem17N 42569 mapdpglem18 42570 mapdpglem19 42571 mapdpglem21 42573 mapdpglem22 42574 mapdheq4lem 42612 mapdheq4 42613 mapdh6lem1N 42614 mapdh6lem2N 42615 mapdh6aN 42616 mapdh6b0N 42617 mapdh6bN 42618 mapdh6cN 42619 mapdh6dN 42620 mapdh6eN 42621 mapdh6fN 42622 mapdh6hN 42624 mapdh7eN 42629 mapdh7dN 42631 mapdh7fN 42632 mapdh75fN 42636 mapdh8aa 42657 mapdh8ab 42658 mapdh8ad 42660 mapdh8b 42661 mapdh8c 42662 mapdh8d0N 42663 mapdh8d 42664 mapdh8e 42665 mapdh9a 42670 mapdh9aOLDN 42671 hdmap1eq4N 42687 hdmap1l6lem1 42688 hdmap1l6lem2 42689 hdmap1l6a 42690 hdmap1l6b0N 42691 hdmap1l6b 42692 hdmap1l6c 42693 hdmap1l6d 42694 hdmap1l6e 42695 hdmap1l6f 42696 hdmap1l6h 42698 hdmap1eulemOLDN 42704 hdmapval0 42714 hdmapval3lemN 42718 hdmap10lem 42720 hdmap11lem1 42722 hdmap11lem2 42723 hdmaprnlem4N 42734 hdmaprnlem3eN 42739 hdmap14lem1a 42747 hdmap14lem4a 42752 hdmap14lem11 42759 hgmap11 42783 hdmaplkr 42794 hdmapip1 42797 hgmapvvlem1 42804 hgmapvvlem2 42805 hgmapvvlem3 42806 hlhillvec 42832

W3C validator