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 41496

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 2734	. . 3 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
3		lcdlmod.c	. . 3 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
4		eqid 2734	. . 3 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
5		eqid 2734	. . 3 ⊢ (LFnl‘((DVecH‘𝐾)‘𝑊)) = (LFnl‘((DVecH‘𝐾)‘𝑊))
6		eqid 2734	. . 3 ⊢ (LKer‘((DVecH‘𝐾)‘𝑊)) = (LKer‘((DVecH‘𝐾)‘𝑊))
7		eqid 2734	. . 3 ⊢ (LDual‘((DVecH‘𝐾)‘𝑊)) = (LDual‘((DVecH‘𝐾)‘𝑊))
8		lcdlmod.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
9	1, 2, 3, 4, 5, 6, 7, 8	lcdval 41494	. 2 ⊢ (𝜑 → 𝐶 = ((LDual‘((DVecH‘𝐾)‘𝑊)) ↾_s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}))
10	1, 4, 8	dvhlvec 41014	. . . 4 ⊢ (𝜑 → ((DVecH‘𝐾)‘𝑊) ∈ LVec)
11	7, 10	lduallvec 39058	. . 3 ⊢ (𝜑 → (LDual‘((DVecH‘𝐾)‘𝑊)) ∈ LVec)
12		eqid 2734	. . . 4 ⊢ (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) = (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊)))
13		eqid 2734	. . . 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 41438	. . 3 ⊢ (𝜑 → {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)} ∈ (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))))
15		eqid 2734	. . . 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 21126	. . 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 583	. 2 ⊢ (𝜑 → ((LDual‘((DVecH‘𝐾)‘𝑊)) ↾_s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}) ∈ LVec)
18	9, 17	eqeltrd 2838	1 ⊢ (𝜑 → 𝐶 ∈ LVec)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2103 {crab 3438 ‘cfv 6572 (class class class)co 7445 ↾_s cress 17282 LSubSpclss 20947 LVecclvec 21119 LFnlclfn 38961 LKerclk 38989 LDualcld 39027 HLchlt 39254 LHypclh 39889 DVecHcdvh 40983 ocHcoch 41252 LCDualclcd 41491

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-rep 5306 ax-sep 5320 ax-nul 5327 ax-pow 5386 ax-pr 5450 ax-un 7766 ax-cnex 11236 ax-resscn 11237 ax-1cn 11238 ax-icn 11239 ax-addcl 11240 ax-addrcl 11241 ax-mulcl 11242 ax-mulrcl 11243 ax-mulcom 11244 ax-addass 11245 ax-mulass 11246 ax-distr 11247 ax-i2m1 11248 ax-1ne0 11249 ax-1rid 11250 ax-rnegex 11251 ax-rrecex 11252 ax-cnre 11253 ax-pre-lttri 11254 ax-pre-lttrn 11255 ax-pre-ltadd 11256 ax-pre-mulgt0 11257 ax-riotaBAD 38857

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-rmo 3383 df-reu 3384 df-rab 3439 df-v 3484 df-sbc 3799 df-csb 3916 df-dif 3973 df-un 3975 df-in 3977 df-ss 3987 df-pss 3990 df-nul 4348 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4973 df-iun 5021 df-iin 5022 df-br 5170 df-opab 5232 df-mpt 5253 df-tr 5287 df-id 5597 df-eprel 5603 df-po 5611 df-so 5612 df-fr 5654 df-we 5656 df-xp 5705 df-rel 5706 df-cnv 5707 df-co 5708 df-dm 5709 df-rn 5710 df-res 5711 df-ima 5712 df-pred 6331 df-ord 6397 df-on 6398 df-lim 6399 df-suc 6400 df-iota 6524 df-fun 6574 df-fn 6575 df-f 6576 df-f1 6577 df-fo 6578 df-f1o 6579 df-fv 6580 df-riota 7401 df-ov 7448 df-oprab 7449 df-mpo 7450 df-of 7710 df-om 7900 df-1st 8026 df-2nd 8027 df-tpos 8263 df-undef 8310 df-frecs 8318 df-wrecs 8349 df-recs 8423 df-rdg 8462 df-1o 8518 df-2o 8519 df-er 8759 df-map 8882 df-en 9000 df-dom 9001 df-sdom 9002 df-fin 9003 df-pnf 11322 df-mnf 11323 df-xr 11324 df-ltxr 11325 df-le 11326 df-sub 11518 df-neg 11519 df-nn 12290 df-2 12352 df-3 12353 df-4 12354 df-5 12355 df-6 12356 df-n0 12550 df-z 12636 df-uz 12900 df-fz 13564 df-struct 17189 df-sets 17206 df-slot 17224 df-ndx 17236 df-base 17254 df-ress 17283 df-plusg 17319 df-mulr 17320 df-sca 17322 df-vsca 17323 df-0g 17496 df-mre 17639 df-mrc 17640 df-acs 17642 df-proset 18360 df-poset 18378 df-plt 18395 df-lub 18411 df-glb 18412 df-join 18413 df-meet 18414 df-p0 18490 df-p1 18491 df-lat 18497 df-clat 18564 df-mgm 18673 df-sgrp 18752 df-mnd 18768 df-submnd 18814 df-grp 18971 df-minusg 18972 df-sbg 18973 df-subg 19158 df-cntz 19352 df-oppg 19381 df-lsm 19673 df-cmn 19819 df-abl 19820 df-mgp 20157 df-rng 20175 df-ur 20204 df-ring 20257 df-oppr 20355 df-dvdsr 20378 df-unit 20379 df-invr 20409 df-dvr 20422 df-nzr 20534 df-rlreg 20711 df-domn 20712 df-drng 20748 df-lmod 20877 df-lss 20948 df-lsp 20988 df-lvec 21120 df-lsatoms 38880 df-lshyp 38881 df-lcv 38923 df-lfl 38962 df-lkr 38990 df-ldual 39028 df-oposet 39080 df-ol 39082 df-oml 39083 df-covers 39170 df-ats 39171 df-atl 39202 df-cvlat 39226 df-hlat 39255 df-llines 39403 df-lplanes 39404 df-lvols 39405 df-lines 39406 df-psubsp 39408 df-pmap 39409 df-padd 39701 df-lhyp 39893 df-laut 39894 df-ldil 40009 df-ltrn 40010 df-trl 40064 df-tgrp 40648 df-tendo 40660 df-edring 40662 df-dveca 40908 df-disoa 40934 df-dvech 40984 df-dib 41044 df-dic 41078 df-dih 41134 df-doch 41253 df-djh 41300 df-lcdual 41492

This theorem is referenced by: lcdlmod 41497 mapdcnvatN 41571 mapdat 41572 mapdpglem18 41594 mapdpglem20 41596 mapdpglem22 41598 mapdpglem26 41603 mapdpglem27 41604 mapdpglem30 41607 mapdheq4lem 41636 mapdh6lem1N 41638 mapdh6lem2N 41639 hdmap1l6lem1 41712 hdmap1l6lem2 41713 hdmaprnlem3N 41755 hdmaprnlem3uN 41756 hdmaprnlem9N 41762 hdmap14lem2a 41772 hdmap14lem2N 41774 hdmap14lem3 41775 hdmap14lem6 41778 hdmap14lem9 41781 hgmapval0 41797 hgmapval1 41798 hgmapadd 41799 hgmapmul 41800 hgmaprnlem1N 41801

W3C validator