Metamath Proof Explorer


Theorem dihmeetbclemN

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetc.b B = Base K
dihmeetc.l ˙ = K
dihmeetc.m ˙ = meet K
dihmeetc.h H = LHyp K
dihmeetc.i I = DIsoH K W
Assertion dihmeetbclemN K HL W H X B Y B X ˙ Y ˙ W I X ˙ Y = I X I Y I W

Proof

Step Hyp Ref Expression
1 dihmeetc.b B = Base K
2 dihmeetc.l ˙ = K
3 dihmeetc.m ˙ = meet K
4 dihmeetc.h H = LHyp K
5 dihmeetc.i I = DIsoH K W
6 simp3 K HL W H X B Y B X ˙ Y ˙ W X ˙ Y ˙ W
7 simp1l K HL W H X B Y B X ˙ Y ˙ W K HL
8 7 hllatd K HL W H X B Y B X ˙ Y ˙ W K Lat
9 simp2l K HL W H X B Y B X ˙ Y ˙ W X B
10 simp2r K HL W H X B Y B X ˙ Y ˙ W Y B
11 1 3 latmcl K Lat X B Y B X ˙ Y B
12 8 9 10 11 syl3anc K HL W H X B Y B X ˙ Y ˙ W X ˙ Y B
13 simp1r K HL W H X B Y B X ˙ Y ˙ W W H
14 1 4 lhpbase W H W B
15 13 14 syl K HL W H X B Y B X ˙ Y ˙ W W B
16 1 2 3 latleeqm1 K Lat X ˙ Y B W B X ˙ Y ˙ W X ˙ Y ˙ W = X ˙ Y
17 8 12 15 16 syl3anc K HL W H X B Y B X ˙ Y ˙ W X ˙ Y ˙ W X ˙ Y ˙ W = X ˙ Y
18 6 17 mpbid K HL W H X B Y B X ˙ Y ˙ W X ˙ Y ˙ W = X ˙ Y
19 hlol K HL K OL
20 7 19 syl K HL W H X B Y B X ˙ Y ˙ W K OL
21 1 3 latmassOLD K OL X B Y B W B X ˙ Y ˙ W = X ˙ Y ˙ W
22 20 9 10 15 21 syl13anc K HL W H X B Y B X ˙ Y ˙ W X ˙ Y ˙ W = X ˙ Y ˙ W
23 18 22 eqtr3d K HL W H X B Y B X ˙ Y ˙ W X ˙ Y = X ˙ Y ˙ W
24 23 fveq2d K HL W H X B Y B X ˙ Y ˙ W I X ˙ Y = I X ˙ Y ˙ W
25 simp1 K HL W H X B Y B X ˙ Y ˙ W K HL W H
26 1 3 latmcl K Lat Y B W B Y ˙ W B
27 8 10 15 26 syl3anc K HL W H X B Y B X ˙ Y ˙ W Y ˙ W B
28 1 2 3 latmle2 K Lat Y B W B Y ˙ W ˙ W
29 8 10 15 28 syl3anc K HL W H X B Y B X ˙ Y ˙ W Y ˙ W ˙ W
30 1 2 3 4 5 dihmeetbN K HL W H X B Y ˙ W B Y ˙ W ˙ W I X ˙ Y ˙ W = I X I Y ˙ W
31 25 9 27 29 30 syl112anc K HL W H X B Y B X ˙ Y ˙ W I X ˙ Y ˙ W = I X I Y ˙ W
32 1 2 latref K Lat W B W ˙ W
33 8 15 32 syl2anc K HL W H X B Y B X ˙ Y ˙ W W ˙ W
34 1 2 3 4 5 dihmeetbN K HL W H Y B W B W ˙ W I Y ˙ W = I Y I W
35 25 10 15 33 34 syl112anc K HL W H X B Y B X ˙ Y ˙ W I Y ˙ W = I Y I W
36 35 ineq2d K HL W H X B Y B X ˙ Y ˙ W I X I Y ˙ W = I X I Y I W
37 24 31 36 3eqtrd K HL W H X B Y B X ˙ Y ˙ W I X ˙ Y = I X I Y I W
38 inass I X I Y I W = I X I Y I W
39 37 38 eqtr4di K HL W H X B Y B X ˙ Y ˙ W I X ˙ Y = I X I Y I W