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 42358

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 2763	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		dvhlvec.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
4		eqid 2763	. . 3 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
5		eqid 2763	. . 3 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
6		dvhlvec.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		eqid 2763	. . 3 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
8		eqid 2763	. . 3 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
9		eqid 2763	. . 3 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
10		eqid 2763	. . 3 ⊢ (0_g‘(Scalar‘𝑈)) = (0_g‘(Scalar‘𝑈))
11		eqid 2763	. . 3 ⊢ (inv_g‘(Scalar‘𝑈)) = (inv_g‘(Scalar‘𝑈))
12		eqid 2763	. . 3 ⊢ (._r‘(Scalar‘𝑈)) = (._r‘(Scalar‘𝑈))
13		eqid 2763	. . 3 ⊢ ( ·_𝑠 ‘𝑈) = ( ·_𝑠 ‘𝑈)
14	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	dvhlveclem 42357	. 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 2147 ‘cfv 6558 Basecbs 17416 +_gcplusg 17457 ._rcmulr 17458 Scalarcsca 17460 ·_𝑠 cvsca 17461 0_gc0g 17639 inv_gcminusg 19174 LVecclvec 21407 HLchlt 40599 LHypclh 41233 LTrncltrn 41350 TEndoctendo 42001 DVecHcdvh 42327

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-riotaBAD 40202

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-tpos 8271 df-undef 8318 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-er 8745 df-map 8877 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-n0 12634 df-z 12721 df-uz 12993 df-fz 13667 df-struct 17354 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-mulr 17471 df-sca 17473 df-vsca 17474 df-0g 17641 df-proset 18497 df-poset 18516 df-plt 18531 df-lub 18547 df-glb 18548 df-join 18549 df-meet 18550 df-p0 18626 df-p1 18627 df-lat 18635 df-clat 18702 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-grp 19176 df-minusg 19177 df-cmn 20026 df-abl 20027 df-mgp 20391 df-rng 20405 df-ur 20438 df-ring 20491 df-oppr 20597 df-dvdsr 20617 df-unit 20618 df-invr 20648 df-dvr 20661 df-drng 21012 df-lmod 21167 df-lvec 21408 df-oposet 40425 df-ol 40427 df-oml 40428 df-covers 40515 df-ats 40516 df-atl 40547 df-cvlat 40571 df-hlat 40600 df-llines 40747 df-lplanes 40748 df-lvols 40749 df-lines 40750 df-psubsp 40752 df-pmap 40753 df-padd 41045 df-lhyp 41237 df-laut 41238 df-ldil 41353 df-ltrn 41354 df-trl 41408 df-tendo 42004 df-edring 42006 df-dvech 42328

This theorem is used by: dvhlmod 42359 dih1dimatlem 42578 dihlspsnssN 42581 dihlspsnat 42582 dihpN 42585 dihlatat 42586 dochsat 42632 dochshpncl 42633 dochlkr 42634 dochkrshp 42635 dochkrshp3 42637 dvh2dimatN 42689 dvh3dim3N 42698 dochsatshp 42700 dochsatshpb 42701 dochexmidat 42708 dochexmidlem3 42711 dochsnkr 42721 dochsnkr2 42722 dochflcl 42724 dochfl1 42725 dochkr1 42727 dochkr1OLDN 42728 lcfl6lem 42747 lcfl7lem 42748 lcfl9a 42754 lclkrlem1 42755 lclkrlem2a 42756 lclkrlem2e 42760 lclkrlem2g 42762 lclkrlem2h 42763 lclkrlem2o 42770 lclkrlem2p 42771 lclkrlem2q 42772 lclkrlem2s 42774 lclkrlem2v 42777 lclkrslem1 42786 lcfrvalsnN 42790 lcfrlem16 42807 lcfrlem20 42811 lcfrlem25 42816 lcfrlem29 42820 lcfrlem31 42822 lcfrlem33 42824 lcfrlem35 42826 lcdlvec 42840 lcdlkreqN 42871 lcdlkreq2N 42872 mapdordlem2 42886 mapdsn3 42892 mapdrvallem2 42894 mapdcnvatN 42915 mapdat 42916 mapdpglem10 42930 mapdpglem15 42935 mapdpglem17N 42937 mapdpglem18 42938 mapdpglem19 42939 mapdpglem21 42941 mapdpglem22 42942 mapdheq4lem 42980 mapdheq4 42981 mapdh6lem1N 42982 mapdh6lem2N 42983 mapdh6aN 42984 mapdh6b0N 42985 mapdh6bN 42986 mapdh6cN 42987 mapdh6dN 42988 mapdh6eN 42989 mapdh6fN 42990 mapdh6hN 42992 mapdh7eN 42997 mapdh7dN 42999 mapdh7fN 43000 mapdh75fN 43004 mapdh8aa 43025 mapdh8ab 43026 mapdh8ad 43028 mapdh8b 43029 mapdh8c 43030 mapdh8d0N 43031 mapdh8d 43032 mapdh8e 43033 mapdh9a 43038 mapdh9aOLDN 43039 hdmap1eq4N 43055 hdmap1l6lem1 43056 hdmap1l6lem2 43057 hdmap1l6a 43058 hdmap1l6b0N 43059 hdmap1l6b 43060 hdmap1l6c 43061 hdmap1l6d 43062 hdmap1l6e 43063 hdmap1l6f 43064 hdmap1l6h 43066 hdmap1eulemOLDN 43072 hdmapval0 43082 hdmapval3lemN 43086 hdmap10lem 43088 hdmap11lem1 43090 hdmap11lem2 43091 hdmaprnlem4N 43102 hdmaprnlem3eN 43107 hdmap14lem1a 43115 hdmap14lem4a 43120 hdmap14lem11 43127 hgmap11 43151 hdmaplkr 43162 hdmapip1 43165 hgmapvvlem1 43172 hgmapvvlem2 43173 hgmapvvlem3 43174 hlhillvec 43200

W3C validator