Theorem dia1eldmN

Description: The fiducial hyperplane (the largest allowed lattice element) belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dia1eldm.h	|- H = ( LHyp ` K )
	dia1eldm.i	|- I = ( ( DIsoA ` K ) ` W )
Assertion	dia1eldmN	|- ( ( K e. HL /\ W e. H ) -> W e. dom I )

Proof

Step	Hyp	Ref	Expression
1		dia1eldm.h	|- H = ( LHyp ` K )
2		dia1eldm.i	|- I = ( ( DIsoA ` K ) ` W )
3		eqid	|- ( Base ` K ) = ( Base ` K )
4	3 1	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
5	4	adantl	|- ( ( K e. HL /\ W e. H ) -> W e. ( Base ` K ) )
6		hllat	|- ( K e. HL -> K e. Lat )
7		eqid	|- ( le ` K ) = ( le ` K )
8	3 7	latref	|- ( ( K e. Lat /\ W e. ( Base ` K ) ) -> W ( le ` K ) W )
9	6 4 8	syl2an	|- ( ( K e. HL /\ W e. H ) -> W ( le ` K ) W )
10	3 7 1 2	diaeldm	|- ( ( K e. HL /\ W e. H ) -> ( W e. dom I <-> ( W e. ( Base ` K ) /\ W ( le ` K ) W ) ) )
11	5 9 10	mpbir2and	|- ( ( K e. HL /\ W e. H ) -> W e. dom I )