Metamath Proof Explorer


Theorem dia2dimlem2

Description: Lemma for dia2dim . Define a translation G whose trace is atom U . Part of proof of Lemma M in Crawley p. 121 line 4. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem2.l ˙ = K
dia2dimlem2.j ˙ = join K
dia2dimlem2.m ˙ = meet K
dia2dimlem2.a A = Atoms K
dia2dimlem2.h H = LHyp K
dia2dimlem2.t T = LTrn K W
dia2dimlem2.r R = trL K W
dia2dimlem2.q Q = P ˙ U ˙ F P ˙ V
dia2dimlem2.k φ K HL W H
dia2dimlem2.u φ U A U ˙ W
dia2dimlem2.v φ V A V ˙ W
dia2dimlem2.p φ P A ¬ P ˙ W
dia2dimlem2.f φ F T F P P
dia2dimlem2.rf φ R F ˙ U ˙ V
dia2dimlem2.rv φ R F V
dia2dimlem2.g φ G T
dia2dimlem2.gv φ G P = Q
Assertion dia2dimlem2 φ R G = U

Proof

Step Hyp Ref Expression
1 dia2dimlem2.l ˙ = K
2 dia2dimlem2.j ˙ = join K
3 dia2dimlem2.m ˙ = meet K
4 dia2dimlem2.a A = Atoms K
5 dia2dimlem2.h H = LHyp K
6 dia2dimlem2.t T = LTrn K W
7 dia2dimlem2.r R = trL K W
8 dia2dimlem2.q Q = P ˙ U ˙ F P ˙ V
9 dia2dimlem2.k φ K HL W H
10 dia2dimlem2.u φ U A U ˙ W
11 dia2dimlem2.v φ V A V ˙ W
12 dia2dimlem2.p φ P A ¬ P ˙ W
13 dia2dimlem2.f φ F T F P P
14 dia2dimlem2.rf φ R F ˙ U ˙ V
15 dia2dimlem2.rv φ R F V
16 dia2dimlem2.g φ G T
17 dia2dimlem2.gv φ G P = Q
18 9 simpld φ K HL
19 18 hllatd φ K Lat
20 12 simpld φ P A
21 eqid Base K = Base K
22 21 4 atbase P A P Base K
23 20 22 syl φ P Base K
24 10 simpld φ U A
25 21 4 atbase U A U Base K
26 24 25 syl φ U Base K
27 21 1 2 latlej2 K Lat P Base K U Base K U ˙ P ˙ U
28 19 23 26 27 syl3anc φ U ˙ P ˙ U
29 21 2 4 hlatjcl K HL P A U A P ˙ U Base K
30 18 20 24 29 syl3anc φ P ˙ U Base K
31 21 1 3 latleeqm2 K Lat U Base K P ˙ U Base K U ˙ P ˙ U P ˙ U ˙ U = U
32 19 26 30 31 syl3anc φ U ˙ P ˙ U P ˙ U ˙ U = U
33 28 32 mpbid φ P ˙ U ˙ U = U
34 1 4 5 6 7 trlat K HL W H P A ¬ P ˙ W F T F P P R F A
35 9 12 13 34 syl3anc φ R F A
36 11 simpld φ V A
37 1 2 4 hlatexch2 K HL R F A U A V A R F V R F ˙ U ˙ V U ˙ R F ˙ V
38 18 35 24 36 15 37 syl131anc φ R F ˙ U ˙ V U ˙ R F ˙ V
39 14 38 mpd φ U ˙ R F ˙ V
40 13 simpld φ F T
41 1 2 3 4 5 6 7 trlval2 K HL W H F T P A ¬ P ˙ W R F = P ˙ F P ˙ W
42 9 40 12 41 syl3anc φ R F = P ˙ F P ˙ W
43 42 oveq1d φ R F ˙ V = P ˙ F P ˙ W ˙ V
44 1 4 5 6 ltrnel K HL W H F T P A ¬ P ˙ W F P A ¬ F P ˙ W
45 9 40 12 44 syl3anc φ F P A ¬ F P ˙ W
46 45 simpld φ F P A
47 21 2 4 hlatjcl K HL P A F P A P ˙ F P Base K
48 18 20 46 47 syl3anc φ P ˙ F P Base K
49 9 simprd φ W H
50 21 5 lhpbase W H W Base K
51 49 50 syl φ W Base K
52 11 simprd φ V ˙ W
53 21 1 2 3 4 atmod4i1 K HL V A P ˙ F P Base K W Base K V ˙ W P ˙ F P ˙ W ˙ V = P ˙ F P ˙ V ˙ W
54 18 36 48 51 52 53 syl131anc φ P ˙ F P ˙ W ˙ V = P ˙ F P ˙ V ˙ W
55 2 4 hlatjass K HL P A F P A V A P ˙ F P ˙ V = P ˙ F P ˙ V
56 18 20 46 36 55 syl13anc φ P ˙ F P ˙ V = P ˙ F P ˙ V
57 56 oveq1d φ P ˙ F P ˙ V ˙ W = P ˙ F P ˙ V ˙ W
58 54 57 eqtrd φ P ˙ F P ˙ W ˙ V = P ˙ F P ˙ V ˙ W
59 43 58 eqtrd φ R F ˙ V = P ˙ F P ˙ V ˙ W
60 39 59 breqtrd φ U ˙ P ˙ F P ˙ V ˙ W
61 21 2 4 hlatjcl K HL F P A V A F P ˙ V Base K
62 18 46 36 61 syl3anc φ F P ˙ V Base K
63 21 2 latjcl K Lat P Base K F P ˙ V Base K P ˙ F P ˙ V Base K
64 19 23 62 63 syl3anc φ P ˙ F P ˙ V Base K
65 21 3 latmcl K Lat P ˙ F P ˙ V Base K W Base K P ˙ F P ˙ V ˙ W Base K
66 19 64 51 65 syl3anc φ P ˙ F P ˙ V ˙ W Base K
67 21 1 3 latmlem2 K Lat U Base K P ˙ F P ˙ V ˙ W Base K P ˙ U Base K U ˙ P ˙ F P ˙ V ˙ W P ˙ U ˙ U ˙ P ˙ U ˙ P ˙ F P ˙ V ˙ W
68 19 26 66 30 67 syl13anc φ U ˙ P ˙ F P ˙ V ˙ W P ˙ U ˙ U ˙ P ˙ U ˙ P ˙ F P ˙ V ˙ W
69 60 68 mpd φ P ˙ U ˙ U ˙ P ˙ U ˙ P ˙ F P ˙ V ˙ W
70 33 69 eqbrtrrd φ U ˙ P ˙ U ˙ P ˙ F P ˙ V ˙ W
71 1 2 3 4 5 6 7 trlval2 K HL W H G T P A ¬ P ˙ W R G = P ˙ G P ˙ W
72 9 16 12 71 syl3anc φ R G = P ˙ G P ˙ W
73 17 8 eqtrdi φ G P = P ˙ U ˙ F P ˙ V
74 73 oveq2d φ P ˙ G P = P ˙ P ˙ U ˙ F P ˙ V
75 74 oveq1d φ P ˙ G P ˙ W = P ˙ P ˙ U ˙ F P ˙ V ˙ W
76 1 2 4 hlatlej1 K HL P A U A P ˙ P ˙ U
77 18 20 24 76 syl3anc φ P ˙ P ˙ U
78 21 1 2 3 4 atmod3i1 K HL P A P ˙ U Base K F P ˙ V Base K P ˙ P ˙ U P ˙ P ˙ U ˙ F P ˙ V = P ˙ U ˙ P ˙ F P ˙ V
79 18 20 30 62 77 78 syl131anc φ P ˙ P ˙ U ˙ F P ˙ V = P ˙ U ˙ P ˙ F P ˙ V
80 79 oveq1d φ P ˙ P ˙ U ˙ F P ˙ V ˙ W = P ˙ U ˙ P ˙ F P ˙ V ˙ W
81 hlol K HL K OL
82 18 81 syl φ K OL
83 21 3 latmassOLD K OL P ˙ U Base K P ˙ F P ˙ V Base K W Base K P ˙ U ˙ P ˙ F P ˙ V ˙ W = P ˙ U ˙ P ˙ F P ˙ V ˙ W
84 82 30 64 51 83 syl13anc φ P ˙ U ˙ P ˙ F P ˙ V ˙ W = P ˙ U ˙ P ˙ F P ˙ V ˙ W
85 80 84 eqtrd φ P ˙ P ˙ U ˙ F P ˙ V ˙ W = P ˙ U ˙ P ˙ F P ˙ V ˙ W
86 75 85 eqtrd φ P ˙ G P ˙ W = P ˙ U ˙ P ˙ F P ˙ V ˙ W
87 72 86 eqtrd φ R G = P ˙ U ˙ P ˙ F P ˙ V ˙ W
88 87 eqcomd φ P ˙ U ˙ P ˙ F P ˙ V ˙ W = R G
89 70 88 breqtrd φ U ˙ R G
90 hlatl K HL K AtLat
91 18 90 syl φ K AtLat
92 hlop K HL K OP
93 18 92 syl φ K OP
94 eqid 0. K = 0. K
95 eqid < K = < K
96 94 95 4 0ltat K OP U A 0. K < K U
97 93 24 96 syl2anc φ 0. K < K U
98 hlpos K HL K Poset
99 18 98 syl φ K Poset
100 21 94 op0cl K OP 0. K Base K
101 93 100 syl φ 0. K Base K
102 21 5 6 7 trlcl K HL W H G T R G Base K
103 9 16 102 syl2anc φ R G Base K
104 21 1 95 pltletr K Poset 0. K Base K U Base K R G Base K 0. K < K U U ˙ R G 0. K < K R G
105 99 101 26 103 104 syl13anc φ 0. K < K U U ˙ R G 0. K < K R G
106 97 89 105 mp2and φ 0. K < K R G
107 21 95 94 opltn0 K OP R G Base K 0. K < K R G R G 0. K
108 93 103 107 syl2anc φ 0. K < K R G R G 0. K
109 106 108 mpbid φ R G 0. K
110 109 neneqd φ ¬ R G = 0. K
111 94 4 5 6 7 trlator0 K HL W H G T R G A R G = 0. K
112 9 16 111 syl2anc φ R G A R G = 0. K
113 112 orcomd φ R G = 0. K R G A
114 113 ord φ ¬ R G = 0. K R G A
115 110 114 mpd φ R G A
116 1 4 atcmp K AtLat U A R G A U ˙ R G U = R G
117 91 24 115 116 syl3anc φ U ˙ R G U = R G
118 89 117 mpbid φ U = R G
119 118 eqcomd φ R G = U