Metamath Proof Explorer


Theorem dib11N

Description: The isomorphism B for a lattice K is one-to-one in the region under co-atom W . (Contributed by NM, 24-Feb-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dib11.b B = Base K
dib11.l ˙ = K
dib11.h H = LHyp K
dib11.i I = DIsoB K W
Assertion dib11N K HL W H X B X ˙ W Y B Y ˙ W I X = I Y X = Y

Proof

Step Hyp Ref Expression
1 dib11.b B = Base K
2 dib11.l ˙ = K
3 dib11.h H = LHyp K
4 dib11.i I = DIsoB K W
5 eqss I X = I Y I X I Y I Y I X
6 1 2 3 4 dibord K HL W H X B X ˙ W Y B Y ˙ W I X I Y X ˙ Y
7 1 2 3 4 dibord 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 syl5bb K HL W H X B X ˙ W Y B Y ˙ W I X = I Y X = Y