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 )