Users' Mathboxes 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 35894
Description: Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 35956. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 35932 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 35893 . 2 class LCDual
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1474 . . . . 5 class 𝑘
6 clh 34288 . . . . 5 class LHyp
75, 6cfv 5804 . . . 4 class (LHyp‘𝑘)
84cv 1474 . . . . . . 7 class 𝑤
9 cdvh 35385 . . . . . . . 8 class DVecH
105, 9cfv 5804 . . . . . . 7 class (DVecH‘𝑘)
118, 10cfv 5804 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
12 cld 33428 . . . . . 6 class LDual
1311, 12cfv 5804 . . . . 5 class (LDual‘((DVecH‘𝑘)‘𝑤))
14 vf . . . . . . . . . . 11 setvar 𝑓
1514cv 1474 . . . . . . . . . 10 class 𝑓
16 clk 33390 . . . . . . . . . . 11 class LKer
1711, 16cfv 5804 . . . . . . . . . 10 class (LKer‘((DVecH‘𝑘)‘𝑤))
1815, 17cfv 5804 . . . . . . . . 9 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
19 coch 35654 . . . . . . . . . . 11 class ocH
205, 19cfv 5804 . . . . . . . . . 10 class (ocH‘𝑘)
218, 20cfv 5804 . . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
2218, 21cfv 5804 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
2322, 21cfv 5804 . . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
2423, 18wceq 1475 . . . . . 6 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
25 clfn 33362 . . . . . . 7 class LFnl
2611, 25cfv 5804 . . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
2724, 14, 26crab 2900 . . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}
28 cress 15696 . . . . 5 class s
2913, 27, 28co 6549 . . . 4 class ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})
304, 7, 29cmpt 4643 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}))
312, 3, 30cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})))
321, 31wceq 1475 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  35895
  Copyright terms: Public domain W3C validator