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

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

Proof of Theorem dalawlem12
StepHypRef Expression
1 eqid 2798 . . . 4 (Base‘𝐾) = (Base‘𝐾)
2 dalawlem.l . . . 4 = (le‘𝐾)
3 simp11 1200 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ HL)
43hllatd 36660 . . . 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 36663 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
103, 5, 6, 9syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
11 simp31 1206 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆𝐴)
12 simp32 1207 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇𝐴)
131, 7, 8hlatjcl 36663 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
143, 11, 12, 13syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 𝑇) ∈ (Base‘𝐾))
15 dalawlem.m . . . . . 6 = (meet‘𝐾)
161, 15latmcl 17654 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
174, 10, 14, 16syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
181, 8atbase 36585 . . . . . . . 8 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
1911, 18syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ∈ (Base‘𝐾))
201, 7latjcl 17653 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾))
214, 10, 19, 20syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾))
221, 8atbase 36585 . . . . . . 7 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
2312, 22syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 ∈ (Base‘𝐾))
241, 15latmcl 17654 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑆) 𝑇) ∈ (Base‘𝐾))
254, 21, 23, 24syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑆) 𝑇) ∈ (Base‘𝐾))
261, 7latjcl 17653 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) 𝑆) 𝑇) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) ∈ (Base‘𝐾))
274, 25, 19, 26syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) ∈ (Base‘𝐾))
281, 8atbase 36585 . . . . . . 7 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
296, 28syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 ∈ (Base‘𝐾))
30 simp33 1208 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈𝐴)
311, 7, 8hlatjcl 36663 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
323, 12, 30, 31syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑈) ∈ (Base‘𝐾))
331, 15latmcl 17654 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾)) → (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾))
344, 29, 32, 33syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾))
351, 7, 8hlatjcl 36663 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑆𝐴) → (𝑈 𝑆) ∈ (Base‘𝐾))
363, 30, 11, 35syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑆) ∈ (Base‘𝐾))
371, 7latjcl 17653 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∈ (Base‘𝐾))
384, 34, 36, 37syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∈ (Base‘𝐾))
391, 2, 7latlej1 17662 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑆))
404, 10, 19, 39syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑆))
411, 7, 8hlatjcl 36663 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑆𝐴) → (𝑇 𝑆) ∈ (Base‘𝐾))
423, 12, 11, 41syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑆) ∈ (Base‘𝐾))
431, 2, 15latmlem1 17683 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾) ∧ (𝑇 𝑆) ∈ (Base‘𝐾))) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑆) → ((𝑃 𝑄) (𝑇 𝑆)) (((𝑃 𝑄) 𝑆) (𝑇 𝑆))))
444, 10, 21, 42, 43syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑆) → ((𝑃 𝑄) (𝑇 𝑆)) (((𝑃 𝑄) 𝑆) (𝑇 𝑆))))
4540, 44mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑇 𝑆)) (((𝑃 𝑄) 𝑆) (𝑇 𝑆)))
467, 8hlatjcom 36664 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) = (𝑇 𝑆))
473, 11, 12, 46syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 𝑇) = (𝑇 𝑆))
4847oveq2d 7151 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) = ((𝑃 𝑄) (𝑇 𝑆)))
491, 2, 7latlej2 17663 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 ((𝑃 𝑄) 𝑆))
504, 10, 19, 49syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ((𝑃 𝑄) 𝑆))
511, 2, 7, 15, 8atmod2i2 37158 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑇𝐴 ∧ ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) ∧ 𝑆 ((𝑃 𝑄) 𝑆)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) = (((𝑃 𝑄) 𝑆) (𝑇 𝑆)))
523, 12, 21, 19, 50, 51syl131anc 1380 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) = (((𝑃 𝑄) 𝑆) (𝑇 𝑆)))
5345, 48, 523brtr4d 5062 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆))
54 hlol 36657 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
553, 54syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ OL)
561, 7, 8hlatjcl 36663 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → (𝑃 𝑆) ∈ (Base‘𝐾))
573, 5, 11, 56syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
581, 7latjcl 17653 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → (𝑄 (𝑃 𝑆)) ∈ (Base‘𝐾))
594, 29, 57, 58syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑃 𝑆)) ∈ (Base‘𝐾))
601, 7, 8hlatjcl 36663 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → (𝑄 𝑇) ∈ (Base‘𝐾))
613, 6, 12, 60syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑇) ∈ (Base‘𝐾))
621, 15latmassOLD 36525 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ ((𝑄 (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾))) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) = ((𝑄 (𝑃 𝑆)) ((𝑄 𝑇) 𝑇)))
6355, 59, 61, 23, 62syl13anc 1369 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) = ((𝑄 (𝑃 𝑆)) ((𝑄 𝑇) 𝑇)))
647, 8hlatjass 36666 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → ((𝑃 𝑄) 𝑆) = (𝑃 (𝑄 𝑆)))
653, 5, 6, 11, 64syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑆) = (𝑃 (𝑄 𝑆)))
667, 8hlatj12 36667 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → (𝑃 (𝑄 𝑆)) = (𝑄 (𝑃 𝑆)))
673, 5, 6, 11, 66syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑄 𝑆)) = (𝑄 (𝑃 𝑆)))
6865, 67eqtr2d 2834 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑃 𝑆)) = ((𝑃 𝑄) 𝑆))
692, 7, 8hlatlej2 36672 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → 𝑇 (𝑄 𝑇))
703, 6, 12, 69syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 (𝑄 𝑇))
711, 2, 15latleeqm2 17682 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → (𝑇 (𝑄 𝑇) ↔ ((𝑄 𝑇) 𝑇) = 𝑇))
724, 23, 61, 71syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 (𝑄 𝑇) ↔ ((𝑄 𝑇) 𝑇) = 𝑇))
7370, 72mpbid 235 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) 𝑇) = 𝑇)
7468, 73oveq12d 7153 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑃 𝑆)) ((𝑄 𝑇) 𝑇)) = (((𝑃 𝑄) 𝑆) 𝑇))
7563, 74eqtr2d 2834 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑆) 𝑇) = (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇))
762, 7, 8hlatlej1 36671 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → 𝑄 (𝑄 𝑇))
773, 6, 12, 76syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑇))
781, 2, 7, 15, 8atmod1i1 37153 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑄𝐴 ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) ∧ 𝑄 (𝑄 𝑇)) → (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) = ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)))
793, 6, 57, 61, 77, 78syl131anc 1380 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) = ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)))
802, 7, 8hlatlej2 36672 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑄𝐴) → 𝑄 (𝑈 𝑄))
813, 30, 6, 80syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑈 𝑄))
82 simp13 1202 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈))
83 simp12 1201 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 = 𝑅)
8483oveq1d 7150 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑈) = (𝑅 𝑈))
857, 8hlatjcom 36664 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑈𝐴) → (𝑄 𝑈) = (𝑈 𝑄))
863, 6, 30, 85syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑈) = (𝑈 𝑄))
8784, 86eqtr3d 2835 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑈) = (𝑈 𝑄))
8882, 87breqtrd 5056 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑈 𝑄))
891, 15latmcl 17654 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾))
904, 57, 61, 89syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾))
911, 7, 8hlatjcl 36663 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑄𝐴) → (𝑈 𝑄) ∈ (Base‘𝐾))
923, 30, 6, 91syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑄) ∈ (Base‘𝐾))
931, 2, 7latjle12 17664 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑈 𝑄) ∈ (Base‘𝐾))) → ((𝑄 (𝑈 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑈 𝑄)) ↔ (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) (𝑈 𝑄)))
944, 29, 90, 92, 93syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑈 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑈 𝑄)) ↔ (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) (𝑈 𝑄)))
9581, 88, 94mpbi2and 711 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) (𝑈 𝑄))
9679, 95eqbrtrrd 5054 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) (𝑈 𝑄))
972, 7, 8hlatlej1 36671 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → 𝑇 (𝑇 𝑈))
983, 12, 30, 97syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 (𝑇 𝑈))
991, 15latmcl 17654 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑄 (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) ∈ (Base‘𝐾))
1004, 59, 61, 99syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) ∈ (Base‘𝐾))
1011, 2, 15latmlem12 17685 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑈 𝑄) ∈ (Base‘𝐾)) ∧ (𝑇 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾))) → ((((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) (𝑈 𝑄) ∧ 𝑇 (𝑇 𝑈)) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) ((𝑈 𝑄) (𝑇 𝑈))))
1024, 100, 92, 23, 32, 101syl122anc 1376 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) (𝑈 𝑄) ∧ 𝑇 (𝑇 𝑈)) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) ((𝑈 𝑄) (𝑇 𝑈))))
10396, 98, 102mp2and 698 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) ((𝑈 𝑄) (𝑇 𝑈)))
10475, 103eqbrtrd 5052 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑆) 𝑇) ((𝑈 𝑄) (𝑇 𝑈)))
1052, 7, 8hlatlej2 36672 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → 𝑈 (𝑇 𝑈))
1063, 12, 30, 105syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑇 𝑈))
1071, 2, 7, 15, 8atmod1i1 37153 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑄 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑇 𝑈)) → (𝑈 (𝑄 (𝑇 𝑈))) = ((𝑈 𝑄) (𝑇 𝑈)))
1083, 30, 29, 32, 106, 107syl131anc 1380 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 (𝑄 (𝑇 𝑈))) = ((𝑈 𝑄) (𝑇 𝑈)))
1091, 8atbase 36585 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
11030, 109syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 ∈ (Base‘𝐾))
1111, 7latjcom 17661 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾)) → (𝑈 (𝑄 (𝑇 𝑈))) = ((𝑄 (𝑇 𝑈)) 𝑈))
1124, 110, 34, 111syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 (𝑄 (𝑇 𝑈))) = ((𝑄 (𝑇 𝑈)) 𝑈))
113108, 112eqtr3d 2835 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑈 𝑄) (𝑇 𝑈)) = ((𝑄 (𝑇 𝑈)) 𝑈))
114104, 113breqtrd 5056 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑆) 𝑇) ((𝑄 (𝑇 𝑈)) 𝑈))
1151, 7latjcl 17653 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑄 (𝑇 𝑈)) 𝑈) ∈ (Base‘𝐾))
1164, 34, 110, 115syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑇 𝑈)) 𝑈) ∈ (Base‘𝐾))
1171, 2, 7latjlej1 17667 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((((𝑃 𝑄) 𝑆) 𝑇) ∈ (Base‘𝐾) ∧ ((𝑄 (𝑇 𝑈)) 𝑈) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑆) 𝑇) ((𝑄 (𝑇 𝑈)) 𝑈) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆)))
1184, 25, 116, 19, 117syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) ((𝑄 (𝑇 𝑈)) 𝑈) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆)))
119114, 118mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆))
1201, 7latjass 17697 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆) = ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)))
1214, 34, 110, 19, 120syl13anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆) = ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)))
122119, 121breqtrd 5056 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)))
1231, 2, 4, 17, 27, 38, 53, 122lattrd 17660 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)))
1241, 2, 15latmle1 17678 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
1254, 10, 14, 124syl3anc 1368 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
1261, 2, 15latlem12 17680 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾) ∧ ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → ((((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∧ ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄)) ↔ ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄))))
1274, 17, 38, 10, 126syl13anc 1369 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∧ ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄)) ↔ ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄))))
128123, 125, 127mpbi2and 711 . 2 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄)))
1291, 8atbase 36585 . . . . . 6 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1305, 129syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 ∈ (Base‘𝐾))
1311, 2, 7, 15latmlej12 17693 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (𝑄 (𝑇 𝑈)) (𝑃 𝑄))
1324, 29, 32, 130, 131syl13anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑇 𝑈)) (𝑃 𝑄))
1331, 2, 7, 15, 8llnmod1i2 37156 . . . 4 (((𝐾 ∈ HL ∧ (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) ∧ (𝑈𝐴𝑆𝐴) ∧ (𝑄 (𝑇 𝑈)) (𝑃 𝑄)) → ((𝑄 (𝑇 𝑈)) ((𝑈 𝑆) (𝑃 𝑄))) = (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄)))
1343, 34, 10, 30, 11, 132, 133syl321anc 1389 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑇 𝑈)) ((𝑈 𝑆) (𝑃 𝑄))) = (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄)))
1357, 8hlatjidm 36665 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑄𝐴) → (𝑄 𝑄) = 𝑄)
1363, 6, 135syl2anc 587 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑄) = 𝑄)
13783oveq2d 7151 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑄) = (𝑄 𝑅))
138136, 137eqtr3d 2835 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 = (𝑄 𝑅))
139138oveq1d 7150 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑇 𝑈)) = ((𝑄 𝑅) (𝑇 𝑈)))
1401, 15latmcom 17677 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑈 𝑆) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → ((𝑈 𝑆) (𝑃 𝑄)) = ((𝑃 𝑄) (𝑈 𝑆)))
1414, 36, 10, 140syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑈 𝑆) (𝑃 𝑄)) = ((𝑃 𝑄) (𝑈 𝑆)))
1427, 8hlatjcom 36664 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) = (𝑄 𝑃))
1433, 5, 6, 142syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) = (𝑄 𝑃))
14483oveq1d 7150 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑃) = (𝑅 𝑃))
145143, 144eqtrd 2833 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) = (𝑅 𝑃))
146145oveq1d 7150 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑈 𝑆)) = ((𝑅 𝑃) (𝑈 𝑆)))
147141, 146eqtrd 2833 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑈 𝑆) (𝑃 𝑄)) = ((𝑅 𝑃) (𝑈 𝑆)))
148139, 147oveq12d 7153 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑇 𝑈)) ((𝑈 𝑆) (𝑃 𝑄))) = (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
149134, 148eqtr3d 2835 . 2 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄)) = (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
150128, 149breqtrd 5056 1 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2111   class class class wbr 5030  cfv 6324  (class class class)co 7135  Basecbs 16475  lecple 16564  joincjn 17546  meetcmee 17547  Latclat 17647  OLcol 36470  Atomscatm 36559  HLchlt 36646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-proset 17530  df-poset 17548  df-plt 17560  df-lub 17576  df-glb 17577  df-join 17578  df-meet 17579  df-p0 17641  df-lat 17648  df-clat 17710  df-oposet 36472  df-ol 36474  df-oml 36475  df-covers 36562  df-ats 36563  df-atl 36594  df-cvlat 36618  df-hlat 36647  df-psubsp 36799  df-pmap 36800  df-padd 37092
This theorem is referenced by:  dalawlem13  37179
  Copyright terms: Public domain W3C validator