Theorem mapdval 35241

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

Hypotheses

Ref	Expression
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

Ref	Expression
mapdval	|- ( ph -> ( M ` T ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } )

Distinct variable groups:   f, K   f, F   f, W   T, f

Allowed substitution hints:   ph( f)   S( f)   U( f)   H( f)   L( f)   M( f)   O( f)   X( f)

Proof of Theorem mapdval

Dummy variable s is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapdval.k	. . . 4 |- ( ph -> ( K e. X /\ W e. H ) )
2		mapdval.h	. . . . 5 |- H = ( LHyp ` K )
3		mapdval.u	. . . . 5 |- U = ( ( DVecH ` K ) ` W )
4		mapdval.s	. . . . 5 |- S = ( LSubSp ` U )
5		mapdval.f	. . . . 5 |- F = (LFnl ` U )
6		mapdval.l	. . . . 5 |- L = (LKer ` U )
7		mapdval.o	. . . . 5 |- O = ( ( ocH ` K ) ` W )
8		mapdval.m	. . . . 5 |- M = ( (mapd ` K ) ` W )
9	2, 3, 4, 5, 6, 7, 8	mapdfval 35240	. . . 4 |- ( ( K e. X /\ W e. H ) -> M = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )
10	1, 9	syl 17	. . 3 |- ( ph -> M = ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) )
11	10	fveq1d 5890	. 2 |- ( ph -> ( M ` T ) = ( ( s e. S |-> { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) ` T ) )
12		mapdval.t	. . 3 |- ( ph -> T e. S )
13		fvex 5898	. . . . 5 |- (LFnl ` U ) e. _V
14	5, 13	eqeltri 2536	. . . 4 |- F e. _V
15	14	rabex 4568	. . 3 |- { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } e. _V
16		sseq2 3466	. . . . . 6 |- ( s = T -> ( ( O ` ( L ` f ) ) C_ s <-> ( O ` ( L ` f ) ) C_ T ) )
17	16	anbi2d 715	. . . . 5 |- ( s = T -> ( ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) <-> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) ) )
18	17	rabbidv 3048	. . . 4 |- ( 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 ) } )
19		eqid 2462	. . . 4 |- ( 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 ) } )
20	18, 19	fvmptg 5969	. . 3 |- ( ( 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 ) } )
21	12, 15, 20	sylancl 673	. 2 |- ( 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 ) } )
22	11, 21	eqtrd 2496	1 |- ( ph -> ( M ` T ) = { f e. F | ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ T ) } )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1455   e. wcel 1898   {crab 2753   _Vcvv 3057   C_ wss 3416   |-> cmpt 4475   ` cfv 5601   LSubSpclss 18204  LFnlclfn 32668  LKerclk 32696   LHypclh 33594   DVecHcdvh 34691   ocHcoch 34960  mapdcmpd 35237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-mapd 35238

This theorem is referenced by:  mapdvalc  35242  mapddlssN  35253  mapdsn  35254  mapd1o  35261  mapd0  35278