This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )