Metamath Proof Explorer

Theorem mapd1o

Description: The map defined by df-mapd is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows M satisfies part of the definition of projectivity of Baer p. 40. TODO: change theorems leading to this ( lcfr , mapdrval , lclkrs , lclkr ,...) to use T i^i ~P C ? TODO: maybe get rid of $d's for g versus K U W ; propagate to mapdrn and any others. (Contributed by NM, 12-Mar-2015)

Ref Expression
Hypotheses mapd1o.h 
|- H = ( LHyp ` K )
mapd1o.o 
|- O = ( ( ocH ` K ) ` W )
mapd1o.m 
|- M = ( ( mapd ` K ) ` W )
mapd1o.u 
|- U = ( ( DVecH ` K ) ` W )
mapd1o.s 
|- S = ( LSubSp ` U )
mapd1o.f 
|- F = ( LFnl ` U )
mapd1o.l 
|- L = ( LKer ` U )
mapd1o.d 
|- D = ( LDual ` U )
mapd1o.t 
|- T = ( LSubSp ` D )
mapd1o.c 
|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
mapd1o.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion mapd1o 
|- ( ph -> M : S -1-1-onto-> ( T i^i ~P C ) )

Proof

Step Hyp Ref Expression
1 mapd1o.h 
 |-  H = ( LHyp ` K )
2 mapd1o.o 
 |-  O = ( ( ocH ` K ) ` W )
3 mapd1o.m 
 |-  M = ( ( mapd ` K ) ` W )
4 mapd1o.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 mapd1o.s 
 |-  S = ( LSubSp ` U )
6 mapd1o.f 
 |-  F = ( LFnl ` U )
7 mapd1o.l 
 |-  L = ( LKer ` U )
8 mapd1o.d 
 |-  D = ( LDual ` U )
9 mapd1o.t 
 |-  T = ( LSubSp ` D )
10 mapd1o.c 
 |-  C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
11 mapd1o.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 6 fvexi 
 |-  F e. _V
13 12 rabex 
 |-  { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ t ) } e. _V
14 eqid 
 |-  ( t e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ t ) } ) = ( t e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ t ) } )
15 13 14 fnmpti 
 |-  ( t e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ t ) } ) Fn S
16 1 4 5 6 7 2 3 mapdfval 
 |-  ( ( K e. HL /\ W e. H ) -> M = ( t e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ t ) } ) )
17 11 16 syl 
 |-  ( ph -> M = ( t e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ t ) } ) )
18 17 fneq1d 
 |-  ( ph -> ( M Fn S <-> ( t e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ t ) } ) Fn S ) )
19 15 18 mpbiri 
 |-  ( ph -> M Fn S )
20 12 rabex 
 |-  { g e. F | ( ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) /\ ( O ` ( L ` g ) ) C_ t ) } e. _V
21 eqid 
 |-  ( t e. S |-> { g e. F | ( ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) /\ ( O ` ( L ` g ) ) C_ t ) } ) = ( t e. S |-> { g e. F | ( ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) /\ ( O ` ( L ` g ) ) C_ t ) } )
22 20 21 fnmpti 
 |-  ( t e. S |-> { g e. F | ( ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) /\ ( O ` ( L ` g ) ) C_ t ) } ) Fn S
23 1 4 5 6 7 2 3 mapdfval 
 |-  ( ( K e. HL /\ W e. H ) -> M = ( t e. S |-> { g e. F | ( ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) /\ ( O ` ( L ` g ) ) C_ t ) } ) )
24 11 23 syl 
 |-  ( ph -> M = ( t e. S |-> { g e. F | ( ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) /\ ( O ` ( L ` g ) ) C_ t ) } ) )
25 24 fneq1d 
 |-  ( ph -> ( M Fn S <-> ( t e. S |-> { g e. F | ( ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) /\ ( O ` ( L ` g ) ) C_ t ) } ) Fn S ) )
26 22 25 mpbiri 
 |-  ( ph -> M Fn S )
27 fvelrnb 
 |-  ( M Fn S -> ( t e. ran M <-> E. c e. S ( M ` c ) = t ) )
28 26 27 syl 
 |-  ( ph -> ( t e. ran M <-> E. c e. S ( M ` c ) = t ) )
29 11 adantr 
 |-  ( ( ph /\ c e. S ) -> ( K e. HL /\ W e. H ) )
30 simpr 
 |-  ( ( ph /\ c e. S ) -> c e. S )
31 1 4 5 6 7 2 3 29 30 mapdval 
 |-  ( ( ph /\ c e. S ) -> ( M ` c ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } )
32 eqid 
 |-  { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) }
33 1 2 4 5 6 7 8 9 10 32 29 30 lclkrs2 
 |-  ( ( ph /\ c e. S ) -> ( { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. T /\ { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } C_ C ) )
34 elin 
 |-  ( { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. ( T i^i ~P C ) <-> ( { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. T /\ { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. ~P C ) )
35 12 rabex 
 |-  { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. _V
36 35 elpw 
 |-  ( { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. ~P C <-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } C_ C )
37 36 anbi2i 
 |-  ( ( { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. T /\ { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. ~P C ) <-> ( { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. T /\ { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } C_ C ) )
38 34 37 bitr2i 
 |-  ( ( { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. T /\ { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } C_ C ) <-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. ( T i^i ~P C ) )
39 33 38 sylib 
 |-  ( ( ph /\ c e. S ) -> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ c ) } e. ( T i^i ~P C ) )
40 31 39 eqeltrd 
 |-  ( ( ph /\ c e. S ) -> ( M ` c ) e. ( T i^i ~P C ) )
41 eleq1 
 |-  ( ( M ` c ) = t -> ( ( M ` c ) e. ( T i^i ~P C ) <-> t e. ( T i^i ~P C ) ) )
42 40 41 syl5ibcom 
 |-  ( ( ph /\ c e. S ) -> ( ( M ` c ) = t -> t e. ( T i^i ~P C ) ) )
43 42 rexlimdva 
 |-  ( ph -> ( E. c e. S ( M ` c ) = t -> t e. ( T i^i ~P C ) ) )
44 eqid 
 |-  U_ f e. t ( O ` ( L ` f ) ) = U_ f e. t ( O ` ( L ` f ) )
45 11 adantr 
 |-  ( ( ph /\ t e. ( T i^i ~P C ) ) -> ( K e. HL /\ W e. H ) )
46 inss1 
 |-  ( T i^i ~P C ) C_ T
47 46 sseli 
 |-  ( t e. ( T i^i ~P C ) -> t e. T )
48 47 adantl 
 |-  ( ( ph /\ t e. ( T i^i ~P C ) ) -> t e. T )
49 inss2 
 |-  ( T i^i ~P C ) C_ ~P C
50 49 sseli 
 |-  ( t e. ( T i^i ~P C ) -> t e. ~P C )
51 50 elpwid 
 |-  ( t e. ( T i^i ~P C ) -> t C_ C )
52 51 adantl 
 |-  ( ( ph /\ t e. ( T i^i ~P C ) ) -> t C_ C )
53 1 2 4 5 6 7 8 9 10 44 45 48 52 lcfr 
 |-  ( ( ph /\ t e. ( T i^i ~P C ) ) -> U_ f e. t ( O ` ( L ` f ) ) e. S )
54 1 2 3 4 5 6 7 8 9 10 45 48 52 44 mapdrval 
 |-  ( ( ph /\ t e. ( T i^i ~P C ) ) -> ( M ` U_ f e. t ( O ` ( L ` f ) ) ) = t )
55 fveqeq2 
 |-  ( c = U_ f e. t ( O ` ( L ` f ) ) -> ( ( M ` c ) = t <-> ( M ` U_ f e. t ( O ` ( L ` f ) ) ) = t ) )
56 55 rspcev 
 |-  ( ( U_ f e. t ( O ` ( L ` f ) ) e. S /\ ( M ` U_ f e. t ( O ` ( L ` f ) ) ) = t ) -> E. c e. S ( M ` c ) = t )
57 53 54 56 syl2anc 
 |-  ( ( ph /\ t e. ( T i^i ~P C ) ) -> E. c e. S ( M ` c ) = t )
58 57 ex 
 |-  ( ph -> ( t e. ( T i^i ~P C ) -> E. c e. S ( M ` c ) = t ) )
59 43 58 impbid 
 |-  ( ph -> ( E. c e. S ( M ` c ) = t <-> t e. ( T i^i ~P C ) ) )
60 28 59 bitrd 
 |-  ( ph -> ( t e. ran M <-> t e. ( T i^i ~P C ) ) )
61 60 eqrdv 
 |-  ( ph -> ran M = ( T i^i ~P C ) )
62 11 adantr 
 |-  ( ( ph /\ ( t e. S /\ u e. S ) ) -> ( K e. HL /\ W e. H ) )
63 simprl 
 |-  ( ( ph /\ ( t e. S /\ u e. S ) ) -> t e. S )
64 simprr 
 |-  ( ( ph /\ ( t e. S /\ u e. S ) ) -> u e. S )
65 1 4 5 3 62 63 64 mapd11 
 |-  ( ( ph /\ ( t e. S /\ u e. S ) ) -> ( ( M ` t ) = ( M ` u ) <-> t = u ) )
66 65 biimpd 
 |-  ( ( ph /\ ( t e. S /\ u e. S ) ) -> ( ( M ` t ) = ( M ` u ) -> t = u ) )
67 66 ralrimivva 
 |-  ( ph -> A. t e. S A. u e. S ( ( M ` t ) = ( M ` u ) -> t = u ) )
68 dff1o6 
 |-  ( M : S -1-1-onto-> ( T i^i ~P C ) <-> ( M Fn S /\ ran M = ( T i^i ~P C ) /\ A. t e. S A. u e. S ( ( M ` t ) = ( M ` u ) -> t = u ) ) )
69 19 61 67 68 syl3anbrc 
 |-  ( ph -> M : S -1-1-onto-> ( T i^i ~P C ) )