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 ⊢ H = LHyp ⁡ K
dia1eldm.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion dia1eldmN ⊢ K ∈ HL ∧ W ∈ H → W ∈ dom ⁡ I

Proof

Step Hyp Ref Expression
1 dia1eldm.h ⊢ H = LHyp ⁡ K
2 dia1eldm.i ⊢ I = DIsoA ⁡ K ⁡ W
3 eqid ⊢ Base K = Base K
4 3 1 lhpbase ⊢ W ∈ H → W ∈ Base K
5 4 adantl ⊢ K ∈ HL ∧ W ∈ H → W ∈ Base K
6 hllat ⊢ K ∈ HL → K ∈ Lat
7 eqid ⊢ ≤ K = ≤ K
8 3 7 latref ⊢ K ∈ Lat ∧ W ∈ Base K → W ≤ K W
9 6 4 8 syl2an ⊢ K ∈ HL ∧ W ∈ H → W ≤ K W
10 3 7 1 2 diaeldm ⊢ K ∈ HL ∧ W ∈ H → W ∈ dom ⁡ I ↔ W ∈ Base K ∧ W ≤ K W
11 5 9 10 mpbir2and ⊢ K ∈ HL ∧ W ∈ H → W ∈ dom ⁡ I