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

Theorem 2lplnja 36624
Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 36625 in terms of atoms). (Contributed by NM, 12-Jul-2012.)
Hypotheses
Ref Expression
2lplnja.l = (le‘𝐾)
2lplnja.j = (join‘𝐾)
2lplnja.a 𝐴 = (Atoms‘𝐾)
2lplnja.v 𝑉 = (LVols‘𝐾)
Assertion
Ref Expression
2lplnja ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) = 𝑊)

Proof of Theorem 2lplnja
StepHypRef Expression
1 eqid 2825 . 2 (Base‘𝐾) = (Base‘𝐾)
2 2lplnja.l . 2 = (le‘𝐾)
3 simp11l 1278 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝐾 ∈ HL)
43hllatd 36369 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝐾 ∈ Lat)
5 simp121 1299 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑃𝐴)
6 simp122 1300 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑄𝐴)
7 2lplnja.j . . . . . 6 = (join‘𝐾)
8 2lplnja.a . . . . . 6 𝐴 = (Atoms‘𝐾)
91, 7, 8hlatjcl 36372 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
103, 5, 6, 9syl3anc 1365 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑃 𝑄) ∈ (Base‘𝐾))
11 simp123 1301 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑅𝐴)
121, 8atbase 36294 . . . . 5 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
1311, 12syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑅 ∈ (Base‘𝐾))
141, 7latjcl 17653 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
154, 10, 13, 14syl3anc 1365 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
16 simp2l1 1266 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑆𝐴)
17 simp2l2 1267 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑇𝐴)
181, 7, 8hlatjcl 36372 . . . . 5 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
193, 16, 17, 18syl3anc 1365 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑆 𝑇) ∈ (Base‘𝐾))
20 simp2l3 1268 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑈𝐴)
211, 8atbase 36294 . . . . 5 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
2220, 21syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑈 ∈ (Base‘𝐾))
231, 7latjcl 17653 . . . 4 ((𝐾 ∈ Lat ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑆 𝑇) 𝑈) ∈ (Base‘𝐾))
244, 19, 22, 23syl3anc 1365 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((𝑆 𝑇) 𝑈) ∈ (Base‘𝐾))
251, 7latjcl 17653 . . 3 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾) ∧ ((𝑆 𝑇) 𝑈) ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) ∈ (Base‘𝐾))
264, 15, 24, 25syl3anc 1365 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) ∈ (Base‘𝐾))
27 simp11r 1279 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑊𝑉)
28 2lplnja.v . . . 4 𝑉 = (LVols‘𝐾)
291, 28lvolbase 36583 . . 3 (𝑊𝑉𝑊 ∈ (Base‘𝐾))
3027, 29syl 17 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑊 ∈ (Base‘𝐾))
31 simp31 1203 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((𝑃 𝑄) 𝑅) 𝑊)
32 simp32 1204 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((𝑆 𝑇) 𝑈) 𝑊)
331, 2, 7latjle12 17664 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾) ∧ ((𝑆 𝑇) 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊) ↔ (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) 𝑊))
344, 15, 24, 30, 33syl13anc 1366 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊) ↔ (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) 𝑊))
3531, 32, 34mpbi2and 708 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) 𝑊)
361, 2, 7latlej2 17663 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → 𝑈 ((𝑆 𝑇) 𝑈))
374, 19, 22, 36syl3anc 1365 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑈 ((𝑆 𝑇) 𝑈))
381, 2, 4, 22, 24, 30, 37, 32lattrd 17660 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑈 𝑊)
391, 2, 7latjle12 17664 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑅) 𝑊𝑈 𝑊) ↔ (((𝑃 𝑄) 𝑅) 𝑈) 𝑊))
404, 15, 22, 30, 39syl13anc 1366 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((((𝑃 𝑄) 𝑅) 𝑊𝑈 𝑊) ↔ (((𝑃 𝑄) 𝑅) 𝑈) 𝑊))
4131, 38, 40mpbi2and 708 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) 𝑈) 𝑊)
4241ad2antrr 722 . . . . . 6 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑈) 𝑊)
433ad2antrr 722 . . . . . . 7 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝐾 ∈ HL)
443, 5, 63jca 1122 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴))
4544ad2antrr 722 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴))
4611, 20jca 512 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑅𝐴𝑈𝐴))
4746ad2antrr 722 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (𝑅𝐴𝑈𝐴))
48 simp13l 1282 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑃𝑄)
4948ad2antrr 722 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝑃𝑄)
50 simp13r 1283 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ¬ 𝑅 (𝑃 𝑄))
5150ad2antrr 722 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → ¬ 𝑅 (𝑃 𝑄))
52 simp33 1205 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))
5352ad2antrr 722 . . . . . . . . 9 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))
54 simplr 765 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝑆 ((𝑃 𝑄) 𝑅))
55 simpr 485 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝑇 ((𝑃 𝑄) 𝑅))
561, 8atbase 36294 . . . . . . . . . . . . . . . . . . 19 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
5716, 56syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑆 ∈ (Base‘𝐾))
581, 8atbase 36294 . . . . . . . . . . . . . . . . . . 19 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
5917, 58syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑇 ∈ (Base‘𝐾))
601, 2, 7latjle12 17664 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))) → ((𝑆 ((𝑃 𝑄) 𝑅) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ↔ (𝑆 𝑇) ((𝑃 𝑄) 𝑅)))
614, 57, 59, 15, 60syl13anc 1366 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((𝑆 ((𝑃 𝑄) 𝑅) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ↔ (𝑆 𝑇) ((𝑃 𝑄) 𝑅)))
6261ad2antrr 722 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → ((𝑆 ((𝑃 𝑄) 𝑅) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ↔ (𝑆 𝑇) ((𝑃 𝑄) 𝑅)))
6354, 55, 62mpbi2and 708 . . . . . . . . . . . . . . 15 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (𝑆 𝑇) ((𝑃 𝑄) 𝑅))
6463adantr 481 . . . . . . . . . . . . . 14 (((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) → (𝑆 𝑇) ((𝑃 𝑄) 𝑅))
65 simpr 485 . . . . . . . . . . . . . 14 (((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) → 𝑈 ((𝑃 𝑄) 𝑅))
661, 2, 7latjle12 17664 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Lat ∧ ((𝑆 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))) → (((𝑆 𝑇) ((𝑃 𝑄) 𝑅) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) ↔ ((𝑆 𝑇) 𝑈) ((𝑃 𝑄) 𝑅)))
674, 19, 22, 15, 66syl13anc 1366 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑆 𝑇) ((𝑃 𝑄) 𝑅) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) ↔ ((𝑆 𝑇) 𝑈) ((𝑃 𝑄) 𝑅)))
6867ad3antrrr 726 . . . . . . . . . . . . . 14 (((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) → (((𝑆 𝑇) ((𝑃 𝑄) 𝑅) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) ↔ ((𝑆 𝑇) 𝑈) ((𝑃 𝑄) 𝑅)))
6964, 65, 68mpbi2and 708 . . . . . . . . . . . . 13 (((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) → ((𝑆 𝑇) 𝑈) ((𝑃 𝑄) 𝑅))
70 simp2l 1193 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑆𝐴𝑇𝐴𝑈𝐴))
71 simp12 1198 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑃𝐴𝑄𝐴𝑅𝐴))
72 simp2rr 1237 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ¬ 𝑈 (𝑆 𝑇))
73 simp2rl 1236 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑆𝑇)
742, 7, 83at 36495 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) ∧ (¬ 𝑈 (𝑆 𝑇) ∧ 𝑆𝑇)) → (((𝑆 𝑇) 𝑈) ((𝑃 𝑄) 𝑅) ↔ ((𝑆 𝑇) 𝑈) = ((𝑃 𝑄) 𝑅)))
753, 70, 71, 72, 73, 74syl32anc 1372 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑆 𝑇) 𝑈) ((𝑃 𝑄) 𝑅) ↔ ((𝑆 𝑇) 𝑈) = ((𝑃 𝑄) 𝑅)))
7675ad3antrrr 726 . . . . . . . . . . . . 13 (((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) → (((𝑆 𝑇) 𝑈) ((𝑃 𝑄) 𝑅) ↔ ((𝑆 𝑇) 𝑈) = ((𝑃 𝑄) 𝑅)))
7769, 76mpbid 233 . . . . . . . . . . . 12 (((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) → ((𝑆 𝑇) 𝑈) = ((𝑃 𝑄) 𝑅))
7877eqcomd 2831 . . . . . . . . . . 11 (((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) ∧ 𝑈 ((𝑃 𝑄) 𝑅)) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈))
7978ex 413 . . . . . . . . . 10 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (𝑈 ((𝑃 𝑄) 𝑅) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈)))
8079necon3ad 3033 . . . . . . . . 9 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈) → ¬ 𝑈 ((𝑃 𝑄) 𝑅)))
8153, 80mpd 15 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → ¬ 𝑈 ((𝑃 𝑄) 𝑅))
822, 7, 8, 28lvoli2 36586 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑈𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑈 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) 𝑅) 𝑈) ∈ 𝑉)
8345, 47, 49, 51, 81, 82syl113anc 1376 . . . . . . 7 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑈) ∈ 𝑉)
8427ad2antrr 722 . . . . . . 7 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝑊𝑉)
852, 28lvolcmp 36622 . . . . . . 7 ((𝐾 ∈ HL ∧ (((𝑃 𝑄) 𝑅) 𝑈) ∈ 𝑉𝑊𝑉) → ((((𝑃 𝑄) 𝑅) 𝑈) 𝑊 ↔ (((𝑃 𝑄) 𝑅) 𝑈) = 𝑊))
8643, 83, 84, 85syl3anc 1365 . . . . . 6 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → ((((𝑃 𝑄) 𝑅) 𝑈) 𝑊 ↔ (((𝑃 𝑄) 𝑅) 𝑈) = 𝑊))
8742, 86mpbid 233 . . . . 5 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑈) = 𝑊)
881, 2, 7latjlej2 17668 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ ((𝑆 𝑇) 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))) → (𝑈 ((𝑆 𝑇) 𝑈) → (((𝑃 𝑄) 𝑅) 𝑈) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈))))
894, 22, 24, 15, 88syl13anc 1366 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑈 ((𝑆 𝑇) 𝑈) → (((𝑃 𝑄) 𝑅) 𝑈) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈))))
9037, 89mpd 15 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) 𝑈) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
9190ad2antrr 722 . . . . 5 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑈) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
9287, 91eqbrtrrd 5086 . . . 4 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝑊 (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
931, 7, 8hlatjcl 36372 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑈𝐴) → (𝑆 𝑈) ∈ (Base‘𝐾))
943, 16, 20, 93syl3anc 1365 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑆 𝑈) ∈ (Base‘𝐾))
951, 2, 7latlej2 17663 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑆 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 ((𝑆 𝑈) 𝑇))
964, 94, 59, 95syl3anc 1365 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑇 ((𝑆 𝑈) 𝑇))
977, 8hlatj32 36377 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) → ((𝑆 𝑇) 𝑈) = ((𝑆 𝑈) 𝑇))
983, 16, 17, 20, 97syl13anc 1366 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((𝑆 𝑇) 𝑈) = ((𝑆 𝑈) 𝑇))
9996, 98breqtrrd 5090 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑇 ((𝑆 𝑇) 𝑈))
1001, 2, 4, 59, 24, 30, 99, 32lattrd 17660 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑇 𝑊)
1011, 2, 7latjle12 17664 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑅) 𝑊𝑇 𝑊) ↔ (((𝑃 𝑄) 𝑅) 𝑇) 𝑊))
1024, 15, 59, 30, 101syl13anc 1366 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((((𝑃 𝑄) 𝑅) 𝑊𝑇 𝑊) ↔ (((𝑃 𝑄) 𝑅) 𝑇) 𝑊))
10331, 100, 102mpbi2and 708 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) 𝑇) 𝑊)
104103ad2antrr 722 . . . . . 6 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑇) 𝑊)
1053ad2antrr 722 . . . . . . 7 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝐾 ∈ HL)
10644ad2antrr 722 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴))
10711, 17jca 512 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑅𝐴𝑇𝐴))
108107ad2antrr 722 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → (𝑅𝐴𝑇𝐴))
10948ad2antrr 722 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝑃𝑄)
11050ad2antrr 722 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → ¬ 𝑅 (𝑃 𝑄))
111 simpr 485 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → ¬ 𝑇 ((𝑃 𝑄) 𝑅))
1122, 7, 8, 28lvoli2 36586 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑇𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) 𝑅) 𝑇) ∈ 𝑉)
113106, 108, 109, 110, 111, 112syl113anc 1376 . . . . . . 7 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑇) ∈ 𝑉)
11427ad2antrr 722 . . . . . . 7 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝑊𝑉)
1152, 28lvolcmp 36622 . . . . . . 7 ((𝐾 ∈ HL ∧ (((𝑃 𝑄) 𝑅) 𝑇) ∈ 𝑉𝑊𝑉) → ((((𝑃 𝑄) 𝑅) 𝑇) 𝑊 ↔ (((𝑃 𝑄) 𝑅) 𝑇) = 𝑊))
116105, 113, 114, 115syl3anc 1365 . . . . . 6 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → ((((𝑃 𝑄) 𝑅) 𝑇) 𝑊 ↔ (((𝑃 𝑄) 𝑅) 𝑇) = 𝑊))
117104, 116mpbid 233 . . . . 5 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑇) = 𝑊)
1181, 2, 7latjlej2 17668 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Base‘𝐾) ∧ ((𝑆 𝑇) 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))) → (𝑇 ((𝑆 𝑇) 𝑈) → (((𝑃 𝑄) 𝑅) 𝑇) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈))))
1194, 59, 24, 15, 118syl13anc 1366 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑇 ((𝑆 𝑇) 𝑈) → (((𝑃 𝑄) 𝑅) 𝑇) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈))))
12099, 119mpd 15 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) 𝑇) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
121120ad2antrr 722 . . . . 5 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑇) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
122117, 121eqbrtrrd 5086 . . . 4 ((((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑇 ((𝑃 𝑄) 𝑅)) → 𝑊 (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
12392, 122pm2.61dan 809 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ 𝑆 ((𝑃 𝑄) 𝑅)) → 𝑊 (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
1241, 7, 8hlatjcl 36372 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
1253, 17, 20, 124syl3anc 1365 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑇 𝑈) ∈ (Base‘𝐾))
1261, 2, 7latlej1 17662 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ (𝑇 𝑈) ∈ (Base‘𝐾)) → 𝑆 (𝑆 (𝑇 𝑈)))
1274, 57, 125, 126syl3anc 1365 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑆 (𝑆 (𝑇 𝑈)))
1281, 7latjass 17697 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → ((𝑆 𝑇) 𝑈) = (𝑆 (𝑇 𝑈)))
1294, 57, 59, 22, 128syl13anc 1366 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((𝑆 𝑇) 𝑈) = (𝑆 (𝑇 𝑈)))
130127, 129breqtrrd 5090 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑆 ((𝑆 𝑇) 𝑈))
1311, 2, 4, 57, 24, 30, 130, 32lattrd 17660 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑆 𝑊)
1321, 2, 7latjle12 17664 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 𝑄) 𝑅) 𝑊𝑆 𝑊) ↔ (((𝑃 𝑄) 𝑅) 𝑆) 𝑊))
1334, 15, 57, 30, 132syl13anc 1366 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → ((((𝑃 𝑄) 𝑅) 𝑊𝑆 𝑊) ↔ (((𝑃 𝑄) 𝑅) 𝑆) 𝑊))
13431, 131, 133mpbi2and 708 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) 𝑆) 𝑊)
135134adantr 481 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑆) 𝑊)
1363adantr 481 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → 𝐾 ∈ HL)
13744adantr 481 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴))
13811, 16jca 512 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑅𝐴𝑆𝐴))
139138adantr 481 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → (𝑅𝐴𝑆𝐴))
14048adantr 481 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → 𝑃𝑄)
14150adantr 481 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → ¬ 𝑅 (𝑃 𝑄))
142 simpr 485 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → ¬ 𝑆 ((𝑃 𝑄) 𝑅))
1432, 7, 8, 28lvoli2 36586 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉)
144137, 139, 140, 141, 142, 143syl113anc 1376 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉)
14527adantr 481 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → 𝑊𝑉)
1462, 28lvolcmp 36622 . . . . . 6 ((𝐾 ∈ HL ∧ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉𝑊𝑉) → ((((𝑃 𝑄) 𝑅) 𝑆) 𝑊 ↔ (((𝑃 𝑄) 𝑅) 𝑆) = 𝑊))
147136, 144, 145, 146syl3anc 1365 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → ((((𝑃 𝑄) 𝑅) 𝑆) 𝑊 ↔ (((𝑃 𝑄) 𝑅) 𝑆) = 𝑊))
148135, 147mpbid 233 . . . 4 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑆) = 𝑊)
1491, 2, 7latjlej2 17668 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑆 𝑇) 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))) → (𝑆 ((𝑆 𝑇) 𝑈) → (((𝑃 𝑄) 𝑅) 𝑆) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈))))
1504, 57, 24, 15, 149syl13anc 1366 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (𝑆 ((𝑆 𝑇) 𝑈) → (((𝑃 𝑄) 𝑅) 𝑆) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈))))
151130, 150mpd 15 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) 𝑆) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
152151adantr 481 . . . 4 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑆) (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
153148, 152eqbrtrrd 5086 . . 3 (((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → 𝑊 (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
154123, 153pm2.61dan 809 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → 𝑊 (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)))
1551, 2, 4, 26, 30, 35, 154latasymd 17659 1 ((((𝐾 ∈ HL ∧ 𝑊𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) ∧ ((𝑆𝐴𝑇𝐴𝑈𝐴) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ (((𝑃 𝑄) 𝑅) 𝑊 ∧ ((𝑆 𝑇) 𝑈) 𝑊 ∧ ((𝑃 𝑄) 𝑅) ≠ ((𝑆 𝑇) 𝑈))) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) = 𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wne 3020   class class class wbr 5062  cfv 6351  (class class class)co 7151  Basecbs 16475  lecple 16564  joincjn 17546  Latclat 17647  Atomscatm 36268  HLchlt 36355  LVolsclvol 36498
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 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  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 36181  df-ol 36183  df-oml 36184  df-covers 36271  df-ats 36272  df-atl 36303  df-cvlat 36327  df-hlat 36356  df-llines 36503  df-lplanes 36504  df-lvols 36505
This theorem is referenced by:  2lplnj  36625
  Copyright terms: Public domain W3C validator