Metamath Proof Explorer

Theorem dia0eldmN

Description: The lattice zero belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia0eldm.z ⊢ 0 ˙ = 0. ⁡ K
dia0eldm.h ⊢ H = LHyp ⁡ K
dia0eldm.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion dia0eldmN ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ dom ⁡ I

Proof

Step Hyp Ref Expression
1 dia0eldm.z ⊢ 0 ˙ = 0. ⁡ K
2 dia0eldm.h ⊢ H = LHyp ⁡ K
3 dia0eldm.i ⊢ I = DIsoA ⁡ K ⁡ W
4 hlop ⊢ K ∈ HL → K ∈ OP
5 4 adantr ⊢ K ∈ HL ∧ W ∈ H → K ∈ OP
6 eqid ⊢ Base K = Base K
7 6 1 op0cl ⊢ K ∈ OP → 0 ˙ ∈ Base K
8 5 7 syl ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ Base K
9 6 2 lhpbase ⊢ W ∈ H → W ∈ Base K
10 eqid ⊢ ≤ K = ≤ K
11 6 10 1 op0le ⊢ K ∈ OP ∧ W ∈ Base K → 0 ˙ ≤ K W
12 4 9 11 syl2an ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ≤ K W
13 6 10 2 3 diaeldm ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ dom ⁡ I ↔ 0 ˙ ∈ Base K ∧ 0 ˙ ≤ K W
14 8 12 13 mpbir2and ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ dom ⁡ I