Metamath Proof Explorer


Theorem diadmleN

Description: A member of domain of the partial isomorphism A is under the fiducial hyperplane. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diadmle.l
|- .<_ = ( le ` K )
diadmle.h
|- H = ( LHyp ` K )
diadmle.i
|- I = ( ( DIsoA ` K ) ` W )
Assertion diadmleN
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X .<_ W )

Proof

Step Hyp Ref Expression
1 diadmle.l
 |-  .<_ = ( le ` K )
2 diadmle.h
 |-  H = ( LHyp ` K )
3 diadmle.i
 |-  I = ( ( DIsoA ` K ) ` W )
4 eqid
 |-  ( Base ` K ) = ( Base ` K )
5 4 1 2 3 diaeldm
 |-  ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> ( X e. ( Base ` K ) /\ X .<_ W ) ) )
6 5 simplbda
 |-  ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X .<_ W )