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 ‘ 𝐾 )
diadmle.h 𝐻 = ( LHyp ‘ 𝐾 )
diadmle.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diadmleN ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 𝑊 )

Proof

Step Hyp Ref Expression
1 diadmle.l = ( le ‘ 𝐾 )
2 diadmle.h 𝐻 = ( LHyp ‘ 𝐾 )
3 diadmle.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5 4 1 2 3 diaeldm ( ( 𝐾𝑉𝑊𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 𝑊 ) ) )
6 5 simplbda ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 𝑊 )