Metamath Proof Explorer


Theorem dihmeetlem6

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014)

Ref Expression
Hypotheses dihmeetlem6.b B = Base K
dihmeetlem6.l ˙ = K
dihmeetlem6.h H = LHyp K
dihmeetlem6.j ˙ = join K
dihmeetlem6.m ˙ = meet K
dihmeetlem6.a A = Atoms K
Assertion dihmeetlem6 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X ¬ X ˙ Y ˙ Q ˙ W

Proof

Step Hyp Ref Expression
1 dihmeetlem6.b B = Base K
2 dihmeetlem6.l ˙ = K
3 dihmeetlem6.h H = LHyp K
4 dihmeetlem6.j ˙ = join K
5 dihmeetlem6.m ˙ = meet K
6 dihmeetlem6.a A = Atoms K
7 simprlr K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X ¬ Q ˙ W
8 simpl1l K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X K HL
9 8 hllatd K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X K Lat
10 simpl2 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X B
11 simpl3 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X Y B
12 1 5 latmcl K Lat X B Y B X ˙ Y B
13 9 10 11 12 syl3anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y B
14 simprll K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X Q A
15 1 6 atbase Q A Q B
16 14 15 syl K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X Q B
17 simpl1r K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X W H
18 1 3 lhpbase W H W B
19 17 18 syl K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X W B
20 1 2 4 latjle12 K Lat X ˙ Y B Q B W B X ˙ Y ˙ W Q ˙ W X ˙ Y ˙ Q ˙ W
21 9 13 16 19 20 syl13anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W Q ˙ W X ˙ Y ˙ Q ˙ W
22 simpr X ˙ Y ˙ W Q ˙ W Q ˙ W
23 21 22 syl6bir K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ Q ˙ W Q ˙ W
24 7 23 mtod K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X ¬ X ˙ Y ˙ Q ˙ W
25 simprr K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X Q ˙ X
26 1 2 4 5 6 dihmeetlem5 K HL X B Y B Q A Q ˙ X X ˙ Y ˙ Q = X ˙ Y ˙ Q
27 8 10 11 14 25 26 syl32anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ Q = X ˙ Y ˙ Q
28 27 breq1d K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ Q ˙ W X ˙ Y ˙ Q ˙ W
29 24 28 mtbird K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X ¬ X ˙ Y ˙ Q ˙ W