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 39338
Description: Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 39400. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 39376 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 39337 . 2 class LCDual
2 vk . . 3 setvar 𝑘
3 cvv 3408 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1542 . . . . 5 class 𝑘
6 clh 37735 . . . . 5 class LHyp
75, 6cfv 6380 . . . 4 class (LHyp‘𝑘)
84cv 1542 . . . . . . 7 class 𝑤
9 cdvh 38829 . . . . . . . 8 class DVecH
105, 9cfv 6380 . . . . . . 7 class (DVecH‘𝑘)
118, 10cfv 6380 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
12 cld 36874 . . . . . 6 class LDual
1311, 12cfv 6380 . . . . 5 class (LDual‘((DVecH‘𝑘)‘𝑤))
14 vf . . . . . . . . . . 11 setvar 𝑓
1514cv 1542 . . . . . . . . . 10 class 𝑓
16 clk 36836 . . . . . . . . . . 11 class LKer
1711, 16cfv 6380 . . . . . . . . . 10 class (LKer‘((DVecH‘𝑘)‘𝑤))
1815, 17cfv 6380 . . . . . . . . 9 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
19 coch 39098 . . . . . . . . . . 11 class ocH
205, 19cfv 6380 . . . . . . . . . 10 class (ocH‘𝑘)
218, 20cfv 6380 . . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
2218, 21cfv 6380 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
2322, 21cfv 6380 . . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
2423, 18wceq 1543 . . . . . 6 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
25 clfn 36808 . . . . . . 7 class LFnl
2611, 25cfv 6380 . . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
2724, 14, 26crab 3065 . . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}
28 cress 16784 . . . . 5 class s
2913, 27, 28co 7213 . . . 4 class ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})
304, 7, 29cmpt 5135 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}))
312, 3, 30cmpt 5135 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})))
321, 31wceq 1543 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  39339
  Copyright terms: Public domain W3C validator