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 𝐼 ) → 𝑋 ≤ 𝑊 ) |
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 𝐼 ) → 𝑋 ≤ 𝑊 ) |