Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dalawlem11 Structured version   Visualization version   GIF version

Theorem dalawlem11 39486
Description: Lemma for dalaw 39491. First part of dalawlem13 39488. (Contributed by NM, 17-Sep-2012.)
Hypotheses
Ref Expression
dalawlem.l = (le‘𝐾)
dalawlem.j = (join‘𝐾)
dalawlem.m = (meet‘𝐾)
dalawlem.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
dalawlem11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))

Proof of Theorem dalawlem11
StepHypRef Expression
1 eqid 2725 . . . 4 (Base‘𝐾) = (Base‘𝐾)
2 dalawlem.l . . . 4 = (le‘𝐾)
3 simp11 1200 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ HL)
43hllatd 38968 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ Lat)
5 simp21 1203 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃𝐴)
6 simp22 1204 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄𝐴)
7 dalawlem.j . . . . . . 7 = (join‘𝐾)
8 dalawlem.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
91, 7, 8hlatjcl 38971 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
103, 5, 6, 9syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
11 simp31 1206 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆𝐴)
12 simp32 1207 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇𝐴)
131, 7, 8hlatjcl 38971 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
143, 11, 12, 13syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 𝑇) ∈ (Base‘𝐾))
15 dalawlem.m . . . . . 6 = (meet‘𝐾)
161, 15latmcl 18440 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
174, 10, 14, 16syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
18 simp23 1205 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅𝐴)
191, 7, 8hlatjcl 38971 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
203, 6, 18, 19syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑅) ∈ (Base‘𝐾))
211, 2, 15latmle1 18464 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
224, 10, 14, 21syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
23 simp12 1201 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑄 𝑅))
241, 8atbase 38893 . . . . . . 7 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
256, 24syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 ∈ (Base‘𝐾))
261, 8atbase 38893 . . . . . . 7 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
2718, 26syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 ∈ (Base‘𝐾))
281, 2, 7latlej1 18448 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑄 (𝑄 𝑅))
294, 25, 27, 28syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑅))
301, 8atbase 38893 . . . . . . 7 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
315, 30syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 ∈ (Base‘𝐾))
321, 2, 7latjle12 18450 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑃 (𝑄 𝑅) ∧ 𝑄 (𝑄 𝑅)) ↔ (𝑃 𝑄) (𝑄 𝑅)))
334, 31, 25, 20, 32syl13anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑅) ∧ 𝑄 (𝑄 𝑅)) ↔ (𝑃 𝑄) (𝑄 𝑅)))
3423, 29, 33mpbi2and 710 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) (𝑄 𝑅))
351, 2, 4, 17, 10, 20, 22, 34lattrd 18446 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅))
361, 8atbase 38893 . . . . . . . 8 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
3712, 36syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 ∈ (Base‘𝐾))
381, 7latjcl 18439 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾))
394, 10, 37, 38syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾))
401, 15latmcl 18440 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ∈ (Base‘𝐾))
414, 39, 14, 40syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ∈ (Base‘𝐾))
421, 7, 8hlatjcl 38971 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑃𝐴) → (𝑅 𝑃) ∈ (Base‘𝐾))
433, 18, 5, 42syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑃) ∈ (Base‘𝐾))
44 simp33 1208 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈𝐴)
451, 7, 8hlatjcl 38971 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑆𝐴) → (𝑈 𝑆) ∈ (Base‘𝐾))
463, 44, 11, 45syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑆) ∈ (Base‘𝐾))
471, 15latmcl 18440 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
484, 43, 46, 47syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
491, 8atbase 38893 . . . . . . . 8 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
5044, 49syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 ∈ (Base‘𝐾))
511, 7latjcl 18439 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾))
524, 48, 50, 51syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾))
531, 7latjcl 18439 . . . . . 6 ((𝐾 ∈ Lat ∧ (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) ∈ (Base‘𝐾))
544, 52, 37, 53syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) ∈ (Base‘𝐾))
551, 2, 7latlej1 18448 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑇))
564, 10, 37, 55syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑇))
571, 2, 15latmlem1 18469 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾))) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑇) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇))))
584, 10, 39, 14, 57syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑇) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇))))
5956, 58mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
601, 2, 7latlej2 18449 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 ((𝑃 𝑄) 𝑇))
614, 10, 37, 60syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 ((𝑃 𝑄) 𝑇))
621, 2, 7, 15, 8atmod2i2 39467 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑆𝐴 ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) ∧ 𝑇 ((𝑃 𝑄) 𝑇)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) = (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
633, 11, 39, 37, 61, 62syl131anc 1380 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) = (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
641, 7, 8hlatjcl 38971 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → (𝑄 𝑇) ∈ (Base‘𝐾))
653, 6, 12, 64syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑇) ∈ (Base‘𝐾))
661, 7, 8hlatjcl 38971 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → (𝑃 𝑆) ∈ (Base‘𝐾))
673, 5, 11, 66syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
681, 15latmcom 18463 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
694, 65, 67, 68syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
70 simp13 1202 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈))
7169, 70eqbrtrd 5171 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈))
721, 15latmcl 18440 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
734, 65, 67, 72syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
741, 7, 8hlatjcl 38971 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → (𝑅 𝑈) ∈ (Base‘𝐾))
753, 18, 44, 74syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑈) ∈ (Base‘𝐾))
761, 2, 7latjlej2 18454 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑅 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈))))
774, 73, 75, 31, 76syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈))))
7871, 77mpd 15 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈)))
791, 8atbase 38893 . . . . . . . . . . . . 13 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
8011, 79syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ∈ (Base‘𝐾))
811, 2, 7latlej1 18448 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑃 (𝑃 𝑆))
824, 31, 80, 81syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑃 𝑆))
831, 2, 7, 15, 8atmod1i1 39462 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑆)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) = ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)))
843, 5, 65, 67, 82, 83syl131anc 1380 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) = ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)))
857, 8hlatjass 38974 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑅𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = (𝑃 (𝑅 𝑈)))
863, 5, 18, 44, 85syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = (𝑃 (𝑅 𝑈)))
877, 8hlatjcom 38972 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴) → (𝑃 𝑅) = (𝑅 𝑃))
883, 5, 18, 87syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑅) = (𝑅 𝑃))
8988oveq1d 7434 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = ((𝑅 𝑃) 𝑈))
9086, 89eqtr3d 2767 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑅 𝑈)) = ((𝑅 𝑃) 𝑈))
9178, 84, 903brtr3d 5180 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈))
921, 2, 7latlej2 18449 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 (𝑈 𝑆))
934, 50, 80, 92syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 (𝑈 𝑆))
941, 7latjcl 18439 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾))
954, 31, 65, 94syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾))
961, 15latmcl 18440 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾))
974, 95, 67, 96syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾))
981, 7latjcl 18439 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾))
994, 43, 50, 98syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾))
1001, 2, 15latmlem12 18471 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾)) ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾))) → ((((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈) ∧ 𝑆 (𝑈 𝑆)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆))))
1014, 97, 99, 80, 46, 100syl122anc 1376 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈) ∧ 𝑆 (𝑈 𝑆)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆))))
10291, 93, 101mp2and 697 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
103 hlol 38965 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
1043, 103syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ OL)
1051, 15latmassOLD 38833 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ ((𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) = ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)))
106104, 95, 67, 80, 105syl13anc 1369 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) = ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)))
1077, 8hlatjass 38974 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑇𝐴)) → ((𝑃 𝑄) 𝑇) = (𝑃 (𝑄 𝑇)))
1083, 5, 6, 12, 107syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑇) = (𝑃 (𝑄 𝑇)))
109108eqcomd 2731 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑄 𝑇)) = ((𝑃 𝑄) 𝑇))
1101, 2, 7latlej2 18449 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 (𝑃 𝑆))
1114, 31, 80, 110syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 (𝑃 𝑆))
1121, 2, 15latleeqm2 18468 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → (𝑆 (𝑃 𝑆) ↔ ((𝑃 𝑆) 𝑆) = 𝑆))
1134, 80, 67, 112syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 (𝑃 𝑆) ↔ ((𝑃 𝑆) 𝑆) = 𝑆))
114111, 113mpbid 231 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑆) = 𝑆)
115109, 114oveq12d 7437 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)) = (((𝑃 𝑄) 𝑇) 𝑆))
116106, 115eqtr2d 2766 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) = (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆))
1171, 2, 7latlej1 18448 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑈 (𝑈 𝑆))
1184, 50, 80, 117syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑈 𝑆))
1191, 2, 7, 15, 8atmod4i1 39471 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑈 𝑆)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) = (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
1203, 44, 43, 46, 118, 119syl131anc 1380 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) = (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
121102, 116, 1203brtr4d 5181 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈))
1221, 15latmcl 18440 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾))
1234, 39, 80, 122syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾))
1241, 2, 7latjlej1 18453 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾) ∧ (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇)))
1254, 123, 52, 37, 124syl13anc 1369 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇)))
126121, 125mpd 15 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
12763, 126eqbrtrrd 5173 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
1281, 2, 4, 17, 41, 54, 59, 127lattrd 18446 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
1291, 7latj31 18487 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾))) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) = ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
1304, 48, 50, 37, 129syl13anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) = ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
131128, 130breqtrd 5175 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
1321, 7, 8hlatjcl 38971 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
1333, 12, 44, 132syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑈) ∈ (Base‘𝐾))
1341, 7latjcl 18439 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) → ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
1354, 133, 48, 134syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
1361, 2, 15latlem12 18466 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))) → ((((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅) ∧ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))) ↔ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))))
1374, 17, 20, 135, 136syl13anc 1369 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅) ∧ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))) ↔ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))))
13835, 131, 137mpbi2and 710 . 2 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
1391, 2, 15latmle1 18464 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑅 𝑃))
1404, 43, 46, 139syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑅 𝑃))
1411, 2, 7latlej2 18449 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑅 (𝑄 𝑅))
1424, 25, 27, 141syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 (𝑄 𝑅))
1431, 2, 7latjle12 18450 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑅 (𝑄 𝑅) ∧ 𝑃 (𝑄 𝑅)) ↔ (𝑅 𝑃) (𝑄 𝑅)))
1444, 27, 31, 20, 143syl13anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 (𝑄 𝑅) ∧ 𝑃 (𝑄 𝑅)) ↔ (𝑅 𝑃) (𝑄 𝑅)))
145142, 23, 144mpbi2and 710 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑃) (𝑄 𝑅))
1461, 2, 4, 48, 43, 20, 140, 145lattrd 18446 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑄 𝑅))
1471, 2, 7, 15, 8llnmod2i2 39468 . . 3 (((𝐾 ∈ HL ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) ∧ (𝑇𝐴𝑈𝐴) ∧ ((𝑅 𝑃) (𝑈 𝑆)) (𝑄 𝑅)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) = ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
1483, 20, 48, 12, 44, 146, 147syl321anc 1389 . 2 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) = ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
149138, 148breqtrrd 5177 1 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098   class class class wbr 5149  cfv 6549  (class class class)co 7419  Basecbs 17188  lecple 17248  joincjn 18311  meetcmee 18312  Latclat 18431  OLcol 38778  Atomscatm 38867  HLchlt 38954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7994  df-2nd 7995  df-proset 18295  df-poset 18313  df-plt 18330  df-lub 18346  df-glb 18347  df-join 18348  df-meet 18349  df-p0 18425  df-lat 18432  df-clat 18499  df-oposet 38780  df-ol 38782  df-oml 38783  df-covers 38870  df-ats 38871  df-atl 38902  df-cvlat 38926  df-hlat 38955  df-psubsp 39108  df-pmap 39109  df-padd 39401
This theorem is referenced by:  dalawlem13  39488
  Copyright terms: Public domain W3C validator