Theorem dibopelvalN

Description: Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014) (Revised by Mario Carneiro, 6-May-2015) (New usage is discouraged.)

	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	dibopelvalN	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( <. F , S >. e. ( I ` X ) <-> ( F e. ( J ` X ) /\ S = .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	dibval	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( I ` X ) = ( ( J ` X ) X. { .0. } ) )
8	7	eleq2d	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( <. F , S >. e. ( I ` X ) <-> <. F , S >. e. ( ( J ` X ) X. { .0. } ) ) )
9		opelxp	|- ( <. F , S >. e. ( ( J ` X ) X. { .0. } ) <-> ( F e. ( J ` X ) /\ S e. { .0. } ) )
10	3	fvexi	|- T e. _V
11	10	mptex	|- ( f e. T |-> ( _I |` B ) ) e. _V
12	4 11	eqeltri	|- .0. e. _V
13	12	elsn2	|- ( S e. { .0. } <-> S = .0. )
14	13	anbi2i	|- ( ( F e. ( J ` X ) /\ S e. { .0. } ) <-> ( F e. ( J ` X ) /\ S = .0. ) )
15	9 14	bitri	|- ( <. F , S >. e. ( ( J ` X ) X. { .0. } ) <-> ( F e. ( J ` X ) /\ S = .0. ) )
16	8 15	bitrdi	|- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( <. F , S >. e. ( I ` X ) <-> ( F e. ( J ` X ) /\ S = .0. ) ) )