Theorem dihglblem3aN

Description: Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihglblem.b	|- B = ( Base ` K )
	dihglblem.l	|- .<_ = ( le ` K )
	dihglblem.m	|- ./\ = ( meet ` K )
	dihglblem.g	|- G = ( glb ` K )
	dihglblem.h	|- H = ( LHyp ` K )
	dihglblem.t	|- T = { u e. B | E. v e. S u = ( v ./\ W ) }
	dihglblem.i	|- J = ( ( DIsoB ` K ) ` W )
	dihglblem.ih	|- I = ( ( DIsoH ` K ) ` W )
Assertion	dihglblem3aN	|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = |^|_ x e. T ( I ` x ) )

Proof

Step	Hyp	Ref	Expression
1		dihglblem.b	|- B = ( Base ` K )
2		dihglblem.l	|- .<_ = ( le ` K )
3		dihglblem.m	|- ./\ = ( meet ` K )
4		dihglblem.g	|- G = ( glb ` K )
5		dihglblem.h	|- H = ( LHyp ` K )
6		dihglblem.t	|- T = { u e. B | E. v e. S u = ( v ./\ W ) }
7		dihglblem.i	|- J = ( ( DIsoB ` K ) ` W )
8		dihglblem.ih	|- I = ( ( DIsoH ` K ) ` W )
9	1 2 3 4 5 6	dihglblem2N	|- ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) -> ( G ` S ) = ( G ` T ) )
10	9	3adant2r	|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( G ` S ) = ( G ` T ) )
11	10	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = ( I ` ( G ` T ) ) )
12	1 2 3 4 5 6 7 8	dihglblem3N	|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( I ` ( G ` T ) ) = |^|_ x e. T ( I ` x ) )
13	11 12	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = |^|_ x e. T ( I ` x ) )