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

Definition df-lcdual 37397
 Description: Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 37459. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 37435 using (Base‘((LCDual‘𝐾)‘𝑊)). (Contributed by NM, 13-Mar-2015.)
Assertion
Ref Expression
df-lcdual LCDual = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})))
Distinct variable group:   𝑓,𝑘,𝑤

Detailed syntax breakdown of Definition df-lcdual
StepHypRef Expression
1 clcd 37396 . 2 class LCDual
2 vk . . 3 setvar 𝑘
3 cvv 3351 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1630 . . . . 5 class 𝑘
6 clh 35792 . . . . 5 class LHyp
75, 6cfv 6031 . . . 4 class (LHyp‘𝑘)
84cv 1630 . . . . . . 7 class 𝑤
9 cdvh 36888 . . . . . . . 8 class DVecH
105, 9cfv 6031 . . . . . . 7 class (DVecH‘𝑘)
118, 10cfv 6031 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
12 cld 34932 . . . . . 6 class LDual
1311, 12cfv 6031 . . . . 5 class (LDual‘((DVecH‘𝑘)‘𝑤))
14 vf . . . . . . . . . . 11 setvar 𝑓
1514cv 1630 . . . . . . . . . 10 class 𝑓
16 clk 34894 . . . . . . . . . . 11 class LKer
1711, 16cfv 6031 . . . . . . . . . 10 class (LKer‘((DVecH‘𝑘)‘𝑤))
1815, 17cfv 6031 . . . . . . . . 9 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
19 coch 37157 . . . . . . . . . . 11 class ocH
205, 19cfv 6031 . . . . . . . . . 10 class (ocH‘𝑘)
218, 20cfv 6031 . . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
2218, 21cfv 6031 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
2322, 21cfv 6031 . . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
2423, 18wceq 1631 . . . . . 6 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
25 clfn 34866 . . . . . . 7 class LFnl
2611, 25cfv 6031 . . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
2724, 14, 26crab 3065 . . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}
28 cress 16065 . . . . 5 class s
2913, 27, 28co 6793 . . . 4 class ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})
304, 7, 29cmpt 4863 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}))
312, 3, 30cmpt 4863 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})))
321, 31wceq 1631 1 wff LCDual = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})))
 Colors of variables: wff setvar class This definition is referenced by:  lcdfval  37398
 Copyright terms: Public domain W3C validator