Metamath Proof Explorer

Theorem mapdfval

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

Ref Expression
Hypotheses mapdval.h 
|- H = ( LHyp ` K )
mapdval.u 
|- U = ( ( DVecH ` K ) ` W )
mapdval.s 
|- S = ( LSubSp ` U )
mapdval.f 
|- F = ( LFnl ` U )
mapdval.l 
|- L = ( LKer ` U )
mapdval.o 
|- O = ( ( ocH ` K ) ` W )
mapdval.m 
|- M = ( ( mapd ` K ) ` W )
Assertion mapdfval 
|- ( ( K e. X /\ W e. H ) -> M = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )

Proof

Step Hyp Ref Expression
1 mapdval.h 
 |-  H = ( LHyp ` K )
2 mapdval.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 mapdval.s 
 |-  S = ( LSubSp ` U )
4 mapdval.f 
 |-  F = ( LFnl ` U )
5 mapdval.l 
 |-  L = ( LKer ` U )
6 mapdval.o 
 |-  O = ( ( ocH ` K ) ` W )
7 mapdval.m 
 |-  M = ( ( mapd ` K ) ` W )
8 1 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 ) } ) ) )
9 8 fveq1d 
 |-  ( K e. X -> ( ( mapd ` K ) ` W ) = ( ( 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 ) } ) ) ` W ) )
10 7 9 syl5eq 
 |-  ( K e. X -> M = ( ( 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 ) } ) ) ` W ) )
11 fveq2 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = ( ( DVecH ` K ) ` W ) )
12 11 2 eqtr4di 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = U )
13 12 fveq2d 
 |-  ( w = W -> ( LSubSp ` ( ( DVecH ` K ) ` w ) ) = ( LSubSp ` U ) )
14 13 3 eqtr4di 
 |-  ( w = W -> ( LSubSp ` ( ( DVecH ` K ) ` w ) ) = S )
15 12 fveq2d 
 |-  ( w = W -> ( LFnl ` ( ( DVecH ` K ) ` w ) ) = ( LFnl ` U ) )
16 15 4 eqtr4di 
 |-  ( w = W -> ( LFnl ` ( ( DVecH ` K ) ` w ) ) = F )
17 fveq2 
 |-  ( w = W -> ( ( ocH ` K ) ` w ) = ( ( ocH ` K ) ` W ) )
18 17 6 eqtr4di 
 |-  ( w = W -> ( ( ocH ` K ) ` w ) = O )
19 12 fveq2d 
 |-  ( w = W -> ( LKer ` ( ( DVecH ` K ) ` w ) ) = ( LKer ` U ) )
20 19 5 eqtr4di 
 |-  ( w = W -> ( LKer ` ( ( DVecH ` K ) ` w ) ) = L )
21 20 fveq1d 
 |-  ( w = W -> ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) = ( L ` f ) )
22 18 21 fveq12d 
 |-  ( w = W -> ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) = ( O ` ( L ` f ) ) )
23 18 22 fveq12d 
 |-  ( w = W -> ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( O ` ( O ` ( L ` f ) ) ) )
24 23 21 eqeq12d 
 |-  ( w = W -> ( ( ( ( ocH ` K ) ` w ) ` ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) <-> ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) )
25 22 sseq1d 
 |-  ( w = W -> ( ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s <-> ( O ` ( L ` f ) ) C_ s ) )
26 24 25 anbi12d 
 |-  ( w = 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 ) <-> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) ) )
27 16 26 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 ) /\ ( ( ( ocH ` K ) ` w ) ` ( ( LKer ` ( ( DVecH ` K ) ` w ) ) ` f ) ) C_ s ) } = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } )
28 14 27 mpteq12dv 
 |-  ( w = W -> ( 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. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )
29 eqid 
 |-  ( 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 ) } ) ) = ( 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 ) } ) )
30 28 29 3 mptfvmpt 
 |-  ( W e. H -> ( ( 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 ) } ) ) ` W ) = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )
31 10 30 sylan9eq 
 |-  ( ( K e. X /\ W e. H ) -> M = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )