This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dicelval1sta

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

		Ref	Expression
	Hypotheses	dicelval1sta.l	\|- .<_ = ( le ` K )
		dicelval1sta.a	\|- A = ( Atoms ` K )
		dicelval1sta.h	\|- H = ( LHyp ` K )
		dicelval1sta.p	\|- P = ( ( oc ` K ) ` W )
		dicelval1sta.t	\|- T = ( ( LTrn ` K ) ` W )
		dicelval1sta.i	\|- I = ( ( DIsoC ` K ) ` W )
	Assertion	dicelval1sta	\|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) )

Proof

Step	Hyp	Ref	Expression
1		dicelval1sta.l	\|- .<_ = ( le ` K )
2		dicelval1sta.a	\|- A = ( Atoms ` K )
3		dicelval1sta.h	\|- H = ( LHyp ` K )
4		dicelval1sta.p	\|- P = ( ( oc ` K ) ` W )
5		dicelval1sta.t	\|- T = ( ( LTrn ` K ) ` W )
6		dicelval1sta.i	\|- I = ( ( DIsoC ` K ) ` W )
7		eqid	\|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
8	1 2 3 4 5 7 6	dicval	\|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. \| ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
9	8	eleq2d	\|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) <-> Y e. { <. f , s >. \| ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) )
10	9	biimp3a	\|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> Y e. { <. f , s >. \| ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
11		eqeq1	\|- ( f = ( 1st ` Y ) -> ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) <-> ( 1st ` Y ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) ) )
12	11	anbi1d	\|- ( f = ( 1st ` Y ) -> ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) <-> ( ( 1st ` Y ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) )
13		fveq1	\|- ( s = ( 2nd ` Y ) -> ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) )
14	13	eqeq2d	\|- ( s = ( 2nd ` Y ) -> ( ( 1st ` Y ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) <-> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) ) )
15		eleq1	\|- ( s = ( 2nd ` Y ) -> ( s e. ( ( TEndo ` K ) ` W ) <-> ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) )
16	14 15	anbi12d	\|- ( s = ( 2nd ` Y ) -> ( ( ( 1st ` Y ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) <-> ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) ) )
17	12 16	elopabi	\|- ( Y e. { <. f , s >. \| ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } -> ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) )
18	10 17	syl	\|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) )
19	18	simpld	\|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) )