Metamath Proof Explorer

Theorem dia11N

Description: The partial isomorphism A for a lattice K is one-to-one in the region under co-atom W . Part of Lemma M of Crawley p. 120 line 28. (Contributed by NM, 25-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia11.b ⊢ B = Base K
dia11.l ⊢ ≤ ˙ = ≤ K
dia11.h ⊢ H = LHyp ⁡ K
dia11.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion dia11N ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X = I ⁡ Y ↔ X = Y

Proof

Step Hyp Ref Expression
1 dia11.b ⊢ B = Base K
2 dia11.l ⊢ ≤ ˙ = ≤ K
3 dia11.h ⊢ H = LHyp ⁡ K
4 dia11.i ⊢ I = DIsoA ⁡ K ⁡ W
5 eqss ⊢ I ⁡ X = I ⁡ Y ↔ I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X
6 1 2 3 4 diaord ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ↔ X ≤ ˙ Y
7 1 2 3 4 diaord ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ B ∧ Y ≤ ˙ W ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ Y ⊆ I ⁡ X ↔ Y ≤ ˙ X
8 7 3com23 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ Y ⊆ I ⁡ X ↔ Y ≤ ˙ X
9 6 8 anbi12d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X ↔ X ≤ ˙ Y ∧ Y ≤ ˙ X
10 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → K ∈ HL
11 10 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → K ∈ Lat
12 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → X ∈ B
13 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → Y ∈ B
14 1 2 latasymb ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ X = Y
15 11 12 13 14 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ X = Y
16 9 15 bitrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X ⊆ I ⁡ Y ∧ I ⁡ Y ⊆ I ⁡ X ↔ X = Y
17 5 16 bitrid ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W → I ⁡ X = I ⁡ Y ↔ X = Y