Metamath Proof Explorer

Definition df-lcdual

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

Ref Expression
Assertion 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 ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcd 
 |-  LCDual
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 cld 
 |-  LDual
8 cdvh 
 |-  DVecH
9 5 8 cfv 
 |-  ( DVecH ` k )
10 3 cv 
 |-  w
11 10 9 cfv 
 |-  ( ( DVecH ` k ) ` w )
12 11 7 cfv 
 |-  ( LDual ` ( ( DVecH ` k ) ` w ) )
13 cress 
 |-  |`s
14 vf 
 |-  f
15 clfn 
 |-  LFnl
16 11 15 cfv 
 |-  ( LFnl ` ( ( DVecH ` k ) ` w ) )
17 coch 
 |-  ocH
18 5 17 cfv 
 |-  ( ocH ` k )
19 10 18 cfv 
 |-  ( ( ocH ` k ) ` w )
20 clk 
 |-  LKer
21 11 20 cfv 
 |-  ( LKer ` ( ( DVecH ` k ) ` w ) )
22 14 cv 
 |-  f
23 22 21 cfv 
 |-  ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f )
24 23 19 cfv 
 |-  ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) )
25 24 19 cfv 
 |-  ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) )
26 25 23 wceq 
 |-  ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f )
27 26 14 16 crab 
 |-  { f e. ( LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) }
28 12 27 13 co 
 |-  ( ( 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 ) } )
29 3 6 28 cmpt 
 |-  ( 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 ) } ) )
30 1 2 29 cmpt 
 |-  ( 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 ) } ) ) )
31 0 30 wceq 
 |-  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 ) } ) ) )