Theorem dibval

Description: The partial isomorphism B for a lattice K . (Contributed by NM, 8-Dec-2013)

	Ref	Expression
Hypotheses	dibval.b	|- B = ( Base ` K )
	dibval.h	|- H = ( LHyp ` K )
	dibval.t	|- T = ( ( LTrn ` K ) ` W )
	dibval.o	|- .0. = ( f e. T |-> ( _I |` B ) )
	dibval.j	|- J = ( ( DIsoA ` K ) ` W )
	dibval.i	|- I = ( ( DIsoB ` K ) ` W )
Assertion	dibval	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( I ` X ) = ( ( J ` X ) X. { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		dibval.b	|- B = ( Base ` K )
2		dibval.h	|- H = ( LHyp ` K )
3		dibval.t	|- T = ( ( LTrn ` K ) ` W )
4		dibval.o	|- .0. = ( f e. T |-> ( _I |` B ) )
5		dibval.j	|- J = ( ( DIsoA ` K ) ` W )
6		dibval.i	|- I = ( ( DIsoB ` K ) ` W )
7	1 2 3 4 5 6	dibfval	|- ( ( K e. V /\ W e. H ) -> I = ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) )
8	7	adantr	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> I = ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) )
9	8	fveq1d	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( I ` X ) = ( ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) ` X ) )
10		fveq2	|- ( x = X -> ( J ` x ) = ( J ` X ) )
11	10	xpeq1d	|- ( x = X -> ( ( J ` x ) X. { .0. } ) = ( ( J ` X ) X. { .0. } ) )
12		eqid	|- ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) = ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) )
13		fvex	|- ( J ` X ) e. _V
14		snex	|- { .0. } e. _V
15	13 14	xpex	|- ( ( J ` X ) X. { .0. } ) e. _V
16	11 12 15	fvmpt	|- ( X e. dom J -> ( ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) ` X ) = ( ( J ` X ) X. { .0. } ) )
17	16	adantl	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) ` X ) = ( ( J ` X ) X. { .0. } ) )
18	9 17	eqtrd	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( I ` X ) = ( ( J ` X ) X. { .0. } ) )