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 ) |
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 ) |