Metamath Proof Explorer

Theorem mapdffval

Description: Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015)

Ref Expression
Hypothesis mapdval.h 
|- H = ( LHyp ` K )
Assertion mapdffval 
|- ( K e. X -> ( mapd ` K ) = ( w e. H |-> ( s e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) |-> { f e. ( LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) /\ ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) } ) ) )

Proof

Step Hyp Ref Expression
1 mapdval.h 
 |-  H = ( LHyp ` K )
2 elex 
 |-  ( K e. X -> K e. _V )
3 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
4 3 1 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
5 fveq2 
 |-  ( k = K -> ( DVecH ` k ) = ( DVecH ` K ) )
6 5 fveq1d 
 |-  ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) )
7 6 fveq2d 
 |-  ( k = K -> ( LSubSp ` ( ( DVecH ` k ) ` w ) ) = ( LSubSp ` ( ( DVecH ` K ) ` w ) ) )
8 6 fveq2d 
 |-  ( k = K -> ( LFnl ` ( ( DVecH ` k ) ` w ) ) = ( LFnl ` ( ( DVecH ` K ) ` w ) ) )
9 fveq2 
 |-  ( k = K -> ( ocH ` k ) = ( ocH ` K ) )
10 9 fveq1d 
 |-  ( k = K -> ( ( ocH ` k ) ` w ) = ( ( ocH ` K ) ` w ) )
11 6 fveq2d 
 |-  ( k = K -> ( LKer ` ( ( DVecH ` k ) ` w ) ) = ( LKer ` ( ( DVecH ` K ) ` w ) ) )
12 11 fveq1d 
 |-  ( k = K -> ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) )
13 10 12 fveq12d 
 |-  ( k = K -> ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) = ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) )
14 10 13 fveq12d 
 |-  ( k = K -> ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) )
15 14 12 eqeq12d 
 |-  ( k = K -> ( ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) <-> ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) )
16 13 sseq1d 
 |-  ( k = K -> ( ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) C_ s <-> ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) )
17 15 16 anbi12d 
 |-  ( k = K -> ( ( ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) /\ ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) C_ s ) <-> ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) /\ ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) ) )
18 8 17 rabeqbidv 
 |-  ( k = K -> { f e. ( LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) /\ ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) C_ s ) } = { f e. ( LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) /\ ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) } )
19 7 18 mpteq12dv 
 |-  ( k = K -> ( s e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) |-> { f e. ( LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) /\ ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) C_ s ) } ) = ( s e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) |-> { f e. ( LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) /\ ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) } ) )
20 4 19 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( s e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) |-> { f e. ( LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) /\ ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) C_ s ) } ) ) = ( w e. H |-> ( s e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) |-> { f e. ( LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) /\ ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) } ) ) )
21 df-mapd 
 |-  mapd = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( s e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) |-> { f e. ( LFnl ` ( ( DVecH ` k ) ` w ) ) | ( ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) /\ ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) C_ s ) } ) ) )
22 20 21 1 mptfvmpt 
 |-  ( K e. _V -> ( mapd ` K ) = ( w e. H |-> ( s e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) |-> { f e. ( LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) /\ ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) } ) ) )
23 2 22 syl 
 |-  ( K e. X -> ( mapd ` K ) = ( w e. H |-> ( s e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) |-> { f e. ( LFnl ` ( ( DVecH ` K ) ` w ) ) | ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) /\ ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) } ) ) )