Theorem mapdvalc

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015)

	Ref	Expression
Hypotheses	mapdval.h	|- H = ( LHyp ` K )
	mapdval.u	|- U = ( ( DVecH ` K ) ` W )
	mapdval.s	|- S = ( LSubSp ` U )
	mapdval.f	|- F = ( LFnl ` U )
	mapdval.l	|- L = ( LKer ` U )
	mapdval.o	|- O = ( ( ocH ` K ) ` W )
	mapdval.m	|- M = ( ( mapd ` K ) ` W )
	mapdval.k	|- ( ph -> ( K e. X /\ W e. H ) )
	mapdval.t	|- ( ph -> T e. S )
	mapdvalc.c	|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
Assertion	mapdvalc	|- ( ph -> ( M ` T ) = { f e. C | ( O ` ( L ` f ) ) C_ T } )

Proof

Step	Hyp	Ref	Expression
1		mapdval.h	|- H = ( LHyp ` K )
2		mapdval.u	|- U = ( ( DVecH ` K ) ` W )
3		mapdval.s	|- S = ( LSubSp ` U )
4		mapdval.f	|- F = ( LFnl ` U )
5		mapdval.l	|- L = ( LKer ` U )
6		mapdval.o	|- O = ( ( ocH ` K ) ` W )
7		mapdval.m	|- M = ( ( mapd ` K ) ` W )
8		mapdval.k	|- ( ph -> ( K e. X /\ W e. H ) )
9		mapdval.t	|- ( ph -> T e. S )
10		mapdvalc.c	|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
11	1 2 3 4 5 6 7 8 9	mapdval	|- ( ph -> ( M ` T ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } )
12		anass	|- ( ( ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) /\ ( O ` ( L ` f ) ) C_ T ) <-> ( f e. F /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) ) )
13	10	lcfl1lem	|- ( f e. C <-> ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) )
14	13	anbi1i	|- ( ( f e. C /\ ( O ` ( L ` f ) ) C_ T ) <-> ( ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) /\ ( O ` ( L ` f ) ) C_ T ) )
15	14	bicomi	|- ( ( ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) /\ ( O ` ( L ` f ) ) C_ T ) <-> ( f e. C /\ ( O ` ( L ` f ) ) C_ T ) )
16	15	a1i	|- ( ph -> ( ( ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) /\ ( O ` ( L ` f ) ) C_ T ) <-> ( f e. C /\ ( O ` ( L ` f ) ) C_ T ) ) )
17	12 16	bitr3id	|- ( ph -> ( ( f e. F /\ ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) ) <-> ( f e. C /\ ( O ` ( L ` f ) ) C_ T ) ) )
18	17	rabbidva2	|- ( ph -> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } = { f e. C | ( O ` ( L ` f ) ) C_ T } )
19	11 18	eqtrd	|- ( ph -> ( M ` T ) = { f e. C | ( O ` ( L ` f ) ) C_ T } )