Metamath Proof Explorer

Theorem lcdval

Description: Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

Ref Expression
Hypotheses lcdval.h 
|- H = ( LHyp ` K )
lcdval.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcdval.c 
|- C = ( ( LCDual ` K ) ` W )
lcdval.u 
|- U = ( ( DVecH ` K ) ` W )
lcdval.f 
|- F = ( LFnl ` U )
lcdval.l 
|- L = ( LKer ` U )
lcdval.d 
|- D = ( LDual ` U )
lcdval.k 
|- ( ph -> ( K e. X /\ W e. H ) )
Assertion lcdval 
|- ( ph -> C = ( D |`s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) )

Proof

Step Hyp Ref Expression
1 lcdval.h 
 |-  H = ( LHyp ` K )
2 lcdval.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcdval.c 
 |-  C = ( ( LCDual ` K ) ` W )
4 lcdval.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 lcdval.f 
 |-  F = ( LFnl ` U )
6 lcdval.l 
 |-  L = ( LKer ` U )
7 lcdval.d 
 |-  D = ( LDual ` U )
8 lcdval.k 
 |-  ( ph -> ( K e. X /\ W e. H ) )
9 1 lcdfval 
 |-  ( K e. X -> ( LCDual ` K ) = ( w e. H |-> ( ( 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 ) } ) ) )
10 9 fveq1d 
 |-  ( K e. X -> ( ( LCDual ` K ) ` W ) = ( ( w e. H |-> ( ( 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 ) } ) ) ` W ) )
11 3 10 eqtrid 
 |-  ( K e. X -> C = ( ( w e. H |-> ( ( 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 ) } ) ) ` W ) )
12 fveq2 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = ( ( DVecH ` K ) ` W ) )
13 12 4 eqtr4di 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = U )
14 13 fveq2d 
 |-  ( w = W -> ( LDual ` ( ( DVecH ` K ) ` w ) ) = ( LDual ` U ) )
15 14 7 eqtr4di 
 |-  ( w = W -> ( LDual ` ( ( DVecH ` K ) ` w ) ) = D )
16 13 fveq2d 
 |-  ( w = W -> ( LFnl ` ( ( DVecH ` K ) ` w ) ) = ( LFnl ` U ) )
17 16 5 eqtr4di 
 |-  ( w = W -> ( LFnl ` ( ( DVecH ` K ) ` w ) ) = F )
18 fveq2 
 |-  ( w = W -> ( ( ocH ` K ) ` w ) = ( ( ocH ` K ) ` W ) )
19 18 2 eqtr4di 
 |-  ( w = W -> ( ( ocH ` K ) ` w ) = ._|_ )
20 13 fveq2d 
 |-  ( w = W -> ( LKer ` ( ( DVecH ` K ) ` w ) ) = ( LKer ` U ) )
21 20 6 eqtr4di 
 |-  ( w = W -> ( LKer ` ( ( DVecH ` K ) ` w ) ) = L )
22 21 fveq1d 
 |-  ( w = W -> ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) = ( L ` f ) )
23 19 22 fveq12d 
 |-  ( w = W -> ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) = ( ._|_ ` ( L ` f ) ) )
24 19 23 fveq12d 
 |-  ( w = W -> ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) )
25 24 22 eqeq12d 
 |-  ( w = W -> ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) <-> ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) ) )
26 17 25 rabeqbidv 
 |-  ( w = W -> { f e. ( LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) } = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
27 15 26 oveq12d 
 |-  ( w = W -> ( ( 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 ) } ) = ( D |`s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) )
28 eqid 
 |-  ( w e. H |-> ( ( 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 ) } ) ) = ( w e. H |-> ( ( 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 ovex 
 |-  ( D |`s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) e. _V
30 27 28 29 fvmpt 
 |-  ( W e. H -> ( ( w e. H |-> ( ( 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 ) } ) ) ` W ) = ( D |`s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) )
31 11 30 sylan9eq 
 |-  ( ( K e. X /\ W e. H ) -> C = ( D |`s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) )
32 8 31 syl 
 |-  ( ph -> C = ( D |`s { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) )