Theorem mapdrvallem3

Description: Lemma for mapdrval . (Contributed by NM, 2-Feb-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 ) )
	mapdrval.v	|- V = ( Base ` U )
	mapdrvallem2.a	|- A = ( LSAtoms ` U )
	mapdrvallem2.n	|- N = ( LSpan ` U )
	mapdrvallem2.z	|- .0. = ( 0g ` U )
	mapdrvallem2.y	|- Y = ( 0g ` D )
Assertion	mapdrvallem3	|- ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ 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		mapdrval.v	|- V = ( Base ` U )
16		mapdrvallem2.a	|- A = ( LSAtoms ` U )
17		mapdrvallem2.n	|- N = ( LSpan ` U )
18		mapdrvallem2.z	|- .0. = ( 0g ` U )
19		mapdrvallem2.y	|- Y = ( 0g ` D )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	mapdrvallem2	|- ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ Q } C_ R )
21		2fveq3	|- ( h = f -> ( O ` ( L ` h ) ) = ( O ` ( L ` f ) ) )
22	21	ssiun2s	|- ( f e. R -> ( O ` ( L ` f ) ) C_ U_ h e. R ( O ` ( L ` h ) ) )
23	22	adantl	|- ( ( ph /\ f e. R ) -> ( O ` ( L ` f ) ) C_ U_ h e. R ( O ` ( L ` h ) ) )
24	23 14	sseqtrrdi	|- ( ( ph /\ f e. R ) -> ( O ` ( L ` f ) ) C_ Q )
25	13 24	ssrabdv	|- ( ph -> R C_ { f e. C | ( O ` ( L ` f ) ) C_ Q } )
26	20 25	eqssd	|- ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ Q } = R )