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 38345
Description: Lemma for dalaw 38349. Second part of dalawlem13 38346. (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 2736 . . . 4 (Base‘𝐾) = (Base‘𝐾)
2 dalawlem.l . . . 4 = (le‘𝐾)
3 simp11 1203 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ HL)
43hllatd 37826 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ Lat)
5 simp21 1206 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃𝐴)
6 simp22 1207 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄𝐴)
7 dalawlem.j . . . . . . 7 = (join‘𝐾)
8 dalawlem.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
91, 7, 8hlatjcl 37829 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
103, 5, 6, 9syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
11 simp31 1209 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆𝐴)
12 simp32 1210 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇𝐴)
131, 7, 8hlatjcl 37829 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
143, 11, 12, 13syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 𝑇) ∈ (Base‘𝐾))
15 dalawlem.m . . . . . 6 = (meet‘𝐾)
161, 15latmcl 18329 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
174, 10, 14, 16syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
181, 8atbase 37751 . . . . . . . 8 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
1911, 18syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ∈ (Base‘𝐾))
201, 7latjcl 18328 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾))
214, 10, 19, 20syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾))
221, 8atbase 37751 . . . . . . 7 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
2312, 22syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 ∈ (Base‘𝐾))
241, 15latmcl 18329 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑆) 𝑇) ∈ (Base‘𝐾))
254, 21, 23, 24syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑆) 𝑇) ∈ (Base‘𝐾))
261, 7latjcl 18328 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) 𝑆) 𝑇) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) ∈ (Base‘𝐾))
274, 25, 19, 26syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) ∈ (Base‘𝐾))
281, 8atbase 37751 . . . . . . 7 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
296, 28syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 ∈ (Base‘𝐾))
30 simp33 1211 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈𝐴)
311, 7, 8hlatjcl 37829 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
323, 12, 30, 31syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑈) ∈ (Base‘𝐾))
331, 15latmcl 18329 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾)) → (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾))
344, 29, 32, 33syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾))
351, 7, 8hlatjcl 37829 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑆𝐴) → (𝑈 𝑆) ∈ (Base‘𝐾))
363, 30, 11, 35syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑆) ∈ (Base‘𝐾))
371, 7latjcl 18328 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∈ (Base‘𝐾))
384, 34, 36, 37syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∈ (Base‘𝐾))
391, 2, 7latlej1 18337 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑆))
404, 10, 19, 39syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑆))
411, 7, 8hlatjcl 37829 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑆𝐴) → (𝑇 𝑆) ∈ (Base‘𝐾))
423, 12, 11, 41syl3anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑆) ∈ (Base‘𝐾))
431, 2, 15latmlem1 18358 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾) ∧ (𝑇 𝑆) ∈ (Base‘𝐾))) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑆) → ((𝑃 𝑄) (𝑇 𝑆)) (((𝑃 𝑄) 𝑆) (𝑇 𝑆))))
444, 10, 21, 42, 43syl13anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑆) → ((𝑃 𝑄) (𝑇 𝑆)) (((𝑃 𝑄) 𝑆) (𝑇 𝑆))))
4540, 44mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑇 𝑆)) (((𝑃 𝑄) 𝑆) (𝑇 𝑆)))
467, 8hlatjcom 37830 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) = (𝑇 𝑆))
473, 11, 12, 46syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 𝑇) = (𝑇 𝑆))
4847oveq2d 7373 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) = ((𝑃 𝑄) (𝑇 𝑆)))
491, 2, 7latlej2 18338 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 ((𝑃 𝑄) 𝑆))
504, 10, 19, 49syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ((𝑃 𝑄) 𝑆))
511, 2, 7, 15, 8atmod2i2 38325 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑇𝐴 ∧ ((𝑃 𝑄) 𝑆) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) ∧ 𝑆 ((𝑃 𝑄) 𝑆)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) = (((𝑃 𝑄) 𝑆) (𝑇 𝑆)))
523, 12, 21, 19, 50, 51syl131anc 1383 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) = (((𝑃 𝑄) 𝑆) (𝑇 𝑆)))
5345, 48, 523brtr4d 5137 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆))
54 hlol 37823 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
553, 54syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ OL)
561, 7, 8hlatjcl 37829 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → (𝑃 𝑆) ∈ (Base‘𝐾))
573, 5, 11, 56syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
581, 7latjcl 18328 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → (𝑄 (𝑃 𝑆)) ∈ (Base‘𝐾))
594, 29, 57, 58syl3anc 1371 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑃 𝑆)) ∈ (Base‘𝐾))
601, 7, 8hlatjcl 37829 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → (𝑄 𝑇) ∈ (Base‘𝐾))
613, 6, 12, 60syl3anc 1371 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑇) ∈ (Base‘𝐾))
621, 15latmassOLD 37691 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ ((𝑄 (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾))) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) = ((𝑄 (𝑃 𝑆)) ((𝑄 𝑇) 𝑇)))
6355, 59, 61, 23, 62syl13anc 1372 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) = ((𝑄 (𝑃 𝑆)) ((𝑄 𝑇) 𝑇)))
647, 8hlatjass 37832 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → ((𝑃 𝑄) 𝑆) = (𝑃 (𝑄 𝑆)))
653, 5, 6, 11, 64syl13anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑆) = (𝑃 (𝑄 𝑆)))
667, 8hlatj12 37833 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → (𝑃 (𝑄 𝑆)) = (𝑄 (𝑃 𝑆)))
673, 5, 6, 11, 66syl13anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑄 𝑆)) = (𝑄 (𝑃 𝑆)))
6865, 67eqtr2d 2777 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑃 𝑆)) = ((𝑃 𝑄) 𝑆))
692, 7, 8hlatlej2 37838 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → 𝑇 (𝑄 𝑇))
703, 6, 12, 69syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 (𝑄 𝑇))
711, 2, 15latleeqm2 18357 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → (𝑇 (𝑄 𝑇) ↔ ((𝑄 𝑇) 𝑇) = 𝑇))
724, 23, 61, 71syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 (𝑄 𝑇) ↔ ((𝑄 𝑇) 𝑇) = 𝑇))
7370, 72mpbid 231 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) 𝑇) = 𝑇)
7468, 73oveq12d 7375 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑃 𝑆)) ((𝑄 𝑇) 𝑇)) = (((𝑃 𝑄) 𝑆) 𝑇))
7563, 74eqtr2d 2777 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑆) 𝑇) = (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇))
762, 7, 8hlatlej1 37837 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → 𝑄 (𝑄 𝑇))
773, 6, 12, 76syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑇))
781, 2, 7, 15, 8atmod1i1 38320 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑄𝐴 ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) ∧ 𝑄 (𝑄 𝑇)) → (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) = ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)))
793, 6, 57, 61, 77, 78syl131anc 1383 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) = ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)))
802, 7, 8hlatlej2 37838 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑄𝐴) → 𝑄 (𝑈 𝑄))
813, 30, 6, 80syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑈 𝑄))
82 simp13 1205 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈))
83 simp12 1204 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 = 𝑅)
8483oveq1d 7372 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑈) = (𝑅 𝑈))
857, 8hlatjcom 37830 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑈𝐴) → (𝑄 𝑈) = (𝑈 𝑄))
863, 6, 30, 85syl3anc 1371 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑈) = (𝑈 𝑄))
8784, 86eqtr3d 2778 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑈) = (𝑈 𝑄))
8882, 87breqtrd 5131 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑈 𝑄))
891, 15latmcl 18329 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾))
904, 57, 61, 89syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾))
911, 7, 8hlatjcl 37829 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑄𝐴) → (𝑈 𝑄) ∈ (Base‘𝐾))
923, 30, 6, 91syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑄) ∈ (Base‘𝐾))
931, 2, 7latjle12 18339 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑈 𝑄) ∈ (Base‘𝐾))) → ((𝑄 (𝑈 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑈 𝑄)) ↔ (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) (𝑈 𝑄)))
944, 29, 90, 92, 93syl13anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑈 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑈 𝑄)) ↔ (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) (𝑈 𝑄)))
9581, 88, 94mpbi2and 710 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 ((𝑃 𝑆) (𝑄 𝑇))) (𝑈 𝑄))
9679, 95eqbrtrrd 5129 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) (𝑈 𝑄))
972, 7, 8hlatlej1 37837 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → 𝑇 (𝑇 𝑈))
983, 12, 30, 97syl3anc 1371 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 (𝑇 𝑈))
991, 15latmcl 18329 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑄 (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) ∈ (Base‘𝐾))
1004, 59, 61, 99syl3anc 1371 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) ∈ (Base‘𝐾))
1011, 2, 15latmlem12 18360 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑈 𝑄) ∈ (Base‘𝐾)) ∧ (𝑇 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾))) → ((((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) (𝑈 𝑄) ∧ 𝑇 (𝑇 𝑈)) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) ((𝑈 𝑄) (𝑇 𝑈))))
1024, 100, 92, 23, 32, 101syl122anc 1379 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) (𝑈 𝑄) ∧ 𝑇 (𝑇 𝑈)) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) ((𝑈 𝑄) (𝑇 𝑈))))
10396, 98, 102mp2and 697 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 (𝑃 𝑆)) (𝑄 𝑇)) 𝑇) ((𝑈 𝑄) (𝑇 𝑈)))
10475, 103eqbrtrd 5127 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑆) 𝑇) ((𝑈 𝑄) (𝑇 𝑈)))
1052, 7, 8hlatlej2 37838 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → 𝑈 (𝑇 𝑈))
1063, 12, 30, 105syl3anc 1371 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑇 𝑈))
1071, 2, 7, 15, 8atmod1i1 38320 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑄 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑇 𝑈)) → (𝑈 (𝑄 (𝑇 𝑈))) = ((𝑈 𝑄) (𝑇 𝑈)))
1083, 30, 29, 32, 106, 107syl131anc 1383 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 (𝑄 (𝑇 𝑈))) = ((𝑈 𝑄) (𝑇 𝑈)))
1091, 8atbase 37751 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
11030, 109syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 ∈ (Base‘𝐾))
1111, 7latjcom 18336 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾)) → (𝑈 (𝑄 (𝑇 𝑈))) = ((𝑄 (𝑇 𝑈)) 𝑈))
1124, 110, 34, 111syl3anc 1371 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 (𝑄 (𝑇 𝑈))) = ((𝑄 (𝑇 𝑈)) 𝑈))
113108, 112eqtr3d 2778 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑈 𝑄) (𝑇 𝑈)) = ((𝑄 (𝑇 𝑈)) 𝑈))
114104, 113breqtrd 5131 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑆) 𝑇) ((𝑄 (𝑇 𝑈)) 𝑈))
1151, 7latjcl 18328 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑄 (𝑇 𝑈)) 𝑈) ∈ (Base‘𝐾))
1164, 34, 110, 115syl3anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑇 𝑈)) 𝑈) ∈ (Base‘𝐾))
1171, 2, 7latjlej1 18342 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((((𝑃 𝑄) 𝑆) 𝑇) ∈ (Base‘𝐾) ∧ ((𝑄 (𝑇 𝑈)) 𝑈) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑆) 𝑇) ((𝑄 (𝑇 𝑈)) 𝑈) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆)))
1184, 25, 116, 19, 117syl13anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) ((𝑄 (𝑇 𝑈)) 𝑈) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆)))
119114, 118mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆))
1201, 7latjass 18372 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆) = ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)))
1214, 34, 110, 19, 120syl13anc 1372 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 (𝑇 𝑈)) 𝑈) 𝑆) = ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)))
122119, 121breqtrd 5131 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑆) 𝑇) 𝑆) ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)))
1231, 2, 4, 17, 27, 38, 53, 122lattrd 18335 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)))
1241, 2, 15latmle1 18353 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
1254, 10, 14, 124syl3anc 1371 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
1261, 2, 15latlem12 18355 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾) ∧ ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → ((((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∧ ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄)) ↔ ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄))))
1274, 17, 38, 10, 126syl13anc 1372 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) ∧ ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄)) ↔ ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄))))
128123, 125, 127mpbi2and 710 . 2 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄)))
1291, 8atbase 37751 . . . . . 6 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1305, 129syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 ∈ (Base‘𝐾))
1311, 2, 7, 15latmlej12 18368 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (𝑄 (𝑇 𝑈)) (𝑃 𝑄))
1324, 29, 32, 130, 131syl13anc 1372 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑇 𝑈)) (𝑃 𝑄))
1331, 2, 7, 15, 8llnmod1i2 38323 . . . 4 (((𝐾 ∈ HL ∧ (𝑄 (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) ∧ (𝑈𝐴𝑆𝐴) ∧ (𝑄 (𝑇 𝑈)) (𝑃 𝑄)) → ((𝑄 (𝑇 𝑈)) ((𝑈 𝑆) (𝑃 𝑄))) = (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄)))
1343, 34, 10, 30, 11, 132, 133syl321anc 1392 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑇 𝑈)) ((𝑈 𝑆) (𝑃 𝑄))) = (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄)))
1357, 8hlatjidm 37831 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑄𝐴) → (𝑄 𝑄) = 𝑄)
1363, 6, 135syl2anc 584 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑄) = 𝑄)
13783oveq2d 7373 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑄) = (𝑄 𝑅))
138136, 137eqtr3d 2778 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 = (𝑄 𝑅))
139138oveq1d 7372 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑇 𝑈)) = ((𝑄 𝑅) (𝑇 𝑈)))
1401, 15latmcom 18352 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑈 𝑆) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → ((𝑈 𝑆) (𝑃 𝑄)) = ((𝑃 𝑄) (𝑈 𝑆)))
1414, 36, 10, 140syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑈 𝑆) (𝑃 𝑄)) = ((𝑃 𝑄) (𝑈 𝑆)))
1427, 8hlatjcom 37830 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) = (𝑄 𝑃))
1433, 5, 6, 142syl3anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) = (𝑄 𝑃))
14483oveq1d 7372 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑃) = (𝑅 𝑃))
145143, 144eqtrd 2776 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) = (𝑅 𝑃))
146145oveq1d 7372 . . . . 5 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑈 𝑆)) = ((𝑅 𝑃) (𝑈 𝑆)))
147141, 146eqtrd 2776 . . . 4 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑈 𝑆) (𝑃 𝑄)) = ((𝑅 𝑃) (𝑈 𝑆)))
148139, 147oveq12d 7375 . . 3 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑇 𝑈)) ((𝑈 𝑆) (𝑃 𝑄))) = (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
149134, 148eqtr3d 2778 . 2 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 (𝑇 𝑈)) (𝑈 𝑆)) (𝑃 𝑄)) = (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
150128, 149breqtrd 5131 1 (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106   class class class wbr 5105  cfv 6496  (class class class)co 7357  Basecbs 17083  lecple 17140  joincjn 18200  meetcmee 18201  Latclat 18320  OLcol 37636  Atomscatm 37725  HLchlt 37812
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-proset 18184  df-poset 18202  df-plt 18219  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-p0 18314  df-lat 18321  df-clat 18388  df-oposet 37638  df-ol 37640  df-oml 37641  df-covers 37728  df-ats 37729  df-atl 37760  df-cvlat 37784  df-hlat 37813  df-psubsp 37966  df-pmap 37967  df-padd 38259
This theorem is referenced by:  dalawlem13  38346
  Copyright terms: Public domain W3C validator