Metamath Proof Explorer

Theorem mapdval2N

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mapdval2.h 
 |-  H = ( LHyp ` K )
2 mapdval2.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 mapdval2.s 
 |-  S = ( LSubSp ` U )
4 mapdval2.n 
 |-  N = ( LSpan ` U )
5 mapdval2.f 
 |-  F = ( LFnl ` U )
6 mapdval2.l 
 |-  L = ( LKer ` U )
7 mapdval2.o 
 |-  O = ( ( ocH ` K ) ` W )
8 mapdval2.m 
 |-  M = ( ( mapd ` K ) ` W )
9 mapdval2.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 mapdval2.t 
 |-  ( ph -> T e. S )
11 mapdval2.c 
 |-  C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
12 1 2 3 5 6 7 8 9 10 11 mapdvalc 
 |-  ( ph -> ( M ` T ) = { f e. C | ( O ` ( L ` f ) ) C_ T } )
13 1 2 9 dvhlmod 
 |-  ( ph -> U e. LMod )
14 13 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) -> U e. LMod )
15 simplr 
 |-  ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) -> ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) )
16 eqid 
 |-  ( Base ` U ) = ( Base ` U )
17 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
18 16 4 17 islsati 
 |-  ( ( U e. LMod /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) -> E. v e. ( Base ` U ) ( O ` ( L ` f ) ) = ( N ` { v } ) )
19 14 15 18 syl2anc 
 |-  ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) -> E. v e. ( Base ` U ) ( O ` ( L ` f ) ) = ( N ` { v } ) )
20 simprr 
 |-  ( ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) /\ ( v e. ( Base ` U ) /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) ) -> ( O ` ( L ` f ) ) = ( N ` { v } ) )
21 simplr 
 |-  ( ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) /\ ( v e. ( Base ` U ) /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) ) -> ( O ` ( L ` f ) ) C_ T )
22 20 21 eqsstrrd 
 |-  ( ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) /\ ( v e. ( Base ` U ) /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) ) -> ( N ` { v } ) C_ T )
23 13 adantr 
 |-  ( ( ph /\ f e. C ) -> U e. LMod )
24 23 ad3antrrr 
 |-  ( ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) /\ ( v e. ( Base ` U ) /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) ) -> U e. LMod )
25 10 adantr 
 |-  ( ( ph /\ f e. C ) -> T e. S )
26 25 ad3antrrr 
 |-  ( ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) /\ ( v e. ( Base ` U ) /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) ) -> T e. S )
27 simprl 
 |-  ( ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) /\ ( v e. ( Base ` U ) /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) ) -> v e. ( Base ` U ) )
28 16 3 4 24 26 27 ellspsn5b 
 |-  ( ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) /\ ( v e. ( Base ` U ) /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) ) -> ( v e. T <-> ( N ` { v } ) C_ T ) )
29 22 28 mpbird 
 |-  ( ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) /\ ( v e. ( Base ` U ) /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) ) -> v e. T )
30 19 29 20 reximssdv 
 |-  ( ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) /\ ( O ` ( L ` f ) ) C_ T ) -> E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) )
31 30 ex 
 |-  ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) ) -> ( ( O ` ( L ` f ) ) C_ T -> E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) ) )
32 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
33 32 3 lss0cl 
 |-  ( ( U e. LMod /\ T e. S ) -> ( 0g ` U ) e. T )
34 13 10 33 syl2anc 
 |-  ( ph -> ( 0g ` U ) e. T )
35 34 adantr 
 |-  ( ( ph /\ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) -> ( 0g ` U ) e. T )
36 simpr 
 |-  ( ( ph /\ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) -> ( O ` ( L ` f ) ) = { ( 0g ` U ) } )
37 13 adantr 
 |-  ( ( ph /\ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) -> U e. LMod )
38 32 4 lspsn0 
 |-  ( U e. LMod -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
39 37 38 syl 
 |-  ( ( ph /\ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
40 36 39 eqtr4d 
 |-  ( ( ph /\ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) -> ( O ` ( L ` f ) ) = ( N ` { ( 0g ` U ) } ) )
41 sneq 
 |-  ( v = ( 0g ` U ) -> { v } = { ( 0g ` U ) } )
42 41 fveq2d 
 |-  ( v = ( 0g ` U ) -> ( N ` { v } ) = ( N ` { ( 0g ` U ) } ) )
43 42 rspceeqv 
 |-  ( ( ( 0g ` U ) e. T /\ ( O ` ( L ` f ) ) = ( N ` { ( 0g ` U ) } ) ) -> E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) )
44 35 40 43 syl2anc 
 |-  ( ( ph /\ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) -> E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) )
45 44 adantlr 
 |-  ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) -> E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) )
46 45 a1d 
 |-  ( ( ( ph /\ f e. C ) /\ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) -> ( ( O ` ( L ` f ) ) C_ T -> E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) ) )
47 9 adantr 
 |-  ( ( ph /\ f e. C ) -> ( K e. HL /\ W e. H ) )
48 11 lcfl1lem 
 |-  ( f e. C <-> ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) )
49 48 simplbi 
 |-  ( f e. C -> f e. F )
50 49 adantl 
 |-  ( ( ph /\ f e. C ) -> f e. F )
51 1 7 2 32 17 5 6 47 50 dochsat0 
 |-  ( ( ph /\ f e. C ) -> ( ( O ` ( L ` f ) ) e. ( LSAtoms ` U ) \/ ( O ` ( L ` f ) ) = { ( 0g ` U ) } ) )
52 31 46 51 mpjaodan 
 |-  ( ( ph /\ f e. C ) -> ( ( O ` ( L ` f ) ) C_ T -> E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) ) )
53 simp3 
 |-  ( ( ( ph /\ f e. C ) /\ v e. T /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) -> ( O ` ( L ` f ) ) = ( N ` { v } ) )
54 23 3ad2ant1 
 |-  ( ( ( ph /\ f e. C ) /\ v e. T /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) -> U e. LMod )
55 25 3ad2ant1 
 |-  ( ( ( ph /\ f e. C ) /\ v e. T /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) -> T e. S )
56 simp2 
 |-  ( ( ( ph /\ f e. C ) /\ v e. T /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) -> v e. T )
57 3 4 54 55 56 ellspsn5 
 |-  ( ( ( ph /\ f e. C ) /\ v e. T /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) -> ( N ` { v } ) C_ T )
58 53 57 eqsstrd 
 |-  ( ( ( ph /\ f e. C ) /\ v e. T /\ ( O ` ( L ` f ) ) = ( N ` { v } ) ) -> ( O ` ( L ` f ) ) C_ T )
59 58 rexlimdv3a 
 |-  ( ( ph /\ f e. C ) -> ( E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) -> ( O ` ( L ` f ) ) C_ T ) )
60 52 59 impbid 
 |-  ( ( ph /\ f e. C ) -> ( ( O ` ( L ` f ) ) C_ T <-> E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) ) )
61 60 rabbidva 
 |-  ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ T } = { f e. C | E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) } )
62 12 61 eqtrd 
 |-  ( ph -> ( M ` T ) = { f e. C | E. v e. T ( O ` ( L ` f ) ) = ( N ` { v } ) } )