Metamath Proof Explorer

Theorem mapdval4N

Description: Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is C_ C ) 2. The unneeded direction of lcfl8a has awkward E. - add another thm with only one direction of it? 3. Swap O{ v } and Lf ? (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdval4.h 
|- H = ( LHyp ` K )
mapdval4.u 
|- U = ( ( DVecH ` K ) ` W )
mapdval4.s 
|- S = ( LSubSp ` U )
mapdval4.f 
|- F = ( LFnl ` U )
mapdval4.l 
|- L = ( LKer ` U )
mapdval4.o 
|- O = ( ( ocH ` K ) ` W )
mapdval4.m 
|- M = ( ( mapd ` K ) ` W )
mapdval4.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdval4.t 
|- ( ph -> T e. S )
Assertion mapdval4N 
|- ( ph -> ( M ` T ) = { f e. F | E. v e. T ( O ` { v } ) = ( L ` f ) } )

Proof

Step Hyp Ref Expression
1 mapdval4.h 
 |-  H = ( LHyp ` K )
2 mapdval4.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 mapdval4.s 
 |-  S = ( LSubSp ` U )
4 mapdval4.f 
 |-  F = ( LFnl ` U )
5 mapdval4.l 
 |-  L = ( LKer ` U )
6 mapdval4.o 
 |-  O = ( ( ocH ` K ) ` W )
7 mapdval4.m 
 |-  M = ( ( mapd ` K ) ` W )
8 mapdval4.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 mapdval4.t 
 |-  ( ph -> T e. S )
10 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
11 eqid 
 |-  { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) } = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
12 1 2 3 10 4 5 6 7 8 9 11 mapdval2N 
 |-  ( ph -> ( M ` T ) = { f e. { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) } | E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) } )
13 11 lcfl1lem 
 |-  ( f e. { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) } <-> ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) )
14 13 anbi1i 
 |-  ( ( f e. { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) } /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) <-> ( ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) )
15 anass 
 |-  ( ( ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) <-> ( f e. F /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) )
16 14 15 bitri 
 |-  ( ( f e. { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) } /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) <-> ( f e. F /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) )
17 r19.42v 
 |-  ( E. v e. T ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) <-> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) )
18 simprr 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) -> ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) )
19 18 fveq2d 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) -> ( O ` ( O ` ( L ` f ) ) ) = ( O ` ( ( LSpan ` U ) ` { v } ) ) )
20 simprl 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) -> ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) )
21 eqid 
 |-  ( Base ` U ) = ( Base ` U )
22 8 adantr 
 |-  ( ( ph /\ f e. F ) -> ( K e. HL /\ W e. H ) )
23 22 adantr 
 |-  ( ( ( ph /\ f e. F ) /\ v e. T ) -> ( K e. HL /\ W e. H ) )
24 23 adantr 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) -> ( K e. HL /\ W e. H ) )
25 9 adantr 
 |-  ( ( ph /\ f e. F ) -> T e. S )
26 21 3 lssel 
 |-  ( ( T e. S /\ v e. T ) -> v e. ( Base ` U ) )
27 25 26 sylan 
 |-  ( ( ( ph /\ f e. F ) /\ v e. T ) -> v e. ( Base ` U ) )
28 27 snssd 
 |-  ( ( ( ph /\ f e. F ) /\ v e. T ) -> { v } C_ ( Base ` U ) )
29 28 adantr 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) -> { v } C_ ( Base ` U ) )
30 1 2 6 21 10 24 29 dochocsp 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) -> ( O ` ( ( LSpan ` U ) ` { v } ) ) = ( O ` { v } ) )
31 19 20 30 3eqtr3rd 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) -> ( O ` { v } ) = ( L ` f ) )
32 27 adantr 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> v e. ( Base ` U ) )
33 simpr 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> ( O ` { v } ) = ( L ` f ) )
34 33 eqcomd 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> ( L ` f ) = ( O ` { v } ) )
35 sneq 
 |-  ( w = v -> { w } = { v } )
36 35 fveq2d 
 |-  ( w = v -> ( O ` { w } ) = ( O ` { v } ) )
37 36 rspceeqv 
 |-  ( ( v e. ( Base ` U ) /\ ( L ` f ) = ( O ` { v } ) ) -> E. w e. ( Base ` U ) ( L ` f ) = ( O ` { w } ) )
38 32 34 37 syl2anc 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> E. w e. ( Base ` U ) ( L ` f ) = ( O ` { w } ) )
39 23 adantr 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> ( K e. HL /\ W e. H ) )
40 simpllr 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> f e. F )
41 1 6 2 21 4 5 39 40 lcfl8a 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) <-> E. w e. ( Base ` U ) ( L ` f ) = ( O ` { w } ) ) )
42 38 41 mpbird 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) )
43 1 2 6 21 10 23 27 dochocsn 
 |-  ( ( ( ph /\ f e. F ) /\ v e. T ) -> ( O ` ( O ` { v } ) ) = ( ( LSpan ` U ) ` { v } ) )
44 fveq2 
 |-  ( ( O ` { v } ) = ( L ` f ) -> ( O ` ( O ` { v } ) ) = ( O ` ( L ` f ) ) )
45 43 44 sylan9req 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> ( ( LSpan ` U ) ` { v } ) = ( O ` ( L ` f ) ) )
46 45 eqcomd 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) )
47 42 46 jca 
 |-  ( ( ( ( ph /\ f e. F ) /\ v e. T ) /\ ( O ` { v } ) = ( L ` f ) ) -> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) )
48 31 47 impbida 
 |-  ( ( ( ph /\ f e. F ) /\ v e. T ) -> ( ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) <-> ( O ` { v } ) = ( L ` f ) ) )
49 48 rexbidva 
 |-  ( ( ph /\ f e. F ) -> ( E. v e. T ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) <-> E. v e. T ( O ` { v } ) = ( L ` f ) ) )
50 17 49 bitr3id 
 |-  ( ( ph /\ f e. F ) -> ( ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) <-> E. v e. T ( O ` { v } ) = ( L ` f ) ) )
51 50 pm5.32da 
 |-  ( ph -> ( ( f e. F /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) ) <-> ( f e. F /\ E. v e. T ( O ` { v } ) = ( L ` f ) ) ) )
52 16 51 syl5bb 
 |-  ( ph -> ( ( f e. { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) } /\ E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) ) <-> ( f e. F /\ E. v e. T ( O ` { v } ) = ( L ` f ) ) ) )
53 52 rabbidva2 
 |-  ( ph -> { f e. { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) } | E. v e. T ( O ` ( L ` f ) ) = ( ( LSpan ` U ) ` { v } ) } = { f e. F | E. v e. T ( O ` { v } ) = ( L ` f ) } )
54 12 53 eqtrd 
 |-  ( ph -> ( M ` T ) = { f e. F | E. v e. T ( O ` { v } ) = ( L ` f ) } )