Theorem dicelval1stN

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

	Ref	Expression
Hypotheses	dicelval1st.l	|- .<_ = ( le ` K )
	dicelval1st.a	|- A = ( Atoms ` K )
	dicelval1st.h	|- H = ( LHyp ` K )
	dicelval1st.t	|- T = ( ( LTrn ` K ) ` W )
	dicelval1st.i	|- I = ( ( DIsoC ` K ) ` W )
Assertion	dicelval1stN	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) e. T )

Proof

Step	Hyp	Ref	Expression
1		dicelval1st.l	|- .<_ = ( le ` K )
2		dicelval1st.a	|- A = ( Atoms ` K )
3		dicelval1st.h	|- H = ( LHyp ` K )
4		dicelval1st.t	|- T = ( ( LTrn ` K ) ` W )
5		dicelval1st.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	|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
10	3 4 9 6 7	dvhvbase	|- ( ( K e. HL /\ W e. H ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( T X. ( ( TEndo ` K ) ` W ) ) )
11	10	adantr	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( T X. ( ( TEndo ` K ) ` W ) ) )
12	8 11	sseqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( T X. ( ( TEndo ` K ) ` W ) ) )
13	12	sseld	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) -> Y e. ( T X. ( ( TEndo ` K ) ` W ) ) ) )
14	13	3impia	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> Y e. ( T X. ( ( TEndo ` K ) ` W ) ) )
15		xp1st	|- ( Y e. ( T X. ( ( TEndo ` K ) ` W ) ) -> ( 1st ` Y ) e. T )
16	14 15	syl	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) e. T )