Theorem mapdval

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 )
Assertion	mapdval	|- ( ph -> ( M ` T ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( 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	1 2 3 4 5 6 7	mapdfval	|- ( ( K e. X /\ W e. H ) -> M = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )
11	8 10	syl	|- ( ph -> M = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )
12	11	fveq1d	|- ( ph -> ( M ` T ) = ( ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) ` T ) )
13	4	fvexi	|- F e. _V
14	13	rabex	|- { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } e. _V
15		sseq2	|- ( s = T -> ( ( O ` ( L ` f ) ) C_ s <-> ( O ` ( L ` f ) ) C_ T ) )
16	15	anbi2d	|- ( s = T -> ( ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) <-> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) ) )
17	16	rabbidv	|- ( s = T -> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } )
18		eqid	|- ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } )
19	17 18	fvmptg	|- ( ( T e. S /\ { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } e. _V ) -> ( ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) ` T ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } )
20	9 14 19	sylancl	|- ( ph -> ( ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) ` T ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } )
21	12 20	eqtrd	|- ( ph -> ( M ` T ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } )