Theorem dicelval2nd

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 16-Feb-2014)

	Ref	Expression
Hypotheses	dicelval2nd.l	|- .<_ = ( le ` K )
	dicelval2nd.a	|- A = ( Atoms ` K )
	dicelval2nd.h	|- H = ( LHyp ` K )
	dicelval2nd.e	|- E = ( ( TEndo ` K ) ` W )
	dicelval2nd.i	|- I = ( ( DIsoC ` K ) ` W )
Assertion	dicelval2nd	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 2nd ` Y ) e. E )

Proof

Step	Hyp	Ref	Expression
1		dicelval2nd.l	|- .<_ = ( le ` K )
2		dicelval2nd.a	|- A = ( Atoms ` K )
3		dicelval2nd.h	|- H = ( LHyp ` K )
4		dicelval2nd.e	|- E = ( ( TEndo ` K ) ` W )
5		dicelval2nd.i	|- I = ( ( DIsoC ` K ) ` W )
6		eqid	|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
7		eqid	|- ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
8	1 2 3 5 6 7	dicssdvh	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
9		eqid	|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
10	3 9 4 6 7	dvhvbase	|- ( ( K e. HL /\ W e. H ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( ( ( LTrn ` K ) ` W ) X. E ) )
11	10	adantr	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( ( ( LTrn ` K ) ` W ) X. E ) )
12	8 11	sseqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( ( ( LTrn ` K ) ` W ) X. E ) )
13	12	sseld	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) -> Y e. ( ( ( LTrn ` K ) ` W ) X. E ) ) )
14	13	3impia	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> Y e. ( ( ( LTrn ` K ) ` W ) X. E ) )
15		xp2nd	|- ( Y e. ( ( ( LTrn ` K ) ` W ) X. E ) -> ( 2nd ` Y ) e. E )
16	14 15	syl	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 2nd ` Y ) e. E )