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 𝐻 = ( LHyp ‘ 𝐾 )
dia1eldm.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion dia1eldmN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑊 ∈ dom 𝐼 )

Proof

Step Hyp Ref Expression
1 dia1eldm.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dia1eldm.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
3 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4 3 1 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
5 4 adantl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
6 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
7 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 3 7 latref ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → 𝑊 ( le ‘ 𝐾 ) 𝑊 )
9 6 4 8 syl2an ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑊 ( le ‘ 𝐾 ) 𝑊 )
10 3 7 1 2 diaeldm ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑊 ∈ dom 𝐼 ↔ ( 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ( le ‘ 𝐾 ) 𝑊 ) ) )
11 5 9 10 mpbir2and ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑊 ∈ dom 𝐼 )