Metamath Proof Explorer

Theorem dian0

Description: The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014)

Ref Expression
Hypotheses dian0.b ⊢ B = Base K
dian0.l ⊢ ≤ ˙ = ≤ K
dian0.h ⊢ H = LHyp ⁡ K
dian0.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion dian0 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X ≠ ∅

Proof

Step Hyp Ref Expression
1 dian0.b ⊢ B = Base K
2 dian0.l ⊢ ≤ ˙ = ≤ K
3 dian0.h ⊢ H = LHyp ⁡ K
4 dian0.i ⊢ I = DIsoA ⁡ K ⁡ W
5 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
6 1 3 5 idltrn ⊢ K ∈ HL ∧ W ∈ H → I ↾ B ∈ LTrn ⁡ K ⁡ W
7 6 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ↾ B ∈ LTrn ⁡ K ⁡ W
8 eqid ⊢ 0. ⁡ K = 0. ⁡ K
9 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
10 1 8 3 9 trlid0 ⊢ K ∈ HL ∧ W ∈ H → trL ⁡ K ⁡ W ⁡ I ↾ B = 0. ⁡ K
11 10 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → trL ⁡ K ⁡ W ⁡ I ↾ B = 0. ⁡ K
12 hlatl ⊢ K ∈ HL → K ∈ AtLat
13 12 adantr ⊢ K ∈ HL ∧ W ∈ H → K ∈ AtLat
14 simpl ⊢ X ∈ B ∧ X ≤ ˙ W → X ∈ B
15 1 2 8 atl0le ⊢ K ∈ AtLat ∧ X ∈ B → 0. ⁡ K ≤ ˙ X
16 13 14 15 syl2an ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → 0. ⁡ K ≤ ˙ X
17 11 16 eqbrtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → trL ⁡ K ⁡ W ⁡ I ↾ B ≤ ˙ X
18 1 2 3 5 9 4 diaelval ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ↾ B ∈ I ⁡ X ↔ I ↾ B ∈ LTrn ⁡ K ⁡ W ∧ trL ⁡ K ⁡ W ⁡ I ↾ B ≤ ˙ X
19 7 17 18 mpbir2and ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ↾ B ∈ I ⁡ X
20 19 ne0d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X ≠ ∅