Definition df-lcdual 40458

Description: Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 40520. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 40496 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

Step	Hyp	Ref	Expression
1		clcd 40457	. 2 class LCDual
2		vk	. . 3 setvar 𝑘
3		cvv 3475	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1541	. . . . 5 class 𝑘
6		clh 38855	. . . . 5 class LHyp
7	5, 6	cfv 6544	. . . 4 class (LHyp‘𝑘)
8	4	cv 1541	. . . . . . 7 class 𝑤
9		cdvh 39949	. . . . . . . 8 class DVecH
10	5, 9	cfv 6544	. . . . . . 7 class (DVecH‘𝑘)
11	8, 10	cfv 6544	. . . . . 6 class ((DVecH‘𝑘)‘𝑤)
12		cld 37993	. . . . . 6 class LDual
13	11, 12	cfv 6544	. . . . 5 class (LDual‘((DVecH‘𝑘)‘𝑤))
14		vf	. . . . . . . . . . 11 setvar 𝑓
15	14	cv 1541	. . . . . . . . . 10 class 𝑓
16		clk 37955	. . . . . . . . . . 11 class LKer
17	11, 16	cfv 6544	. . . . . . . . . 10 class (LKer‘((DVecH‘𝑘)‘𝑤))
18	15, 17	cfv 6544	. . . . . . . . 9 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
19		coch 40218	. . . . . . . . . . 11 class ocH
20	5, 19	cfv 6544	. . . . . . . . . 10 class (ocH‘𝑘)
21	8, 20	cfv 6544	. . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
22	18, 21	cfv 6544	. . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
23	22, 21	cfv 6544	. . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
24	23, 18	wceq 1542	. . . . . 6 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
25		clfn 37927	. . . . . . 7 class LFnl
26	11, 25	cfv 6544	. . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
27	24, 14, 26	crab 3433	. . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}
28		cress 17173	. . . . 5 class ↾s
29	13, 27, 28	co 7409	. . . 4 class ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})
30	4, 7, 29	cmpt 5232	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}))
31	2, 3, 30	cmpt 5232	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})))
32	1, 31	wceq 1542	1 wff LCDual = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)})))

This definition is referenced by:  lcdfval  40459