Definition df-lcdual 36876

Description: Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 36938. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 36914 using ( Base ` ( (LCDual ` K ) ` W ) ). (Contributed by NM, 13-Mar-2015.)

Assertion

Ref	Expression
df-lcdual	|- LCDual = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( (LDual ` ( ( DVecH ` k ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) } ) ) )

Distinct variable group:   f, k, w

Detailed syntax breakdown of Definition df-lcdual

Step	Hyp	Ref	Expression
1		clcd 36875	. 2 class LCDual
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1482	. . . . 5 class k
6		clh 35270	. . . . 5 class LHyp
7	5, 6	cfv 5888	. . . 4 class ( LHyp ` k )
8	4	cv 1482	. . . . . . 7 class w
9		cdvh 36367	. . . . . . . 8 class DVecH
10	5, 9	cfv 5888	. . . . . . 7 class ( DVecH ` k )
11	8, 10	cfv 5888	. . . . . 6 class ( ( DVecH ` k ) ` w )
12		cld 34410	. . . . . 6 class LDual
13	11, 12	cfv 5888	. . . . 5 class (LDual ` ( ( DVecH ` k ) ` w ) )
14		vf	. . . . . . . . . . 11 setvar f
15	14	cv 1482	. . . . . . . . . 10 class f
16		clk 34372	. . . . . . . . . . 11 class LKer
17	11, 16	cfv 5888	. . . . . . . . . 10 class (LKer ` ( ( DVecH ` k ) ` w ) )
18	15, 17	cfv 5888	. . . . . . . . 9 class ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f )
19		coch 36636	. . . . . . . . . . 11 class ocH
20	5, 19	cfv 5888	. . . . . . . . . 10 class ( ocH ` k )
21	8, 20	cfv 5888	. . . . . . . . 9 class ( ( ocH ` k ) ` w )
22	18, 21	cfv 5888	. . . . . . . 8 class ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) )
23	22, 21	cfv 5888	. . . . . . 7 class ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) )
24	23, 18	wceq 1483	. . . . . 6 wff ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f )
25		clfn 34344	. . . . . . 7 class LFnl
26	11, 25	cfv 5888	. . . . . 6 class (LFnl ` ( ( DVecH ` k ) ` w ) )
27	24, 14, 26	crab 2916	. . . . 5 class { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) }
28		cress 15858	. . . . 5 class ↾s
29	13, 27, 28	co 6650	. . . 4 class ( (LDual ` ( ( DVecH ` k ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) } )
30	4, 7, 29	cmpt 4729	. . 3 class ( w e. ( LHyp ` k ) |-> ( (LDual ` ( ( DVecH ` k ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) } ) )
31	2, 3, 30	cmpt 4729	. 2 class ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( (LDual ` ( ( DVecH ` k ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) } ) ) )
32	1, 31	wceq 1483	1 wff LCDual = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( (LDual ` ( ( DVecH ` k ) ` w ) ) ↾s { f e. (LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( (LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) } ) ) )

This definition is referenced by:  lcdfval  36877