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 33985
Description: Lemma for dalaw 33990. First part of dalawlem13 33987. (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 2606 . . . 4 (Base‘𝐾) = (Base‘𝐾)
2 dalawlem.l . . . 4 = (le‘𝐾)
3 simp11 1083 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ HL)
4 hllat 33468 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ Lat)
53, 4syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ Lat)
6 simp21 1086 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃𝐴)
7 simp22 1087 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄𝐴)
8 dalawlem.j . . . . . . 7 = (join‘𝐾)
9 dalawlem.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
101, 8, 9hlatjcl 33471 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
113, 6, 7, 10syl3anc 1317 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
12 simp31 1089 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆𝐴)
13 simp32 1090 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇𝐴)
141, 8, 9hlatjcl 33471 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
153, 12, 13, 14syl3anc 1317 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 𝑇) ∈ (Base‘𝐾))
16 dalawlem.m . . . . . 6 = (meet‘𝐾)
171, 16latmcl 16818 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
185, 11, 15, 17syl3anc 1317 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾))
19 simp23 1088 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅𝐴)
201, 8, 9hlatjcl 33471 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
213, 7, 19, 20syl3anc 1317 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑅) ∈ (Base‘𝐾))
221, 2, 16latmle1 16842 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
235, 11, 15, 22syl3anc 1317 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑃 𝑄))
24 simp12 1084 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑄 𝑅))
251, 9atbase 33394 . . . . . . 7 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
267, 25syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 ∈ (Base‘𝐾))
271, 9atbase 33394 . . . . . . 7 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
2819, 27syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 ∈ (Base‘𝐾))
291, 2, 8latlej1 16826 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑄 (𝑄 𝑅))
305, 26, 28, 29syl3anc 1317 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑅))
311, 9atbase 33394 . . . . . . 7 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
326, 31syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 ∈ (Base‘𝐾))
331, 2, 8latjle12 16828 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑃 (𝑄 𝑅) ∧ 𝑄 (𝑄 𝑅)) ↔ (𝑃 𝑄) (𝑄 𝑅)))
345, 32, 26, 21, 33syl13anc 1319 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑅) ∧ 𝑄 (𝑄 𝑅)) ↔ (𝑃 𝑄) (𝑄 𝑅)))
3524, 30, 34mpbi2and 957 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) (𝑄 𝑅))
361, 2, 5, 18, 11, 21, 23, 35lattrd 16824 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅))
371, 9atbase 33394 . . . . . . . 8 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
3813, 37syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 ∈ (Base‘𝐾))
391, 8latjcl 16817 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾))
405, 11, 38, 39syl3anc 1317 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾))
411, 16latmcl 16818 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ∈ (Base‘𝐾))
425, 40, 15, 41syl3anc 1317 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ∈ (Base‘𝐾))
431, 8, 9hlatjcl 33471 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑃𝐴) → (𝑅 𝑃) ∈ (Base‘𝐾))
443, 19, 6, 43syl3anc 1317 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑃) ∈ (Base‘𝐾))
45 simp33 1091 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈𝐴)
461, 8, 9hlatjcl 33471 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑆𝐴) → (𝑈 𝑆) ∈ (Base‘𝐾))
473, 45, 12, 46syl3anc 1317 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑆) ∈ (Base‘𝐾))
481, 16latmcl 16818 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
495, 44, 47, 48syl3anc 1317 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
501, 9atbase 33394 . . . . . . . 8 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
5145, 50syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 ∈ (Base‘𝐾))
521, 8latjcl 16817 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾))
535, 49, 51, 52syl3anc 1317 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾))
541, 8latjcl 16817 . . . . . 6 ((𝐾 ∈ Lat ∧ (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) ∈ (Base‘𝐾))
555, 53, 38, 54syl3anc 1317 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) ∈ (Base‘𝐾))
561, 2, 8latlej1 16826 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑇))
575, 11, 38, 56syl3anc 1317 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑇))
581, 2, 16latmlem1 16847 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾))) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑇) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇))))
595, 11, 40, 15, 58syl13anc 1319 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) ((𝑃 𝑄) 𝑇) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇))))
6057, 59mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
611, 2, 8latlej2 16827 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 ((𝑃 𝑄) 𝑇))
625, 11, 38, 61syl3anc 1317 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇 ((𝑃 𝑄) 𝑇))
631, 2, 8, 16, 9atmod2i2 33966 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑆𝐴 ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) ∧ 𝑇 ((𝑃 𝑄) 𝑇)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) = (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
643, 12, 40, 38, 62, 63syl131anc 1330 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) = (((𝑃 𝑄) 𝑇) (𝑆 𝑇)))
651, 8, 9hlatjcl 33471 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → (𝑄 𝑇) ∈ (Base‘𝐾))
663, 7, 13, 65syl3anc 1317 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑇) ∈ (Base‘𝐾))
671, 8, 9hlatjcl 33471 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → (𝑃 𝑆) ∈ (Base‘𝐾))
683, 6, 12, 67syl3anc 1317 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
691, 16latmcom 16841 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
705, 66, 68, 69syl3anc 1317 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
71 simp13 1085 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈))
7270, 71eqbrtrd 4596 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈))
731, 16latmcl 16818 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
745, 66, 68, 73syl3anc 1317 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
751, 8, 9hlatjcl 33471 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → (𝑅 𝑈) ∈ (Base‘𝐾))
763, 19, 45, 75syl3anc 1317 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑈) ∈ (Base‘𝐾))
771, 2, 8latjlej2 16832 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑅 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈))))
785, 74, 76, 32, 77syl13anc 1319 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) (𝑅 𝑈) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈))))
7972, 78mpd 15 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) (𝑃 (𝑅 𝑈)))
801, 9atbase 33394 . . . . . . . . . . . . 13 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
8112, 80syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ∈ (Base‘𝐾))
821, 2, 8latlej1 16826 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑃 (𝑃 𝑆))
835, 32, 81, 82syl3anc 1317 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑃 𝑆))
841, 2, 8, 16, 9atmod1i1 33961 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑆)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) = ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)))
853, 6, 66, 68, 83, 84syl131anc 1330 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑇) (𝑃 𝑆))) = ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)))
868, 9hlatjass 33474 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑅𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = (𝑃 (𝑅 𝑈)))
873, 6, 19, 45, 86syl13anc 1319 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = (𝑃 (𝑅 𝑈)))
888, 9hlatjcom 33472 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴) → (𝑃 𝑅) = (𝑅 𝑃))
893, 6, 19, 88syl3anc 1317 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑅) = (𝑅 𝑃))
9089oveq1d 6539 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑅) 𝑈) = ((𝑅 𝑃) 𝑈))
9187, 90eqtr3d 2642 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑅 𝑈)) = ((𝑅 𝑃) 𝑈))
9279, 85, 913brtr3d 4605 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈))
931, 2, 8latlej2 16827 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 (𝑈 𝑆))
945, 51, 81, 93syl3anc 1317 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 (𝑈 𝑆))
951, 8latjcl 16817 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾))
965, 32, 66, 95syl3anc 1317 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾))
971, 16latmcl 16818 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾))
985, 96, 68, 97syl3anc 1317 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾))
991, 8latjcl 16817 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾))
1005, 44, 51, 99syl3anc 1317 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾))
1011, 2, 16latmlem12 16849 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) 𝑈) ∈ (Base‘𝐾)) ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾))) → ((((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈) ∧ 𝑆 (𝑈 𝑆)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆))))
1025, 98, 100, 81, 47, 101syl122anc 1326 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) ((𝑅 𝑃) 𝑈) ∧ 𝑆 (𝑈 𝑆)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆))))
10392, 94, 102mp2and 710 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
104 hlol 33466 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
1053, 104syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ OL)
1061, 16latmassOLD 33334 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ ((𝑃 (𝑄 𝑇)) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) = ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)))
107105, 96, 68, 81, 106syl13anc 1319 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆) = ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)))
1088, 9hlatjass 33474 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑇𝐴)) → ((𝑃 𝑄) 𝑇) = (𝑃 (𝑄 𝑇)))
1093, 6, 7, 13, 108syl13anc 1319 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) 𝑇) = (𝑃 (𝑄 𝑇)))
110109eqcomd 2612 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑄 𝑇)) = ((𝑃 𝑄) 𝑇))
1111, 2, 8latlej2 16827 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 (𝑃 𝑆))
1125, 32, 81, 111syl3anc 1317 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 (𝑃 𝑆))
1131, 2, 16latleeqm2 16846 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → (𝑆 (𝑃 𝑆) ↔ ((𝑃 𝑆) 𝑆) = 𝑆))
1145, 81, 68, 113syl3anc 1317 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 (𝑃 𝑆) ↔ ((𝑃 𝑆) 𝑆) = 𝑆))
115112, 114mpbid 220 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑆) = 𝑆)
116110, 115oveq12d 6542 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 (𝑄 𝑇)) ((𝑃 𝑆) 𝑆)) = (((𝑃 𝑄) 𝑇) 𝑆))
117107, 116eqtr2d 2641 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) = (((𝑃 (𝑄 𝑇)) (𝑃 𝑆)) 𝑆))
1181, 2, 8latlej1 16826 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑈 (𝑈 𝑆))
1195, 51, 81, 118syl3anc 1317 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑈 𝑆))
1201, 2, 8, 16, 9atmod4i1 33970 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑈 𝑆)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) = (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
1213, 45, 44, 47, 119, 120syl131anc 1330 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) = (((𝑅 𝑃) 𝑈) (𝑈 𝑆)))
122103, 117, 1213brtr4d 4606 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈))
1231, 16latmcl 16818 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑇) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾))
1245, 40, 81, 123syl3anc 1317 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾))
1251, 2, 8latjlej1 16831 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((((𝑃 𝑄) 𝑇) 𝑆) ∈ (Base‘𝐾) ∧ (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇)))
1265, 124, 53, 38, 125syl13anc 1319 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) (((𝑅 𝑃) (𝑈 𝑆)) 𝑈) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇)))
127122, 126mpd 15 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) 𝑇) 𝑆) 𝑇) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
12864, 127eqbrtrrd 4598 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑃 𝑄) 𝑇) (𝑆 𝑇)) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
1291, 2, 5, 18, 42, 55, 60, 128lattrd 16824 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇))
1301, 8latj31 16865 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾))) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) = ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
1315, 49, 51, 38, 130syl13anc 1319 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑅 𝑃) (𝑈 𝑆)) 𝑈) 𝑇) = ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
132129, 131breqtrd 4600 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
1331, 8, 9hlatjcl 33471 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
1343, 13, 45, 133syl3anc 1317 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑈) ∈ (Base‘𝐾))
1351, 8latjcl 16817 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) → ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
1365, 134, 49, 135syl3anc 1317 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
1371, 2, 16latlem12 16844 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) (𝑆 𝑇)) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))) → ((((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅) ∧ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))) ↔ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))))
1385, 18, 21, 136, 137syl13anc 1319 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑃 𝑄) (𝑆 𝑇)) (𝑄 𝑅) ∧ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))) ↔ ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))))
13936, 132, 138mpbi2and 957 . 2 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
1401, 2, 16latmle1 16842 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑅 𝑃))
1415, 44, 47, 140syl3anc 1317 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑅 𝑃))
1421, 2, 8latlej2 16827 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑅 (𝑄 𝑅))
1435, 26, 28, 142syl3anc 1317 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 (𝑄 𝑅))
1441, 2, 8latjle12 16828 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑅 (𝑄 𝑅) ∧ 𝑃 (𝑄 𝑅)) ↔ (𝑅 𝑃) (𝑄 𝑅)))
1455, 28, 32, 21, 144syl13anc 1319 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 (𝑄 𝑅) ∧ 𝑃 (𝑄 𝑅)) ↔ (𝑅 𝑃) (𝑄 𝑅)))
146143, 24, 145mpbi2and 957 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑃) (𝑄 𝑅))
1471, 2, 5, 49, 44, 21, 141, 146lattrd 16824 . . 3 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) (𝑄 𝑅))
1481, 2, 8, 16, 9llnmod2i2 33967 . . 3 (((𝐾 ∈ HL ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) ∧ (𝑇𝐴𝑈𝐴) ∧ ((𝑅 𝑃) (𝑈 𝑆)) (𝑄 𝑅)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) = ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
1493, 21, 49, 13, 45, 147, 148syl321anc 1339 . 2 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) = ((𝑄 𝑅) ((𝑇 𝑈) ((𝑅 𝑃) (𝑈 𝑆)))))
150139, 149breqtrrd 4602 1 (((𝐾 ∈ HL ∧ 𝑃 (𝑄 𝑅) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑄) (𝑆 𝑇)) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976   class class class wbr 4574  cfv 5787  (class class class)co 6524  Basecbs 15638  lecple 15718  joincjn 16710  meetcmee 16711  Latclat 16811  OLcol 33279  Atomscatm 33368  HLchlt 33455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-iun 4448  df-iin 4449  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-1st 7033  df-2nd 7034  df-preset 16694  df-poset 16712  df-plt 16724  df-lub 16740  df-glb 16741  df-join 16742  df-meet 16743  df-p0 16805  df-lat 16812  df-clat 16874  df-oposet 33281  df-ol 33283  df-oml 33284  df-covers 33371  df-ats 33372  df-atl 33403  df-cvlat 33427  df-hlat 33456  df-psubsp 33607  df-pmap 33608  df-padd 33900
This theorem is referenced by:  dalawlem13  33987
  Copyright terms: Public domain W3C validator