Metamath Proof Explorer

Theorem dih11

Description: The isomorphism H is one-to-one. Part of proof after Lemma N of Crawley p. 122 line 6. (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dih11.b ⊢ B = Base K
dih11.h ⊢ H = LHyp ⁡ K
dih11.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dih11 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X = I ⁡ Y ↔ X = Y

Proof

Step Hyp Ref Expression
1 dih11.b ⊢ B = Base K
2 dih11.h ⊢ H = LHyp ⁡ K
3 dih11.i ⊢ I = DIsoH ⁡ K ⁡ W
4 eqss ⊢ I ⁡ X = I ⁡ Y ↔ I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X
5 eqid ⊢ ≤ K = ≤ K
6 1 5 2 3 dihord ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ⊆ I ⁡ Y ↔ X ≤ K Y
7 1 5 2 3 dihord ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ B ∧ X ∈ B → I ⁡ Y ⊆ I ⁡ X ↔ Y ≤ K X
8 7 3com23 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ Y ⊆ I ⁡ X ↔ Y ≤ K X
9 6 8 anbi12d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X ↔ X ≤ K Y ∧ Y ≤ K X
10 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → K ∈ HL
11 10 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → K ∈ Lat
12 1 5 latasymb ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ∧ Y ≤ K X ↔ X = Y
13 11 12 syld3an1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → X ≤ K Y ∧ Y ≤ K X ↔ X = Y
14 9 13 bitrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X ↔ X = Y
15 4 14 bitrid ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X = I ⁡ Y ↔ X = Y