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 36548
Description: Lemma for dalaw 36553. First part of dalawlem13 36550. (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 2795 . . . 4 (Base‘𝐾) = (Base‘𝐾)
2 dalawlem.l . . . 4 = (le‘𝐾)
3 simp11 1196 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ HL)
43hllatd 36031 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ Lat)
5 simp21 1199 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃𝐴)
6 simp22 1200 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄𝐴)
7 dalawlem.j . . . . . . 7 = (join‘𝐾)
8 dalawlem.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
91, 7, 8hlatjcl 36034 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
103, 5, 6, 9syl3anc 1364 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
11 simp31 1202 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆𝐴)
12 simp32 1203 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇𝐴)
131, 7, 8hlatjcl 36034 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
143, 11, 12, 13syl3anc 1364 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 𝑇) ∈ (Base‘𝐾))
15 dalawlem.m . . . . . 6 = (meet‘𝐾)
161, 15latmcl 17491 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
174, 10, 14, 16syl3anc 1364 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
18 simp23 1201 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅𝐴)
191, 7, 8hlatjcl 36034 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
203, 6, 18, 19syl3anc 1364 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑅) ∈ (Base‘𝐾))
211, 2, 15latmle1 17515 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
224, 10, 14, 21syl3anc 1364 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
23 simp12 1197 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑄 𝑅))
241, 8atbase 35956 . . . . . . 7 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
256, 24syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 ∈ (Base‘𝐾))
261, 8atbase 35956 . . . . . . 7 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
2718, 26syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 ∈ (Base‘𝐾))
281, 2, 7latlej1 17499 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑄 (𝑄 𝑅))
294, 25, 27, 28syl3anc 1364 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑅))
301, 8atbase 35956 . . . . . . 7 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
315, 30syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 ∈ (Base‘𝐾))
321, 2, 7latjle12 17501 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑃 (𝑄 𝑅) ∧ 𝑄 (𝑄 𝑅)) ↔ (𝑃 𝑄) (𝑄 𝑅)))
334, 31, 25, 20, 32syl13anc 1365 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑅) ∧ 𝑄 (𝑄 𝑅)) ↔ (𝑃 𝑄) (𝑄 𝑅)))
3423, 29, 33mpbi2and 708 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) (𝑄 𝑅))
351, 2, 4, 17, 10, 20, 22, 34lattrd 17497 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅))
361, 8atbase 35956 . . . . . . . 8 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
3712, 36syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 ∈ (Base‘𝐾))
381, 7latjcl 17490 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾))
394, 10, 37, 38syl3anc 1364 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾))
401, 15latmcl 17491 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ∈ (Base‘𝐾))
414, 39, 14, 40syl3anc 1364 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ∈ (Base‘𝐾))
421, 7, 8hlatjcl 36034 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑃𝐴) → (𝑅 𝑃) ∈ (Base‘𝐾))
433, 18, 5, 42syl3anc 1364 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑃) ∈ (Base‘𝐾))
44 simp33 1204 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈𝐴)
451, 7, 8hlatjcl 36034 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑆𝐴) → (𝑈 𝑆) ∈ (Base‘𝐾))
463, 44, 11, 45syl3anc 1364 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑆) ∈ (Base‘𝐾))
471, 15latmcl 17491 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
484, 43, 46, 47syl3anc 1364 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
491, 8atbase 35956 . . . . . . . 8 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
5044, 49syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 ∈ (Base‘𝐾))
511, 7latjcl 17490 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾))
524, 48, 50, 51syl3anc 1364 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾))
531, 7latjcl 17490 . . . . . 6 ((𝐾 ∈ Lat ∧ (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) ∈ (Base‘𝐾))
544, 52, 37, 53syl3anc 1364 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) ∈ (Base‘𝐾))
551, 2, 7latlej1 17499 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑇))
564, 10, 37, 55syl3anc 1364 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑇))
571, 2, 15latmlem1 17520 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾))) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑇) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇))))
584, 10, 39, 14, 57syl13anc 1365 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑇) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇))))
5956, 58mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
601, 2, 7latlej2 17500 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 ((𝑃 𝑄) 𝑇))
614, 10, 37, 60syl3anc 1364 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 ((𝑃 𝑄) 𝑇))
621, 2, 7, 15, 8atmod2i2 36529 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑆𝐴 ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) ∧ 𝑇 ((𝑃 𝑄) 𝑇)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) = (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
633, 11, 39, 37, 61, 62syl131anc 1376 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) = (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
641, 7, 8hlatjcl 36034 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → (𝑄 𝑇) ∈ (Base‘𝐾))
653, 6, 12, 64syl3anc 1364 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑇) ∈ (Base‘𝐾))
661, 7, 8hlatjcl 36034 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → (𝑃 𝑆) ∈ (Base‘𝐾))
673, 5, 11, 66syl3anc 1364 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
681, 15latmcom 17514 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
694, 65, 67, 68syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
70 simp13 1198 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈))
7169, 70eqbrtrd 4984 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈))
721, 15latmcl 17491 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
734, 65, 67, 72syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
741, 7, 8hlatjcl 36034 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → (𝑅 𝑈) ∈ (Base‘𝐾))
753, 18, 44, 74syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑈) ∈ (Base‘𝐾))
761, 2, 7latjlej2 17505 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑅 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈))))
774, 73, 75, 31, 76syl13anc 1365 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈))))
7871, 77mpd 15 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈)))
791, 8atbase 35956 . . . . . . . . . . . . 13 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
8011, 79syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ∈ (Base‘𝐾))
811, 2, 7latlej1 17499 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑃 (𝑃 𝑆))
824, 31, 80, 81syl3anc 1364 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑃 𝑆))
831, 2, 7, 15, 8atmod1i1 36524 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑆)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) = ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)))
843, 5, 65, 67, 82, 83syl131anc 1376 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) = ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)))
857, 8hlatjass 36037 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑅𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = (𝑃 (𝑅 𝑈)))
863, 5, 18, 44, 85syl13anc 1365 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = (𝑃 (𝑅 𝑈)))
877, 8hlatjcom 36035 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴) → (𝑃 𝑅) = (𝑅 𝑃))
883, 5, 18, 87syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑅) = (𝑅 𝑃))
8988oveq1d 7031 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = ((𝑅 𝑃) 𝑈))
9086, 89eqtr3d 2833 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑅 𝑈)) = ((𝑅 𝑃) 𝑈))
9178, 84, 903brtr3d 4993 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈))
921, 2, 7latlej2 17500 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 (𝑈 𝑆))
934, 50, 80, 92syl3anc 1364 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 (𝑈 𝑆))
941, 7latjcl 17490 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾))
954, 31, 65, 94syl3anc 1364 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾))
961, 15latmcl 17491 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾))
974, 95, 67, 96syl3anc 1364 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾))
981, 7latjcl 17490 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾))
994, 43, 50, 98syl3anc 1364 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾))
1001, 2, 15latmlem12 17522 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾)) ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾))) → ((((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈) ∧ 𝑆 (𝑈 𝑆)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆))))
1014, 97, 99, 80, 46, 100syl122anc 1372 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈) ∧ 𝑆 (𝑈 𝑆)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆))))
10291, 93, 101mp2and 695 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
103 hlol 36028 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
1043, 103syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ OL)
1051, 15latmassOLD 35896 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ ((𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) = ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)))
106104, 95, 67, 80, 105syl13anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) = ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)))
1077, 8hlatjass 36037 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑇𝐴)) → ((𝑃 𝑄) 𝑇) = (𝑃 (𝑄 𝑇)))
1083, 5, 6, 12, 107syl13anc 1365 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑇) = (𝑃 (𝑄 𝑇)))
109108eqcomd 2801 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑄 𝑇)) = ((𝑃 𝑄) 𝑇))
1101, 2, 7latlej2 17500 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 (𝑃 𝑆))
1114, 31, 80, 110syl3anc 1364 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 (𝑃 𝑆))
1121, 2, 15latleeqm2 17519 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → (𝑆 (𝑃 𝑆) ↔ ((𝑃 𝑆) 𝑆) = 𝑆))
1134, 80, 67, 112syl3anc 1364 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 (𝑃 𝑆) ↔ ((𝑃 𝑆) 𝑆) = 𝑆))
114111, 113mpbid 233 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑆) = 𝑆)
115109, 114oveq12d 7034 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)) = (((𝑃 𝑄) 𝑇) 𝑆))
116106, 115eqtr2d 2832 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) = (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆))
1171, 2, 7latlej1 17499 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑈 (𝑈 𝑆))
1184, 50, 80, 117syl3anc 1364 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑈 𝑆))
1191, 2, 7, 15, 8atmod4i1 36533 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑈 𝑆)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) = (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
1203, 44, 43, 46, 118, 119syl131anc 1376 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) = (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
121102, 116, 1203brtr4d 4994 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈))
1221, 15latmcl 17491 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾))
1234, 39, 80, 122syl3anc 1364 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾))
1241, 2, 7latjlej1 17504 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾) ∧ (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇)))
1254, 123, 52, 37, 124syl13anc 1365 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇)))
126121, 125mpd 15 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
12763, 126eqbrtrrd 4986 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
1281, 2, 4, 17, 41, 54, 59, 127lattrd 17497 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
1291, 7latj31 17538 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾))) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) = ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
1304, 48, 50, 37, 129syl13anc 1365 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) = ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
131128, 130breqtrd 4988 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
1321, 7, 8hlatjcl 36034 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
1333, 12, 44, 132syl3anc 1364 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑈) ∈ (Base‘𝐾))
1341, 7latjcl 17490 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) → ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
1354, 133, 48, 134syl3anc 1364 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
1361, 2, 15latlem12 17517 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))) → ((((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅) ∧ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))) ↔ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))))
1374, 17, 20, 135, 136syl13anc 1365 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅) ∧ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))) ↔ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))))
13835, 131, 137mpbi2and 708 . 2 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
1391, 2, 15latmle1 17515 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑅 𝑃))
1404, 43, 46, 139syl3anc 1364 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑅 𝑃))
1411, 2, 7latlej2 17500 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑅 (𝑄 𝑅))
1424, 25, 27, 141syl3anc 1364 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 (𝑄 𝑅))
1431, 2, 7latjle12 17501 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑅 (𝑄 𝑅) ∧ 𝑃 (𝑄 𝑅)) ↔ (𝑅 𝑃) (𝑄 𝑅)))
1444, 27, 31, 20, 143syl13anc 1365 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 (𝑄 𝑅) ∧ 𝑃 (𝑄 𝑅)) ↔ (𝑅 𝑃) (𝑄 𝑅)))
145142, 23, 144mpbi2and 708 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑃) (𝑄 𝑅))
1461, 2, 4, 48, 43, 20, 140, 145lattrd 17497 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑄 𝑅))
1471, 2, 7, 15, 8llnmod2i2 36530 . . 3 (((𝐾 ∈ HL ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) ∧ (𝑇𝐴𝑈𝐴) ∧ ((𝑅 𝑃) (𝑈 𝑆)) (𝑄 𝑅)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) = ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
1483, 20, 48, 12, 44, 146, 147syl321anc 1385 . 2 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) = ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
149138, 148breqtrrd 4990 1 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1080   = wceq 1522  wcel 2081   class class class wbr 4962  cfv 6225  (class class class)co 7016  Basecbs 16312  lecple 16401  joincjn 17383  meetcmee 17384  Latclat 17484  OLcol 35841  Atomscatm 35930  HLchlt 36017
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-1st 7545  df-2nd 7546  df-proset 17367  df-poset 17385  df-plt 17397  df-lub 17413  df-glb 17414  df-join 17415  df-meet 17416  df-p0 17478  df-lat 17485  df-clat 17547  df-oposet 35843  df-ol 35845  df-oml 35846  df-covers 35933  df-ats 35934  df-atl 35965  df-cvlat 35989  df-hlat 36018  df-psubsp 36170  df-pmap 36171  df-padd 36463
This theorem is referenced by:  dalawlem13  36550
  Copyright terms: Public domain W3C validator