Theorem dihopelvalbN

Description: Ordered pair member of the partial isomorphism H for argument under W . (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihval3.b	|- B = ( Base ` K )
	dihval3.l	|- .<_ = ( le ` K )
	dihval3.h	|- H = ( LHyp ` K )
	dihval3.t	|- T = ( ( LTrn ` K ) ` W )
	dihval3.r	|- R = ( ( trL ` K ) ` W )
	dihval3.o	|- O = ( g e. T |-> ( _I |` B ) )
	dihval3.i	|- I = ( ( DIsoH ` K ) ` W )
Assertion	dihopelvalbN	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. F , S >. e. ( I ` X ) <-> ( ( F e. T /\ ( R ` F ) .<_ X ) /\ S = O ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihval3.b	|- B = ( Base ` K )
2		dihval3.l	|- .<_ = ( le ` K )
3		dihval3.h	|- H = ( LHyp ` K )
4		dihval3.t	|- T = ( ( LTrn ` K ) ` W )
5		dihval3.r	|- R = ( ( trL ` K ) ` W )
6		dihval3.o	|- O = ( g e. T |-> ( _I |` B ) )
7		dihval3.i	|- I = ( ( DIsoH ` K ) ` W )
8		eqid	|- ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
9	1 2 3 7 8	dihvalb	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( ( DIsoB ` K ) ` W ) ` X ) )
10	9	eleq2d	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. F , S >. e. ( I ` X ) <-> <. F , S >. e. ( ( ( DIsoB ` K ) ` W ) ` X ) ) )
11	1 2 3 4 5 6 8	dibopelval3	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. F , S >. e. ( ( ( DIsoB ` K ) ` W ) ` X ) <-> ( ( F e. T /\ ( R ` F ) .<_ X ) /\ S = O ) ) )
12	10 11	bitrd	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. F , S >. e. ( I ` X ) <-> ( ( F e. T /\ ( R ` F ) .<_ X ) /\ S = O ) ) )