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

Theorem dalawlem3 35477
 Description: Lemma for dalaw 35490. First piece of dalawlem5 35479. (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 2651 . 2 (Base‘𝐾) = (Base‘𝐾)
2 dalawlem.l . 2 = (le‘𝐾)
3 simp11 1111 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ HL)
4 hllat 34968 . . 3 (𝐾 ∈ HL → 𝐾 ∈ Lat)
53, 4syl 17 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝐾 ∈ Lat)
6 simp22 1115 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄𝐴)
7 simp32 1118 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑇𝐴)
8 dalawlem.j . . . . . 6 = (join‘𝐾)
9 dalawlem.a . . . . . 6 𝐴 = (Atoms‘𝐾)
101, 8, 9hlatjcl 34971 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → (𝑄 𝑇) ∈ (Base‘𝐾))
113, 6, 7, 10syl3anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑇) ∈ (Base‘𝐾))
12 simp21 1114 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃𝐴)
131, 9atbase 34894 . . . . 5 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1412, 13syl 17 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 ∈ (Base‘𝐾))
151, 8latjcl 17098 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾))
165, 11, 14, 15syl3anc 1366 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾))
17 simp31 1117 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆𝐴)
181, 9atbase 34894 . . . 4 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
1917, 18syl 17 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 ∈ (Base‘𝐾))
20 dalawlem.m . . . 4 = (meet‘𝐾)
211, 20latmcl 17099 . . 3 ((𝐾 ∈ Lat ∧ ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑄 𝑇) 𝑃) 𝑆) ∈ (Base‘𝐾))
225, 16, 19, 21syl3anc 1366 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) ∈ (Base‘𝐾))
23 simp23 1116 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅𝐴)
241, 8, 9hlatjcl 34971 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
253, 6, 23, 24syl3anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑅) ∈ (Base‘𝐾))
26 simp33 1119 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈𝐴)
271, 9atbase 34894 . . . . 5 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
2826, 27syl 17 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 ∈ (Base‘𝐾))
291, 20latmcl 17099 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾))
305, 25, 28, 29syl3anc 1366 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾))
311, 8, 9hlatjcl 34971 . . . . 5 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑃𝐴) → (𝑅 𝑃) ∈ (Base‘𝐾))
323, 23, 12, 31syl3anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑃) ∈ (Base‘𝐾))
331, 8, 9hlatjcl 34971 . . . . 5 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑆𝐴) → (𝑈 𝑆) ∈ (Base‘𝐾))
343, 26, 17, 33syl3anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 𝑆) ∈ (Base‘𝐾))
351, 20latmcl 17099 . . . 4 ((𝐾 ∈ Lat ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
365, 32, 34, 35syl3anc 1366 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))
371, 8latjcl 17098 . . 3 ((𝐾 ∈ Lat ∧ ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
385, 30, 36, 37syl3anc 1366 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
391, 8, 9hlatjcl 34971 . . . . 5 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
403, 7, 26, 39syl3anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑇 𝑈) ∈ (Base‘𝐾))
411, 20latmcl 17099 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾)) → ((𝑄 𝑅) (𝑇 𝑈)) ∈ (Base‘𝐾))
425, 25, 40, 41syl3anc 1366 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑅) (𝑇 𝑈)) ∈ (Base‘𝐾))
431, 8latjcl 17098 . . 3 ((𝐾 ∈ Lat ∧ ((𝑄 𝑅) (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
445, 42, 36, 43syl3anc 1366 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))) ∈ (Base‘𝐾))
451, 9atbase 34894 . . . . . . . . . 10 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
466, 45syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 ∈ (Base‘𝐾))
471, 20latmcl 17099 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (𝑄 𝑈) ∈ (Base‘𝐾))
485, 46, 28, 47syl3anc 1366 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑈) ∈ (Base‘𝐾))
491, 8, 9hlatjcl 34971 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → (𝑃 𝑆) ∈ (Base‘𝐾))
503, 12, 17, 49syl3anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
511, 20latmcl 17099 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))
525, 50, 46, 51syl3anc 1366 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))
531, 8latjcl 17098 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑄 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾)) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾))
545, 48, 52, 53syl3anc 1366 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾))
551, 8latjcl 17098 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) ∈ (Base‘𝐾))
565, 14, 54, 55syl3anc 1366 . . . . . 6 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) ∈ (Base‘𝐾))
571, 9atbase 34894 . . . . . . . . 9 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
5823, 57syl 17 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 ∈ (Base‘𝐾))
591, 8latjcl 17098 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾)) → (𝑅 ((𝑄 𝑅) 𝑈)) ∈ (Base‘𝐾))
605, 58, 30, 59syl3anc 1366 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 ((𝑄 𝑅) 𝑈)) ∈ (Base‘𝐾))
611, 8latjcl 17098 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑅 ((𝑄 𝑅) 𝑈)) ∈ (Base‘𝐾)) → (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))) ∈ (Base‘𝐾))
625, 14, 60, 61syl3anc 1366 . . . . . 6 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))) ∈ (Base‘𝐾))
631, 8latjcl 17098 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑄 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → ((𝑄 𝑈) 𝑃) ∈ (Base‘𝐾))
645, 48, 14, 63syl3anc 1366 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) 𝑃) ∈ (Base‘𝐾))
651, 2, 8, 20latmlej22 17140 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾) ∧ ((𝑄 𝑈) 𝑃) ∈ (Base‘𝐾))) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) 𝑃) 𝑆))
665, 19, 16, 64, 65syl13anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) 𝑃) 𝑆))
671, 8latjass 17142 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ ((𝑄 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (((𝑄 𝑈) 𝑃) 𝑆) = ((𝑄 𝑈) (𝑃 𝑆)))
685, 48, 14, 19, 67syl13anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑈) 𝑃) 𝑆) = ((𝑄 𝑈) (𝑃 𝑆)))
6966, 68breqtrd 4711 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) ((𝑄 𝑈) (𝑃 𝑆)))
701, 20latmcl 17099 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
715, 11, 50, 70syl3anc 1366 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾))
721, 8latjcl 17098 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ ((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) ∈ (Base‘𝐾))
735, 71, 14, 72syl3anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) ∈ (Base‘𝐾))
741, 8, 9hlatjcl 34971 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
753, 12, 6, 74syl3anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
762, 8, 9hlatlej2 34980 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → 𝑆 (𝑃 𝑆))
773, 12, 17, 76syl3anc 1366 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑆 (𝑃 𝑆))
781, 2, 20latmlem2 17129 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾))) → (𝑆 (𝑃 𝑆) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑇) 𝑃) (𝑃 𝑆))))
795, 19, 50, 16, 78syl13anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑆 (𝑃 𝑆) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑇) 𝑃) (𝑃 𝑆))))
8077, 79mpd 15 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑇) 𝑃) (𝑃 𝑆)))
812, 8, 9hlatlej1 34979 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → 𝑃 (𝑃 𝑆))
823, 12, 17, 81syl3anc 1366 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑃 𝑆))
831, 2, 8, 20, 9atmod4i1 35470 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑆)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) = (((𝑄 𝑇) 𝑃) (𝑃 𝑆)))
843, 12, 11, 50, 82, 83syl131anc 1379 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) = (((𝑄 𝑇) 𝑃) (𝑃 𝑆)))
8580, 84breqtrrd 4713 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑇) (𝑃 𝑆)) 𝑃))
861, 20latmcom 17122 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
875, 11, 50, 86syl3anc 1366 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
88 simp12 1112 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄))
8987, 88eqbrtrd 4707 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑇) (𝑃 𝑆)) (𝑃 𝑄))
902, 8, 9hlatlej1 34979 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑃 (𝑃 𝑄))
913, 12, 6, 90syl3anc 1366 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑃 (𝑃 𝑄))
921, 2, 8latjle12 17109 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (((𝑄 𝑇) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → ((((𝑄 𝑇) (𝑃 𝑆)) (𝑃 𝑄) ∧ 𝑃 (𝑃 𝑄)) ↔ (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) (𝑃 𝑄)))
935, 71, 14, 75, 92syl13anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((((𝑄 𝑇) (𝑃 𝑆)) (𝑃 𝑄) ∧ 𝑃 (𝑃 𝑄)) ↔ (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) (𝑃 𝑄)))
9489, 91, 93mpbi2and 976 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) (𝑃 𝑆)) 𝑃) (𝑃 𝑄))
951, 2, 5, 22, 73, 75, 85, 94lattrd 17105 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 𝑄))
961, 8latjcl 17098 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑄 𝑈) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑈) (𝑃 𝑆)) ∈ (Base‘𝐾))
975, 48, 50, 96syl3anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) (𝑃 𝑆)) ∈ (Base‘𝐾))
981, 2, 20latlem12 17125 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((((𝑄 𝑇) 𝑃) 𝑆) ∈ (Base‘𝐾) ∧ ((𝑄 𝑈) (𝑃 𝑆)) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → (((((𝑄 𝑇) 𝑃) 𝑆) ((𝑄 𝑈) (𝑃 𝑆)) ∧ (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 𝑄)) ↔ (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄))))
995, 22, 97, 75, 98syl13anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((((𝑄 𝑇) 𝑃) 𝑆) ((𝑄 𝑈) (𝑃 𝑆)) ∧ (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 𝑄)) ↔ (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄))))
10069, 95, 99mpbi2and 976 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄)))
1011, 2, 8, 20, 9atmod3i1 35468 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑆)) → (𝑃 ((𝑃 𝑆) 𝑄)) = ((𝑃 𝑆) (𝑃 𝑄)))
1023, 12, 50, 46, 82, 101syl131anc 1379 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑃 𝑆) 𝑄)) = ((𝑃 𝑆) (𝑃 𝑄)))
103102oveq2d 6706 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) (𝑃 ((𝑃 𝑆) 𝑄))) = ((𝑄 𝑈) ((𝑃 𝑆) (𝑃 𝑄))))
1041, 8latj12 17143 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑄 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))) → ((𝑄 𝑈) (𝑃 ((𝑃 𝑆) 𝑄))) = (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))))
1055, 48, 14, 52, 104syl13anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) (𝑃 ((𝑃 𝑆) 𝑄))) = (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))))
1061, 2, 8, 20latmlej12 17138 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (𝑄 𝑈) (𝑃 𝑄))
1075, 46, 28, 14, 106syl13anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 𝑈) (𝑃 𝑄))
1081, 2, 8, 20, 9atmod1i1m 35462 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑈𝐴) ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) ∧ (𝑄 𝑈) (𝑃 𝑄)) → ((𝑄 𝑈) ((𝑃 𝑆) (𝑃 𝑄))) = (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄)))
1093, 26, 46, 50, 75, 107, 108syl231anc 1386 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) ((𝑃 𝑆) (𝑃 𝑄))) = (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄)))
110103, 105, 1093eqtr3rd 2694 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑈) (𝑃 𝑆)) (𝑃 𝑄)) = (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))))
111100, 110breqtrd 4711 . . . . . 6 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))))
1122, 8, 9hlatlej1 34979 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → 𝑄 (𝑄 𝑅))
1133, 6, 23, 112syl3anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑅))
1142, 8, 9hlatlej2 34980 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → 𝑈 (𝑅 𝑈))
1153, 23, 26, 114syl3anc 1366 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑅 𝑈))
1161, 20latmcl 17099 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾)) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾))
1175, 50, 11, 116syl3anc 1366 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ (Base‘𝐾))
1181, 8, 9hlatjcl 34971 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → (𝑅 𝑈) ∈ (Base‘𝐾))
1193, 23, 26, 118syl3anc 1366 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 𝑈) ∈ (Base‘𝐾))
1202, 8, 9hlatlej1 34979 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → 𝑄 (𝑄 𝑇))
1213, 6, 7, 120syl3anc 1366 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑄 (𝑄 𝑇))
1221, 2, 20latmlem2 17129 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾))) → (𝑄 (𝑄 𝑇) → ((𝑃 𝑆) 𝑄) ((𝑃 𝑆) (𝑄 𝑇))))
1235, 46, 11, 50, 122syl13anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑄 𝑇) → ((𝑃 𝑆) 𝑄) ((𝑃 𝑆) (𝑄 𝑇))))
124121, 123mpd 15 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑄) ((𝑃 𝑆) (𝑄 𝑇)))
125 simp13 1113 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈))
1261, 2, 5, 52, 117, 119, 124, 125lattrd 17105 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑄) (𝑅 𝑈))
1271, 2, 8latjle12 17109 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾) ∧ (𝑅 𝑈) ∈ (Base‘𝐾))) → ((𝑈 (𝑅 𝑈) ∧ ((𝑃 𝑆) 𝑄) (𝑅 𝑈)) ↔ (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈)))
1285, 28, 52, 119, 127syl13anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑈 (𝑅 𝑈) ∧ ((𝑃 𝑆) 𝑄) (𝑅 𝑈)) ↔ (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈)))
129115, 126, 128mpbi2and 976 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈))
1301, 8latjcl 17098 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾)) → (𝑈 ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾))
1315, 28, 52, 130syl3anc 1366 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾))
1321, 2, 20latmlem12 17130 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾)) ∧ ((𝑈 ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾) ∧ (𝑅 𝑈) ∈ (Base‘𝐾))) → ((𝑄 (𝑄 𝑅) ∧ (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈)) → (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))) ((𝑄 𝑅) (𝑅 𝑈))))
1335, 46, 25, 131, 119, 132syl122anc 1375 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 (𝑄 𝑅) ∧ (𝑈 ((𝑃 𝑆) 𝑄)) (𝑅 𝑈)) → (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))) ((𝑄 𝑅) (𝑅 𝑈))))
134113, 129, 133mp2and 715 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))) ((𝑄 𝑅) (𝑅 𝑈)))
1351, 2, 20latmle2 17124 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑄) 𝑄)
1365, 50, 46, 135syl3anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑃 𝑆) 𝑄) 𝑄)
1371, 2, 8, 20, 9atmod2i2 35466 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾)) ∧ ((𝑃 𝑆) 𝑄) 𝑄) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) = (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))))
1383, 26, 46, 52, 136, 137syl131anc 1379 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) = (𝑄 (𝑈 ((𝑃 𝑆) 𝑄))))
1392, 8, 9hlatlej2 34980 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → 𝑅 (𝑄 𝑅))
1403, 6, 23, 139syl3anc 1366 . . . . . . . . 9 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑅 (𝑄 𝑅))
1411, 2, 8, 20, 9atmod3i2 35469 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑅 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾)) ∧ 𝑅 (𝑄 𝑅)) → (𝑅 ((𝑄 𝑅) 𝑈)) = ((𝑄 𝑅) (𝑅 𝑈)))
1423, 26, 58, 25, 140, 141syl131anc 1379 . . . . . . . 8 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑅 ((𝑄 𝑅) 𝑈)) = ((𝑄 𝑅) (𝑅 𝑈)))
143134, 138, 1423brtr4d 4717 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) (𝑅 ((𝑄 𝑅) 𝑈)))
1441, 2, 8latjlej2 17113 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) ∈ (Base‘𝐾) ∧ (𝑅 ((𝑄 𝑅) 𝑈)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) (𝑅 ((𝑄 𝑅) 𝑈)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) (𝑃 (𝑅 ((𝑄 𝑅) 𝑈)))))
1455, 54, 60, 14, 144syl13anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑈) ((𝑃 𝑆) 𝑄)) (𝑅 ((𝑄 𝑅) 𝑈)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) (𝑃 (𝑅 ((𝑄 𝑅) 𝑈)))))
146143, 145mpd 15 . . . . . 6 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 ((𝑄 𝑈) ((𝑃 𝑆) 𝑄))) (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))))
1471, 2, 5, 22, 56, 62, 111, 146lattrd 17105 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))))
1481, 8latj13 17145 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾))) → (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))) = (((𝑄 𝑅) 𝑈) (𝑅 𝑃)))
1495, 14, 58, 30, 148syl13anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑃 (𝑅 ((𝑄 𝑅) 𝑈))) = (((𝑄 𝑅) 𝑈) (𝑅 𝑃)))
150147, 149breqtrd 4711 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) 𝑈) (𝑅 𝑃)))
1511, 2, 8, 20latmlej22 17140 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑄 𝑇) 𝑃) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑈 𝑆))
1525, 19, 16, 28, 151syl13anc 1368 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (𝑈 𝑆))
1531, 8latjcl 17098 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾) ∧ (𝑅 𝑃) ∈ (Base‘𝐾)) → (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∈ (Base‘𝐾))
1545, 30, 32, 153syl3anc 1366 . . . . 5 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∈ (Base‘𝐾))
1551, 2, 20latlem12 17125 . . . . 5 ((𝐾 ∈ Lat ∧ ((((𝑄 𝑇) 𝑃) 𝑆) ∈ (Base‘𝐾) ∧ (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾))) → (((((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∧ (((𝑄 𝑇) 𝑃) 𝑆) (𝑈 𝑆)) ↔ (((𝑄 𝑇) 𝑃) 𝑆) ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆))))
1565, 22, 154, 34, 155syl13anc 1368 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) 𝑈) (𝑅 𝑃)) ∧ (((𝑄 𝑇) 𝑃) 𝑆) (𝑈 𝑆)) ↔ (((𝑄 𝑇) 𝑃) 𝑆) ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆))))
157150, 152, 156mpbi2and 976 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆)))
1581, 2, 8, 20latmlej21 17139 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑄 𝑅) 𝑈) (𝑈 𝑆))
1595, 28, 25, 19, 158syl13anc 1368 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑅) 𝑈) (𝑈 𝑆))
1601, 2, 8, 20, 9atmod1i1m 35462 . . . 4 (((𝐾 ∈ HL ∧ 𝑈𝐴) ∧ ((𝑄 𝑅) ∈ (Base‘𝐾) ∧ (𝑅 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 𝑆) ∈ (Base‘𝐾)) ∧ ((𝑄 𝑅) 𝑈) (𝑈 𝑆)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) = ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆)))
1613, 26, 25, 32, 34, 159, 160syl231anc 1386 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) = ((((𝑄 𝑅) 𝑈) (𝑅 𝑃)) (𝑈 𝑆)))
162157, 161breqtrrd 4713 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))))
1632, 8, 9hlatlej2 34980 . . . . 5 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → 𝑈 (𝑇 𝑈))
1643, 7, 26, 163syl3anc 1366 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → 𝑈 (𝑇 𝑈))
1651, 2, 20latmlem2 17129 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → (𝑈 (𝑇 𝑈) → ((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈))))
1665, 28, 40, 25, 165syl13anc 1368 . . . 4 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (𝑈 (𝑇 𝑈) → ((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈))))
167164, 166mpd 15 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈)))
1681, 2, 8latjlej1 17112 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑄 𝑅) 𝑈) ∈ (Base‘𝐾) ∧ ((𝑄 𝑅) (𝑇 𝑈)) ∈ (Base‘𝐾) ∧ ((𝑅 𝑃) (𝑈 𝑆)) ∈ (Base‘𝐾))) → (((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆)))))
1695, 30, 42, 36, 168syl13anc 1368 . . 3 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) ((𝑄 𝑅) (𝑇 𝑈)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆)))))
170167, 169mpd 15 . 2 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑅) 𝑈) ((𝑅 𝑃) (𝑈 𝑆))) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
1711, 2, 5, 22, 38, 44, 162, 170lattrd 17105 1 (((𝐾 ∈ HL ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑃 𝑄) ∧ ((𝑃 𝑆) (𝑄 𝑇)) (𝑅 𝑈)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → (((𝑄 𝑇) 𝑃) 𝑆) (((𝑄 𝑅) (𝑇 𝑈)) ((𝑅 𝑃) (𝑈 𝑆))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   class class class wbr 4685  ‘cfv 5926  (class class class)co 6690  Basecbs 15904  lecple 15995  joincjn 16991  meetcmee 16992  Latclat 17092  Atomscatm 34868  HLchlt 34955 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-preset 16975  df-poset 16993  df-plt 17005  df-lub 17021  df-glb 17022  df-join 17023  df-meet 17024  df-p0 17086  df-lat 17093  df-clat 17155  df-oposet 34781  df-ol 34783  df-oml 34784  df-covers 34871  df-ats 34872  df-atl 34903  df-cvlat 34927  df-hlat 34956  df-psubsp 35107  df-pmap 35108  df-padd 35400 This theorem is referenced by:  dalawlem4  35478  dalawlem5  35479
 Copyright terms: Public domain W3C validator