lcdlvec - Mathbox for Norm Megill

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

Theorem lcdlvec 42092

Description: The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015.)

**Hypotheses**
Ref	Expression
lcdlmod.h	⊢ 𝐻 = (LHyp‘𝐾)
lcdlmod.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
lcdlmod.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))

**Assertion**
Ref	Expression
lcdlvec	⊢ (𝜑 → 𝐶 ∈ LVec)

Proof of Theorem lcdlvec Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lcdlmod.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		eqid 2739	. . 3 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
3		lcdlmod.c	. . 3 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
4		eqid 2739	. . 3 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
5		eqid 2739	. . 3 ⊢ (LFnl‘((DVecH‘𝐾)‘𝑊)) = (LFnl‘((DVecH‘𝐾)‘𝑊))
6		eqid 2739	. . 3 ⊢ (LKer‘((DVecH‘𝐾)‘𝑊)) = (LKer‘((DVecH‘𝐾)‘𝑊))
7		eqid 2739	. . 3 ⊢ (LDual‘((DVecH‘𝐾)‘𝑊)) = (LDual‘((DVecH‘𝐾)‘𝑊))
8		lcdlmod.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
9	1, 2, 3, 4, 5, 6, 7, 8	lcdval 42090	. 2 ⊢ (𝜑 → 𝐶 = ((LDual‘((DVecH‘𝐾)‘𝑊)) ↾_s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}))
10	1, 4, 8	dvhlvec 41610	. . . 4 ⊢ (𝜑 → ((DVecH‘𝐾)‘𝑊) ∈ LVec)
11	7, 10	lduallvec 39655	. . 3 ⊢ (𝜑 → (LDual‘((DVecH‘𝐾)‘𝑊)) ∈ LVec)
12		eqid 2739	. . . 4 ⊢ (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) = (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊)))
13		eqid 2739	. . . 4 ⊢ {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)} = {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}
14	1, 4, 2, 5, 6, 7, 12, 13, 8	lclkr 42034	. . 3 ⊢ (𝜑 → {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)} ∈ (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))))
15		eqid 2739	. . . 4 ⊢ ((LDual‘((DVecH‘𝐾)‘𝑊)) ↾_s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}) = ((LDual‘((DVecH‘𝐾)‘𝑊)) ↾_s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)})
16	15, 12	lsslvec 21100	. . 3 ⊢ (((LDual‘((DVecH‘𝐾)‘𝑊)) ∈ LVec ∧ {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)} ∈ (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊)))) → ((LDual‘((DVecH‘𝐾)‘𝑊)) ↾_s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}) ∈ LVec)
17	11, 14, 16	syl2anc 590	. 2 ⊢ (𝜑 → ((LDual‘((DVecH‘𝐾)‘𝑊)) ↾_s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}) ∈ LVec)
18	9, 17	eqeltrd 2839	1 ⊢ (𝜑 → 𝐶 ∈ LVec)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1547 ∈ wcel 2119 {crab 3391 ‘cfv 6486 (class class class)co 7357 ↾_s cress 17192 LSubSpclss 20922 LVecclvec 21093 LFnlclfn 39558 LKerclk 39586 LDualcld 39624 HLchlt 39851 LHypclh 40485 DVecHcdvh 41579 ocHcoch 41848 LCDualclcd 42087

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5200 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-riotaBAD 39454

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-tp 4561 df-op 4563 df-uni 4840 df-int 4879 df-iun 4924 df-iin 4925 df-br 5074 df-opab 5136 df-mpt 5155 df-tr 5181 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7621 df-om 7808 df-1st 7932 df-2nd 7933 df-tpos 8167 df-undef 8214 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-map 8766 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-nn 12167 df-2 12236 df-3 12237 df-4 12238 df-5 12239 df-6 12240 df-n0 12430 df-z 12517 df-uz 12781 df-fz 13454 df-struct 17109 df-sets 17126 df-slot 17144 df-ndx 17156 df-base 17172 df-ress 17193 df-plusg 17225 df-mulr 17226 df-sca 17228 df-vsca 17229 df-0g 17396 df-mre 17540 df-mrc 17541 df-acs 17543 df-proset 18252 df-poset 18271 df-plt 18286 df-lub 18302 df-glb 18303 df-join 18304 df-meet 18305 df-p0 18381 df-p1 18382 df-lat 18390 df-clat 18457 df-mgm 18600 df-sgrp 18679 df-mnd 18695 df-submnd 18744 df-grp 18904 df-minusg 18905 df-sbg 18906 df-subg 19091 df-cntz 19284 df-oppg 19313 df-lsm 19603 df-cmn 19749 df-abl 19750 df-mgp 20114 df-rng 20126 df-ur 20155 df-ring 20208 df-oppr 20309 df-dvdsr 20329 df-unit 20330 df-invr 20360 df-dvr 20373 df-nzr 20486 df-rlreg 20667 df-domn 20668 df-drng 20704 df-lmod 20853 df-lss 20923 df-lsp 20963 df-lvec 21094 df-lsatoms 39477 df-lshyp 39478 df-lcv 39520 df-lfl 39559 df-lkr 39587 df-ldual 39625 df-oposet 39677 df-ol 39679 df-oml 39680 df-covers 39767 df-ats 39768 df-atl 39799 df-cvlat 39823 df-hlat 39852 df-llines 39999 df-lplanes 40000 df-lvols 40001 df-lines 40002 df-psubsp 40004 df-pmap 40005 df-padd 40297 df-lhyp 40489 df-laut 40490 df-ldil 40605 df-ltrn 40606 df-trl 40660 df-tgrp 41244 df-tendo 41256 df-edring 41258 df-dveca 41504 df-disoa 41530 df-dvech 41580 df-dib 41640 df-dic 41674 df-dih 41730 df-doch 41849 df-djh 41896 df-lcdual 42088

This theorem is referenced by: lcdlmod 42093 mapdcnvatN 42167 mapdat 42168 mapdpglem18 42190 mapdpglem20 42192 mapdpglem22 42194 mapdpglem26 42199 mapdpglem27 42200 mapdpglem30 42203 mapdheq4lem 42232 mapdh6lem1N 42234 mapdh6lem2N 42235 hdmap1l6lem1 42308 hdmap1l6lem2 42309 hdmaprnlem3N 42351 hdmaprnlem3uN 42352 hdmaprnlem9N 42358 hdmap14lem2a 42368 hdmap14lem2N 42370 hdmap14lem3 42371 hdmap14lem6 42374 hdmap14lem9 42377 hgmapval0 42393 hgmapval1 42394 hgmapadd 42395 hgmapmul 42396 hgmaprnlem1N 42397

W3C validator