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 35690
Description: Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 35752. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 35728 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 35689 . 2 class LCDual
2 vk . . 3 setvar 𝑘
3 cvv 3172 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1473 . . . . 5 class 𝑘
6 clh 34084 . . . . 5 class LHyp
75, 6cfv 5790 . . . 4 class (LHyp‘𝑘)
84cv 1473 . . . . . . 7 class 𝑤
9 cdvh 35181 . . . . . . . 8 class DVecH
105, 9cfv 5790 . . . . . . 7 class (DVecH‘𝑘)
118, 10cfv 5790 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
12 cld 33224 . . . . . 6 class LDual
1311, 12cfv 5790 . . . . 5 class (LDual‘((DVecH‘𝑘)‘𝑤))
14 vf . . . . . . . . . . 11 setvar 𝑓
1514cv 1473 . . . . . . . . . 10 class 𝑓
16 clk 33186 . . . . . . . . . . 11 class LKer
1711, 16cfv 5790 . . . . . . . . . 10 class (LKer‘((DVecH‘𝑘)‘𝑤))
1815, 17cfv 5790 . . . . . . . . 9 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
19 coch 35450 . . . . . . . . . . 11 class ocH
205, 19cfv 5790 . . . . . . . . . 10 class (ocH‘𝑘)
218, 20cfv 5790 . . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
2218, 21cfv 5790 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
2322, 21cfv 5790 . . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
2423, 18wceq 1474 . . . . . 6 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
25 clfn 33158 . . . . . . 7 class LFnl
2611, 25cfv 5790 . . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
2724, 14, 26crab 2899 . . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}
28 cress 15642 . . . . 5 class s
2913, 27, 28co 6527 . . . 4 class ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})
304, 7, 29cmpt 4637 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}))
312, 3, 30cmpt 4637 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})))
321, 31wceq 1474 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  35691
  Copyright terms: Public domain W3C validator