Metamath Proof Explorer


Theorem mapdrval

Description: Given a dual subspace R (of functionals with closed kernels), reconstruct the subspace Q that maps to it. (Contributed by NM, 12-Mar-2015)

Ref Expression
Hypotheses mapdrval.h
|- H = ( LHyp ` K )
mapdrval.o
|- O = ( ( ocH ` K ) ` W )
mapdrval.m
|- M = ( ( mapd ` K ) ` W )
mapdrval.u
|- U = ( ( DVecH ` K ) ` W )
mapdrval.s
|- S = ( LSubSp ` U )
mapdrval.f
|- F = ( LFnl ` U )
mapdrval.l
|- L = ( LKer ` U )
mapdrval.d
|- D = ( LDual ` U )
mapdrval.t
|- T = ( LSubSp ` D )
mapdrval.c
|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
mapdrval.k
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdrval.r
|- ( ph -> R e. T )
mapdrval.e
|- ( ph -> R C_ C )
mapdrval.q
|- Q = U_ h e. R ( O ` ( L ` h ) )
Assertion mapdrval
|- ( ph -> ( M ` Q ) = R )

Proof

Step Hyp Ref Expression
1 mapdrval.h
 |-  H = ( LHyp ` K )
2 mapdrval.o
 |-  O = ( ( ocH ` K ) ` W )
3 mapdrval.m
 |-  M = ( ( mapd ` K ) ` W )
4 mapdrval.u
 |-  U = ( ( DVecH ` K ) ` W )
5 mapdrval.s
 |-  S = ( LSubSp ` U )
6 mapdrval.f
 |-  F = ( LFnl ` U )
7 mapdrval.l
 |-  L = ( LKer ` U )
8 mapdrval.d
 |-  D = ( LDual ` U )
9 mapdrval.t
 |-  T = ( LSubSp ` D )
10 mapdrval.c
 |-  C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
11 mapdrval.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 mapdrval.r
 |-  ( ph -> R e. T )
13 mapdrval.e
 |-  ( ph -> R C_ C )
14 mapdrval.q
 |-  Q = U_ h e. R ( O ` ( L ` h ) )
15 1 2 4 5 6 7 8 9 10 14 11 12 13 lcfr
 |-  ( ph -> Q e. S )
16 1 4 5 6 7 2 3 11 15 10 mapdvalc
 |-  ( ph -> ( M ` Q ) = { f e. C | ( O ` ( L ` f ) ) C_ Q } )
17 2fveq3
 |-  ( h = i -> ( O ` ( L ` h ) ) = ( O ` ( L ` i ) ) )
18 17 cbviunv
 |-  U_ h e. R ( O ` ( L ` h ) ) = U_ i e. R ( O ` ( L ` i ) )
19 14 18 eqtri
 |-  Q = U_ i e. R ( O ` ( L ` i ) )
20 eqid
 |-  ( Base ` U ) = ( Base ` U )
21 eqid
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
22 eqid
 |-  ( LSpan ` U ) = ( LSpan ` U )
23 eqid
 |-  ( 0g ` U ) = ( 0g ` U )
24 eqid
 |-  ( 0g ` D ) = ( 0g ` D )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 19 20 21 22 23 24 mapdrvallem3
 |-  ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ Q } = R )
26 16 25 eqtrd
 |-  ( ph -> ( M ` Q ) = R )