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

Theorem dalawlem3 36879
Description: Lemma for dalaw 36892. First piece of dalawlem5 36881. (Contributed by NM, 4-Oct-2012.)
Hypotheses
Ref Expression
dalawlem.l = (le‘𝐾)
dalawlem.j = (join‘𝐾)
dalawlem.m = (meet‘𝐾)
dalawlem.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
dalawlem3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))

Proof of Theorem dalawlem3
StepHypRef Expression
1 eqid 2826 . 2 (Base‘𝐾) = (Base‘𝐾)
2 dalawlem.l . 2 = (le‘𝐾)
3 simp11 1197 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ HL)
43hllatd 36370 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ Lat)
5 simp22 1201 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄𝐴)
6 simp32 1204 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇𝐴)
7 dalawlem.j . . . . . 6 = (join‘𝐾)
8 dalawlem.a . . . . . 6 𝐴 = (Atoms‘𝐾)
91, 7, 8hlatjcl 36373 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → (𝑄 𝑇) ∈ (Base‘𝐾))
103, 5, 6, 9syl3anc 1365 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑇) ∈ (Base‘𝐾))
11 simp21 1200 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃𝐴)
121, 8atbase 36295 . . . . 5 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1311, 12syl 17 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 ∈ (Base‘𝐾))
141, 7latjcl 17651 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾))
154, 10, 13, 14syl3anc 1365 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾))
16 simp31 1203 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆𝐴)
171, 8atbase 36295 . . . 4 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
1816, 17syl 17 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ∈ (Base‘𝐾))
19 dalawlem.m . . . 4 = (meet‘𝐾)
201, 19latmcl 17652 . . 3 ((𝐾 ∈ Lat ∧ ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑄 𝑇) 𝑃) 𝑆) ∈ (Base‘𝐾))
214, 15, 18, 20syl3anc 1365 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) ∈ (Base‘𝐾))
22 simp23 1202 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅𝐴)
231, 7, 8hlatjcl 36373 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
243, 5, 22, 23syl3anc 1365 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑅) ∈ (Base‘𝐾))
25 simp33 1205 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈𝐴)
261, 8atbase 36295 . . . . 5 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
2725, 26syl 17 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 ∈ (Base‘𝐾))
281, 19latmcl 17652 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾))
294, 24, 27, 28syl3anc 1365 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾))
301, 7, 8hlatjcl 36373 . . . . 5 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑃𝐴) → (𝑅 𝑃) ∈ (Base‘𝐾))
313, 22, 11, 30syl3anc 1365 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑃) ∈ (Base‘𝐾))
321, 7, 8hlatjcl 36373 . . . . 5 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑆𝐴) → (𝑈 𝑆) ∈ (Base‘𝐾))
333, 25, 16, 32syl3anc 1365 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑆) ∈ (Base‘𝐾))
341, 19latmcl 17652 . . . 4 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
354, 31, 33, 34syl3anc 1365 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
361, 7latjcl 17651 . . 3 ((𝐾 ∈ Lat ∧ ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
374, 29, 35, 36syl3anc 1365 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
381, 7, 8hlatjcl 36373 . . . . 5 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
393, 6, 25, 38syl3anc 1365 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑈) ∈ (Base‘𝐾))
401, 19latmcl 17652 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾)) → ((𝑄 𝑅) (𝑇 𝑈)) ∈ (Base‘𝐾))
414, 24, 39, 40syl3anc 1365 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑅) (𝑇 𝑈)) ∈ (Base‘𝐾))
421, 7latjcl 17651 . . 3 ((𝐾 ∈ Lat ∧ ((𝑄 𝑅) (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
434, 41, 35, 42syl3anc 1365 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
441, 8atbase 36295 . . . . . . . . . 10 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
455, 44syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 ∈ (Base‘𝐾))
461, 19latmcl 17652 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (𝑄 𝑈) ∈ (Base‘𝐾))
474, 45, 27, 46syl3anc 1365 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑈) ∈ (Base‘𝐾))
481, 7, 8hlatjcl 36373 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → (𝑃 𝑆) ∈ (Base‘𝐾))
493, 11, 16, 48syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
501, 19latmcl 17652 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))
514, 49, 45, 50syl3anc 1365 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))
521, 7latjcl 17651 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑄 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾)) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾))
534, 47, 51, 52syl3anc 1365 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾))
541, 7latjcl 17651 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) ∈ (Base‘𝐾))
554, 13, 53, 54syl3anc 1365 . . . . . 6 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) ∈ (Base‘𝐾))
561, 8atbase 36295 . . . . . . . . 9 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
5722, 56syl 17 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 ∈ (Base‘𝐾))
581, 7latjcl 17651 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾)) → (𝑅 ((𝑄 𝑅) 𝑈)) ∈ (Base‘𝐾))
594, 57, 29, 58syl3anc 1365 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 ((𝑄 𝑅) 𝑈)) ∈ (Base‘𝐾))
601, 7latjcl 17651 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑅 ((𝑄 𝑅) 𝑈)) ∈ (Base‘𝐾)) → (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))) ∈ (Base‘𝐾))
614, 13, 59, 60syl3anc 1365 . . . . . 6 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))) ∈ (Base‘𝐾))
621, 7latjcl 17651 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑄 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → ((𝑄 𝑈) 𝑃) ∈ (Base‘𝐾))
634, 47, 13, 62syl3anc 1365 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) 𝑃) ∈ (Base‘𝐾))
641, 2, 7, 19latmlej22 17693 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾) ∧ ((𝑄 𝑈) 𝑃) ∈ (Base‘𝐾))) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) 𝑃) 𝑆))
654, 18, 15, 63, 64syl13anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) 𝑃) 𝑆))
661, 7latjass 17695 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ ((𝑄 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (((𝑄 𝑈) 𝑃) 𝑆) = ((𝑄 𝑈) (𝑃 𝑆)))
674, 47, 13, 18, 66syl13anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑈) 𝑃) 𝑆) = ((𝑄 𝑈) (𝑃 𝑆)))
6865, 67breqtrd 5089 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) ((𝑄 𝑈) (𝑃 𝑆)))
691, 19latmcl 17652 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
704, 10, 49, 69syl3anc 1365 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
711, 7latjcl 17651 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) ∈ (Base‘𝐾))
724, 70, 13, 71syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) ∈ (Base‘𝐾))
731, 7, 8hlatjcl 36373 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
743, 11, 5, 73syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
752, 7, 8hlatlej2 36382 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → 𝑆 (𝑃 𝑆))
763, 11, 16, 75syl3anc 1365 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 (𝑃 𝑆))
771, 2, 19latmlem2 17682 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾))) → (𝑆 (𝑃 𝑆) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑇) 𝑃) (𝑃 𝑆))))
784, 18, 49, 15, 77syl13anc 1366 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 (𝑃 𝑆) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑇) 𝑃) (𝑃 𝑆))))
7976, 78mpd 15 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑇) 𝑃) (𝑃 𝑆)))
802, 7, 8hlatlej1 36381 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → 𝑃 (𝑃 𝑆))
813, 11, 16, 80syl3anc 1365 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑃 𝑆))
821, 2, 7, 19, 8atmod4i1 36872 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑆)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) = (((𝑄 𝑇) 𝑃) (𝑃 𝑆)))
833, 11, 10, 49, 81, 82syl131anc 1377 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) = (((𝑄 𝑇) 𝑃) (𝑃 𝑆)))
8479, 83breqtrrd 5091 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑇) (𝑃 𝑆)) 𝑃))
851, 19latmcom 17675 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
864, 10, 49, 85syl3anc 1365 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
87 simp12 1198 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄))
8886, 87eqbrtrd 5085 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) (𝑃 𝑄))
892, 7, 8hlatlej1 36381 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑃 (𝑃 𝑄))
903, 11, 5, 89syl3anc 1365 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑃 𝑄))
911, 2, 7latjle12 17662 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → ((((𝑄 𝑇) (𝑃 𝑆)) (𝑃 𝑄) ∧ 𝑃 (𝑃 𝑄)) ↔ (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) (𝑃 𝑄)))
924, 70, 13, 74, 91syl13anc 1366 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑄 𝑇) (𝑃 𝑆)) (𝑃 𝑄) ∧ 𝑃 (𝑃 𝑄)) ↔ (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) (𝑃 𝑄)))
9388, 90, 92mpbi2and 708 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) (𝑃 𝑄))
941, 2, 4, 21, 72, 74, 84, 93lattrd 17658 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 𝑄))
951, 7latjcl 17651 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑄 𝑈) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑈) (𝑃 𝑆)) ∈ (Base‘𝐾))
964, 47, 49, 95syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) (𝑃 𝑆)) ∈ (Base‘𝐾))
971, 2, 19latlem12 17678 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((((𝑄 𝑇) 𝑃) 𝑆) ∈ (Base‘𝐾) ∧ ((𝑄 𝑈) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → (((((𝑄 𝑇) 𝑃) 𝑆) ((𝑄 𝑈) (𝑃 𝑆)) ∧ (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 𝑄)) ↔ (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄))))
984, 21, 96, 74, 97syl13anc 1366 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((((𝑄 𝑇) 𝑃) 𝑆) ((𝑄 𝑈) (𝑃 𝑆)) ∧ (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 𝑄)) ↔ (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄))))
9968, 94, 98mpbi2and 708 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄)))
1001, 2, 7, 19, 8atmod3i1 36870 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑆)) → (𝑃 ((𝑃 𝑆) 𝑄)) = ((𝑃 𝑆) (𝑃 𝑄)))
1013, 11, 49, 45, 81, 100syl131anc 1377 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑃 𝑆) 𝑄)) = ((𝑃 𝑆) (𝑃 𝑄)))
102101oveq2d 7164 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) (𝑃 ((𝑃 𝑆) 𝑄))) = ((𝑄 𝑈) ((𝑃 𝑆) (𝑃 𝑄))))
1031, 7latj12 17696 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑄 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))) → ((𝑄 𝑈) (𝑃 ((𝑃 𝑆) 𝑄))) = (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))))
1044, 47, 13, 51, 103syl13anc 1366 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) (𝑃 ((𝑃 𝑆) 𝑄))) = (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))))
1051, 2, 7, 19latmlej12 17691 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (𝑄 𝑈) (𝑃 𝑄))
1064, 45, 27, 13, 105syl13anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑈) (𝑃 𝑄))
1071, 2, 7, 19, 8atmod1i1m 36864 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑈𝐴) ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) ∧ (𝑄 𝑈) (𝑃 𝑄)) → ((𝑄 𝑈) ((𝑃 𝑆) (𝑃 𝑄))) = (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄)))
1083, 25, 45, 49, 74, 106, 107syl231anc 1384 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) ((𝑃 𝑆) (𝑃 𝑄))) = (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄)))
109102, 104, 1083eqtr3rd 2870 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄)) = (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))))
11099, 109breqtrd 5089 . . . . . 6 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))))
1112, 7, 8hlatlej1 36381 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → 𝑄 (𝑄 𝑅))
1123, 5, 22, 111syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑅))
1132, 7, 8hlatlej2 36382 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → 𝑈 (𝑅 𝑈))
1143, 22, 25, 113syl3anc 1365 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑅 𝑈))
1151, 19latmcl 17652 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾))
1164, 49, 10, 115syl3anc 1365 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾))
1171, 7, 8hlatjcl 36373 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → (𝑅 𝑈) ∈ (Base‘𝐾))
1183, 22, 25, 117syl3anc 1365 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑈) ∈ (Base‘𝐾))
1192, 7, 8hlatlej1 36381 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → 𝑄 (𝑄 𝑇))
1203, 5, 6, 119syl3anc 1365 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑇))
1211, 2, 19latmlem2 17682 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾))) → (𝑄 (𝑄 𝑇) → ((𝑃 𝑆) 𝑄) ((𝑃 𝑆) (𝑄 𝑇))))
1224, 45, 10, 49, 121syl13anc 1366 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑄 𝑇) → ((𝑃 𝑆) 𝑄) ((𝑃 𝑆) (𝑄 𝑇))))
123120, 122mpd 15 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑄) ((𝑃 𝑆) (𝑄 𝑇)))
124 simp13 1199 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈))
1251, 2, 4, 51, 116, 118, 123, 124lattrd 17658 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑄) (𝑅 𝑈))
1261, 2, 7latjle12 17662 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾) ∧ (𝑅 𝑈) ∈ (Base‘𝐾))) → ((𝑈 (𝑅 𝑈) ∧ ((𝑃 𝑆) 𝑄) (𝑅 𝑈)) ↔ (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈)))
1274, 27, 51, 118, 126syl13anc 1366 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑈 (𝑅 𝑈) ∧ ((𝑃 𝑆) 𝑄) (𝑅 𝑈)) ↔ (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈)))
128114, 125, 127mpbi2and 708 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈))
1291, 7latjcl 17651 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾)) → (𝑈 ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾))
1304, 27, 51, 129syl3anc 1365 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾))
1311, 2, 19latmlem12 17683 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾)) ∧ ((𝑈 ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾) ∧ (𝑅 𝑈) ∈ (Base‘𝐾))) → ((𝑄 (𝑄 𝑅) ∧ (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈)) → (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))) ((𝑄 𝑅) (𝑅 𝑈))))
1324, 45, 24, 130, 118, 131syl122anc 1373 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑄 𝑅) ∧ (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈)) → (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))) ((𝑄 𝑅) (𝑅 𝑈))))
133112, 128, 132mp2and 695 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))) ((𝑄 𝑅) (𝑅 𝑈)))
1341, 2, 19latmle2 17677 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑄) 𝑄)
1354, 49, 45, 134syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑄) 𝑄)
1361, 2, 7, 19, 8atmod2i2 36868 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾)) ∧ ((𝑃 𝑆) 𝑄) 𝑄) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) = (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))))
1373, 25, 45, 51, 135, 136syl131anc 1377 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) = (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))))
1382, 7, 8hlatlej2 36382 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → 𝑅 (𝑄 𝑅))
1393, 5, 22, 138syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 (𝑄 𝑅))
1401, 2, 7, 19, 8atmod3i2 36871 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑅 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾)) ∧ 𝑅 (𝑄 𝑅)) → (𝑅 ((𝑄 𝑅) 𝑈)) = ((𝑄 𝑅) (𝑅 𝑈)))
1413, 25, 57, 24, 139, 140syl131anc 1377 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 ((𝑄 𝑅) 𝑈)) = ((𝑄 𝑅) (𝑅 𝑈)))
142133, 137, 1413brtr4d 5095 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) (𝑅 ((𝑄 𝑅) 𝑈)))
1431, 2, 7latjlej2 17666 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾) ∧ (𝑅 ((𝑄 𝑅) 𝑈)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) (𝑅 ((𝑄 𝑅) 𝑈)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) (𝑃 (𝑅 ((𝑄 𝑅) 𝑈)))))
1444, 53, 59, 13, 143syl13anc 1366 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) (𝑅 ((𝑄 𝑅) 𝑈)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) (𝑃 (𝑅 ((𝑄 𝑅) 𝑈)))))
145142, 144mpd 15 . . . . . 6 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))))
1461, 2, 4, 21, 55, 61, 110, 145lattrd 17658 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))))
1471, 7latj13 17698 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾))) → (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))) = (((𝑄 𝑅) 𝑈) (𝑅 𝑃)))
1484, 13, 57, 29, 147syl13anc 1366 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))) = (((𝑄 𝑅) 𝑈) (𝑅 𝑃)))
149146, 148breqtrd 5089 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) 𝑈) (𝑅 𝑃)))
1501, 2, 7, 19latmlej22 17693 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑈 𝑆))
1514, 18, 15, 27, 150syl13anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑈 𝑆))
1521, 7latjcl 17651 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾) ∧ (𝑅 𝑃) ∈ (Base‘𝐾)) → (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∈ (Base‘𝐾))
1534, 29, 31, 152syl3anc 1365 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∈ (Base‘𝐾))
1541, 2, 19latlem12 17678 . . . . 5 ((𝐾 ∈ Lat ∧ ((((𝑄 𝑇) 𝑃) 𝑆) ∈ (Base‘𝐾) ∧ (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾))) → (((((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∧ (((𝑄 𝑇) 𝑃) 𝑆) (𝑈 𝑆)) ↔ (((𝑄 𝑇) 𝑃) 𝑆) ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆))))
1554, 21, 153, 33, 154syl13anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∧ (((𝑄 𝑇) 𝑃) 𝑆) (𝑈 𝑆)) ↔ (((𝑄 𝑇) 𝑃) 𝑆) ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆))))
156149, 151, 155mpbi2and 708 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆)))
1571, 2, 7, 19latmlej21 17692 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑄 𝑅) 𝑈) (𝑈 𝑆))
1584, 27, 24, 18, 157syl13anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑅) 𝑈) (𝑈 𝑆))
1591, 2, 7, 19, 8atmod1i1m 36864 . . . 4 (((𝐾 ∈ HL ∧ 𝑈𝐴) ∧ ((𝑄 𝑅) ∈ (Base‘𝐾) ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) ∧ ((𝑄 𝑅) 𝑈) (𝑈 𝑆)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) = ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆)))
1603, 25, 24, 31, 33, 158, 159syl231anc 1384 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) = ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆)))
161156, 160breqtrrd 5091 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
1622, 7, 8hlatlej2 36382 . . . . 5 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → 𝑈 (𝑇 𝑈))
1633, 6, 25, 162syl3anc 1365 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑇 𝑈))
1641, 2, 19latmlem2 17682 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → (𝑈 (𝑇 𝑈) → ((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈))))
1654, 27, 39, 24, 164syl13anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 (𝑇 𝑈) → ((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈))))
166163, 165mpd 15 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈)))
1671, 2, 7latjlej1 17665 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾) ∧ ((𝑄 𝑅) (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))) → (((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆)))))
1684, 29, 41, 35, 167syl13anc 1366 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆)))))
169166, 168mpd 15 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
1701, 2, 4, 21, 37, 43, 161, 169lattrd 17658 1 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107   class class class wbr 5063  cfv 6352  (class class class)co 7148  Basecbs 16473  lecple 16562  joincjn 17544  meetcmee 17545  Latclat 17645  Atomscatm 36269  HLchlt 36356
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-1st 7680  df-2nd 7681  df-proset 17528  df-poset 17546  df-plt 17558  df-lub 17574  df-glb 17575  df-join 17576  df-meet 17577  df-p0 17639  df-lat 17646  df-clat 17708  df-oposet 36182  df-ol 36184  df-oml 36185  df-covers 36272  df-ats 36273  df-atl 36304  df-cvlat 36328  df-hlat 36357  df-psubsp 36509  df-pmap 36510  df-padd 36802
This theorem is referenced by:  dalawlem4  36880  dalawlem5  36881
  Copyright terms: Public domain W3C validator