# Metamath Proof Explorer

## Theorem dalawlem6

Description: Lemma for dalaw . First piece of dalawlem8 . (Contributed by NM, 6-Oct-2012)

Ref Expression
Hypotheses dalawlem.l
dalawlem.j
dalawlem.m
dalawlem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion dalawlem6

### Proof

Step Hyp Ref Expression
1 dalawlem.l
2 dalawlem.j
3 dalawlem.m
4 dalawlem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
6 simp11
7 6 hllatd
8 simp21
9 simp22
10 5 2 4 hlatjcl
11 6 8 9 10 syl3anc
12 simp32
13 5 4 atbase ${⊢}{T}\in {A}\to {T}\in {\mathrm{Base}}_{{K}}$
14 12 13 syl
15 5 2 latjcl
16 7 11 14 15 syl3anc
17 simp31
18 5 4 atbase ${⊢}{S}\in {A}\to {S}\in {\mathrm{Base}}_{{K}}$
19 17 18 syl
20 5 3 latmcl
21 7 16 19 20 syl3anc
22 simp23
23 5 2 4 hlatjcl
24 6 9 22 23 syl3anc
25 simp33
26 5 4 atbase ${⊢}{U}\in {A}\to {U}\in {\mathrm{Base}}_{{K}}$
27 25 26 syl
28 5 3 latmcl
29 7 24 27 28 syl3anc
30 5 2 4 hlatjcl
31 6 22 8 30 syl3anc
32 5 2 4 hlatjcl
33 6 25 17 32 syl3anc
34 5 3 latmcl
35 7 31 33 34 syl3anc
36 5 2 latjcl
37 7 29 35 36 syl3anc
38 5 2 4 hlatjcl
39 6 12 25 38 syl3anc
40 5 3 latmcl
41 7 24 39 40 syl3anc
42 5 2 latjcl
43 7 41 35 42 syl3anc
44 5 4 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
45 8 44 syl
46 5 2 4 hlatjcl
47 6 8 17 46 syl3anc
48 5 2 4 hlatjcl
49 6 9 12 48 syl3anc
50 5 3 latmcl
51 7 24 49 50 syl3anc
52 5 3 latmcl
53 7 47 51 52 syl3anc
54 5 2 latjcl
55 7 45 53 54 syl3anc
56 5 4 atbase ${⊢}{R}\in {A}\to {R}\in {\mathrm{Base}}_{{K}}$
57 22 56 syl
58 5 2 latjcl
59 7 57 29 58 syl3anc
60 5 2 latjcl
61 7 45 59 60 syl3anc
62 5 1 2 3 latmlej22
63 7 19 16 45 62 syl13anc
64 5 3 latmcl
65 7 49 47 64 syl3anc
66 5 2 latjcl
67 7 45 65 66 syl3anc
68 5 2 latjcl
69 7 45 51 68 syl3anc
70 1 2 4 hlatlej2
71 6 8 17 70 syl3anc
72 5 2 latjcl
73 7 45 49 72 syl3anc
74 5 1 3 latmlem2
75 7 19 47 73 74 syl13anc
76 71 75 mpd
77 2 4 hlatjass
78 6 8 9 12 77 syl13anc
79 78 oveq1d
80 1 2 4 hlatlej1
81 6 8 17 80 syl3anc
82 5 1 2 3 4 atmod1i1
83 6 8 49 47 81 82 syl131anc
84 76 79 83 3brtr4d
85 5 3 latmcom
86 7 49 47 85 syl3anc
87 simp12
88 86 87 eqbrtrd
89 5 1 3 latmle1
90 7 49 47 89 syl3anc
91 5 1 3 latlem12
92 7 65 24 49 91 syl13anc
93 88 90 92 mpbi2and
94 5 1 2 latjlej2
95 7 65 51 45 94 syl13anc
96 93 95 mpd
97 5 1 7 21 67 69 84 96 lattrd
98 5 1 3 latlem12
99 7 21 47 69 98 syl13anc
100 63 97 99 mpbi2and
101 5 1 2 3 4 atmod3i1
102 6 8 47 51 81 101 syl131anc
103 100 102 breqtrrd
104 simp13
105 5 3 latmcl
106 7 47 49 105 syl3anc
107 5 2 4 hlatjcl
108 6 22 25 107 syl3anc
109 5 1 3 latmlem2
110 7 106 108 24 109 syl13anc
111 104 110 mpd
112 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
113 6 112 syl
114 5 3 latm12
115 113 47 24 49 114 syl13anc
116 1 2 4 hlatlej2
117 6 9 22 116 syl3anc
118 5 1 2 3 4 atmod3i1
119 6 22 24 27 117 118 syl131anc
120 111 115 119 3brtr4d
121 5 1 2 latjlej2
122 7 53 59 45 121 syl13anc
123 120 122 mpd
124 5 1 7 21 55 61 103 123 lattrd
125 5 2 latj13
126 7 45 57 29 125 syl13anc
127 124 126 breqtrd
128 5 1 2 3 latmlej22
129 7 19 16 27 128 syl13anc
130 5 2 latjcl
131 7 29 31 130 syl3anc
132 5 1 3 latlem12
133 7 21 131 33 132 syl13anc
134 127 129 133 mpbi2and
135 5 1 2 3 latmlej21
136 7 27 24 19 135 syl13anc
137 5 1 2 3 4 atmod1i1m
138 6 25 24 31 33 136 137 syl231anc
139 134 138 breqtrrd
140 1 2 4 hlatlej2
141 6 12 25 140 syl3anc
142 5 1 3 latmlem2
143 7 27 39 24 142 syl13anc
144 141 143 mpd
145 5 1 2 latjlej1
146 7 29 41 35 145 syl13anc
147 144 146 mpd
148 5 1 7 21 37 43 139 147 lattrd