Metamath Proof Explorer


Theorem cdleme30a

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Feb-2013)

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

Proof

Step Hyp Ref Expression
1 cdleme30.b B = Base K
2 cdleme30.l ˙ = K
3 cdleme30.j ˙ = join K
4 cdleme30.m ˙ = meet K
5 cdleme30.a A = Atoms K
6 cdleme30.h H = LHyp K
7 simp1l K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y K HL
8 7 hllatd K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y K Lat
9 simp21 K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s A
10 1 5 atbase s A s B
11 9 10 syl K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s B
12 simp23 K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y Y B
13 simp1r K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y W H
14 1 6 lhpbase W H W B
15 13 14 syl K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y W B
16 1 4 latmcl K Lat Y B W B Y ˙ W B
17 8 12 15 16 syl3anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y Y ˙ W B
18 simp22l K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X B
19 1 3 latjass K Lat s B Y ˙ W B X B s ˙ Y ˙ W ˙ X = s ˙ Y ˙ W ˙ X
20 8 11 17 18 19 syl13anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W ˙ X = s ˙ Y ˙ W ˙ X
21 simp3l K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ X ˙ W = X
22 simp3r K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X ˙ Y
23 1 2 4 latmlem1 K Lat X B Y B W B X ˙ Y X ˙ W ˙ Y ˙ W
24 8 18 12 15 23 syl13anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X ˙ Y X ˙ W ˙ Y ˙ W
25 22 24 mpd K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X ˙ W ˙ Y ˙ W
26 1 4 latmcl K Lat X B W B X ˙ W B
27 8 18 15 26 syl3anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X ˙ W B
28 1 2 3 latjlej2 K Lat X ˙ W B Y ˙ W B s B X ˙ W ˙ Y ˙ W s ˙ X ˙ W ˙ s ˙ Y ˙ W
29 8 27 17 11 28 syl13anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X ˙ W ˙ Y ˙ W s ˙ X ˙ W ˙ s ˙ Y ˙ W
30 25 29 mpd K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ X ˙ W ˙ s ˙ Y ˙ W
31 21 30 eqbrtrrd K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X ˙ s ˙ Y ˙ W
32 1 3 latjcl K Lat s B Y ˙ W B s ˙ Y ˙ W B
33 8 11 17 32 syl3anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W B
34 1 2 3 latleeqj2 K Lat X B s ˙ Y ˙ W B X ˙ s ˙ Y ˙ W s ˙ Y ˙ W ˙ X = s ˙ Y ˙ W
35 8 18 33 34 syl3anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X ˙ s ˙ Y ˙ W s ˙ Y ˙ W ˙ X = s ˙ Y ˙ W
36 31 35 mpbid K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W ˙ X = s ˙ Y ˙ W
37 simp1 K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y K HL W H
38 1 2 3 4 6 lhpmod2i2 K HL W H Y B X B X ˙ Y Y ˙ W ˙ X = Y ˙ W ˙ X
39 37 12 18 22 38 syl121anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y Y ˙ W ˙ X = Y ˙ W ˙ X
40 39 oveq2d K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W ˙ X = s ˙ Y ˙ W ˙ X
41 simp22 K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y X B ¬ X ˙ W
42 eqid 1. K = 1. K
43 1 2 3 42 6 lhpj1 K HL W H X B ¬ X ˙ W W ˙ X = 1. K
44 37 41 43 syl2anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y W ˙ X = 1. K
45 44 oveq2d K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y Y ˙ W ˙ X = Y ˙ 1. K
46 hlol K HL K OL
47 7 46 syl K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y K OL
48 1 4 42 olm11 K OL Y B Y ˙ 1. K = Y
49 47 12 48 syl2anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y Y ˙ 1. K = Y
50 45 49 eqtrd K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y Y ˙ W ˙ X = Y
51 50 oveq2d K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W ˙ X = s ˙ Y
52 1 2 3 latlej1 K Lat s B X ˙ W B s ˙ s ˙ X ˙ W
53 8 11 27 52 syl3anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ s ˙ X ˙ W
54 53 21 breqtrd K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ X
55 1 2 8 11 18 12 54 22 lattrd K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y
56 1 2 3 latleeqj1 K Lat s B Y B s ˙ Y s ˙ Y = Y
57 8 11 12 56 syl3anc K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y s ˙ Y = Y
58 55 57 mpbid K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y = Y
59 40 51 58 3eqtrd K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W ˙ X = Y
60 20 36 59 3eqtr3d K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W = Y