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

Theorem 4atlem12 35216
Description: Lemma for 4at 35217. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.)
Hypotheses
Ref Expression
4at.l = (le‘𝐾)
4at.j = (join‘𝐾)
4at.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
4atlem12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) (𝑅 𝑆)) ((𝑇 𝑈) (𝑉 𝑊)) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊))))

Proof of Theorem 4atlem12
StepHypRef Expression
1 simpl11 1156 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝐾 ∈ HL)
2 hllat 34968 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ Lat)
31, 2syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝐾 ∈ Lat)
4 simpl12 1157 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑃𝐴)
5 eqid 2651 . . . . . . 7 (Base‘𝐾) = (Base‘𝐾)
6 4at.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
75, 6atbase 34894 . . . . . 6 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
84, 7syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑃 ∈ (Base‘𝐾))
9 simpl13 1158 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑄𝐴)
105, 6atbase 34894 . . . . . 6 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
119, 10syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑄 ∈ (Base‘𝐾))
12 simpl23 1161 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑇𝐴)
13 simpl31 1162 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑈𝐴)
14 4at.j . . . . . . . 8 = (join‘𝐾)
155, 14, 6hlatjcl 34971 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
161, 12, 13, 15syl3anc 1366 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑇 𝑈) ∈ (Base‘𝐾))
17 simpl32 1163 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑉𝐴)
18 simpl33 1164 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑊𝐴)
195, 14, 6hlatjcl 34971 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑉𝐴𝑊𝐴) → (𝑉 𝑊) ∈ (Base‘𝐾))
201, 17, 18, 19syl3anc 1366 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑉 𝑊) ∈ (Base‘𝐾))
215, 14latjcl 17098 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ (𝑉 𝑊) ∈ (Base‘𝐾)) → ((𝑇 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))
223, 16, 20, 21syl3anc 1366 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑇 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))
23 4at.l . . . . . 6 = (le‘𝐾)
245, 23, 14latjle12 17109 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑇 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))) → ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ↔ (𝑃 𝑄) ((𝑇 𝑈) (𝑉 𝑊))))
253, 8, 11, 22, 24syl13anc 1368 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ↔ (𝑃 𝑄) ((𝑇 𝑈) (𝑉 𝑊))))
26 simpl21 1159 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑅𝐴)
275, 6atbase 34894 . . . . . 6 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
2826, 27syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑅 ∈ (Base‘𝐾))
29 simpl22 1160 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑆𝐴)
305, 6atbase 34894 . . . . . 6 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
3129, 30syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑆 ∈ (Base‘𝐾))
325, 23, 14latjle12 17109 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾) ∧ ((𝑇 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))) → ((𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))) ↔ (𝑅 𝑆) ((𝑇 𝑈) (𝑉 𝑊))))
333, 28, 31, 22, 32syl13anc 1368 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))) ↔ (𝑅 𝑆) ((𝑇 𝑈) (𝑉 𝑊))))
3425, 33anbi12d 747 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) ↔ ((𝑃 𝑄) ((𝑇 𝑈) (𝑉 𝑊)) ∧ (𝑅 𝑆) ((𝑇 𝑈) (𝑉 𝑊)))))
35 simpl1 1084 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴))
365, 14, 6hlatjcl 34971 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
3735, 36syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑃 𝑄) ∈ (Base‘𝐾))
385, 14, 6hlatjcl 34971 . . . . 5 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) → (𝑅 𝑆) ∈ (Base‘𝐾))
391, 26, 29, 38syl3anc 1366 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑅 𝑆) ∈ (Base‘𝐾))
405, 23, 14latjle12 17109 . . . 4 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑅 𝑆) ∈ (Base‘𝐾) ∧ ((𝑇 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))) → (((𝑃 𝑄) ((𝑇 𝑈) (𝑉 𝑊)) ∧ (𝑅 𝑆) ((𝑇 𝑈) (𝑉 𝑊))) ↔ ((𝑃 𝑄) (𝑅 𝑆)) ((𝑇 𝑈) (𝑉 𝑊))))
413, 37, 39, 22, 40syl13anc 1368 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) ((𝑇 𝑈) (𝑉 𝑊)) ∧ (𝑅 𝑆) ((𝑇 𝑈) (𝑉 𝑊))) ↔ ((𝑃 𝑄) (𝑅 𝑆)) ((𝑇 𝑈) (𝑉 𝑊))))
4234, 41bitrd 268 . 2 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) ↔ ((𝑃 𝑄) (𝑅 𝑆)) ((𝑇 𝑈) (𝑉 𝑊))))
43 simp1l 1105 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑃 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
44 simp1r 1106 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑃 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)))
45 simp2 1082 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑃 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ¬ 𝑃 ((𝑈 𝑉) 𝑊))
46 simp3 1083 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑃 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))))
4723, 14, 64atlem12b 35215 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑃 ((𝑈 𝑉) 𝑊)) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))
4843, 44, 45, 46, 47syl121anc 1371 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑃 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))
49483exp 1283 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑃 ((𝑈 𝑉) 𝑊) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))))
505, 14latj4rot 17149 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → ((𝑄 𝑅) (𝑆 𝑃)) = ((𝑃 𝑄) (𝑅 𝑆)))
513, 11, 28, 31, 8, 50syl122anc 1375 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑄 𝑅) (𝑆 𝑃)) = ((𝑃 𝑄) (𝑅 𝑆)))
52513ad2ant1 1102 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑄 𝑅) (𝑆 𝑃)) = ((𝑃 𝑄) (𝑅 𝑆)))
531, 9, 263jca 1261 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴))
5429, 4, 123jca 1261 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑆𝐴𝑃𝐴𝑇𝐴))
55 simpl3 1086 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑈𝐴𝑉𝐴𝑊𝐴))
5653, 54, 553jca 1261 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑃𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
57563ad2ant1 1102 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑃𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
58 simpr 476 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)))
5923, 14, 64noncolr3 35057 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑄𝑅 ∧ ¬ 𝑆 (𝑄 𝑅) ∧ ¬ 𝑃 ((𝑄 𝑅) 𝑆)))
6035, 26, 29, 58, 59syl121anc 1371 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑄𝑅 ∧ ¬ 𝑆 (𝑄 𝑅) ∧ ¬ 𝑃 ((𝑄 𝑅) 𝑆)))
61603ad2ant1 1102 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → (𝑄𝑅 ∧ ¬ 𝑆 (𝑄 𝑅) ∧ ¬ 𝑃 ((𝑄 𝑅) 𝑆)))
62 simp2 1082 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ¬ 𝑄 ((𝑈 𝑉) 𝑊))
63 simprlr 820 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → 𝑄 ((𝑇 𝑈) (𝑉 𝑊)))
64 simprrl 821 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → 𝑅 ((𝑇 𝑈) (𝑉 𝑊)))
6563, 64jca 553 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → (𝑄 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑇 𝑈) (𝑉 𝑊))))
66 simprrr 822 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))
67 simprll 819 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → 𝑃 ((𝑇 𝑈) (𝑉 𝑊)))
6865, 66, 67jca32 557 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑄 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑆 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑃 ((𝑇 𝑈) (𝑉 𝑊)))))
69683adant2 1100 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑄 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑆 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑃 ((𝑇 𝑈) (𝑉 𝑊)))))
7023, 14, 64atlem12b 35215 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑃𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ ((𝑄𝑅 ∧ ¬ 𝑆 (𝑄 𝑅) ∧ ¬ 𝑃 ((𝑄 𝑅) 𝑆)) ∧ ¬ 𝑄 ((𝑈 𝑉) 𝑊)) ∧ ((𝑄 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑆 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑃 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑄 𝑅) (𝑆 𝑃)) = ((𝑇 𝑈) (𝑉 𝑊)))
7157, 61, 62, 69, 70syl121anc 1371 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑄 𝑅) (𝑆 𝑃)) = ((𝑇 𝑈) (𝑉 𝑊)))
7252, 71eqtr3d 2687 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))
73723exp 1283 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑄 ((𝑈 𝑉) 𝑊) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))))
7449, 73jaod 394 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((¬ 𝑃 ((𝑈 𝑉) 𝑊) ∨ ¬ 𝑄 ((𝑈 𝑉) 𝑊)) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))))
755, 14latjcom 17106 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑅 𝑆) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑅 𝑆) (𝑃 𝑄)))
763, 37, 39, 75syl3anc 1366 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑅 𝑆) (𝑃 𝑄)))
77763ad2ant1 1102 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑅 𝑆) (𝑃 𝑄)))
781, 26, 293jca 1261 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴))
794, 9, 123jca 1261 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑃𝐴𝑄𝐴𝑇𝐴))
8078, 79, 553jca 1261 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) ∧ (𝑃𝐴𝑄𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
81803ad2ant1 1102 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) ∧ (𝑃𝐴𝑄𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
8223, 14, 64noncolr2 35058 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑅𝑆 ∧ ¬ 𝑃 (𝑅 𝑆) ∧ ¬ 𝑄 ((𝑅 𝑆) 𝑃)))
8335, 26, 29, 58, 82syl121anc 1371 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑅𝑆 ∧ ¬ 𝑃 (𝑅 𝑆) ∧ ¬ 𝑄 ((𝑅 𝑆) 𝑃)))
84833ad2ant1 1102 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → (𝑅𝑆 ∧ ¬ 𝑃 (𝑅 𝑆) ∧ ¬ 𝑄 ((𝑅 𝑆) 𝑃)))
85 simp2 1082 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ¬ 𝑅 ((𝑈 𝑉) 𝑊))
86 simprr 811 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))
87 simprl 809 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → (𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))))
8886, 87jca 553 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊)))))
89883adant2 1100 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊)))))
9023, 14, 64atlem12b 35215 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) ∧ (𝑃𝐴𝑄𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ ((𝑅𝑆 ∧ ¬ 𝑃 (𝑅 𝑆) ∧ ¬ 𝑄 ((𝑅 𝑆) 𝑃)) ∧ ¬ 𝑅 ((𝑈 𝑉) 𝑊)) ∧ ((𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑅 𝑆) (𝑃 𝑄)) = ((𝑇 𝑈) (𝑉 𝑊)))
9181, 84, 85, 89, 90syl121anc 1371 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑅 𝑆) (𝑃 𝑄)) = ((𝑇 𝑈) (𝑉 𝑊)))
9277, 91eqtrd 2685 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))
93923exp 1283 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑅 ((𝑈 𝑉) 𝑊) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))))
945, 14latj4rot 17149 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑆 𝑃) (𝑄 𝑅)))
953, 8, 11, 28, 31, 94syl122anc 1375 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑆 𝑃) (𝑄 𝑅)))
96953ad2ant1 1102 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑆 𝑃) (𝑄 𝑅)))
971, 29, 43jca 1261 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝐾 ∈ HL ∧ 𝑆𝐴𝑃𝐴))
989, 26, 123jca 1261 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑄𝐴𝑅𝐴𝑇𝐴))
9997, 98, 553jca 1261 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝐾 ∈ HL ∧ 𝑆𝐴𝑃𝐴) ∧ (𝑄𝐴𝑅𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
100993ad2ant1 1102 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝐾 ∈ HL ∧ 𝑆𝐴𝑃𝐴) ∧ (𝑄𝐴𝑅𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
10123, 14, 64noncolr1 35059 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑆𝑃 ∧ ¬ 𝑄 (𝑆 𝑃) ∧ ¬ 𝑅 ((𝑆 𝑃) 𝑄)))
10235, 26, 29, 58, 101syl121anc 1371 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑆𝑃 ∧ ¬ 𝑄 (𝑆 𝑃) ∧ ¬ 𝑅 ((𝑆 𝑃) 𝑄)))
1031023ad2ant1 1102 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → (𝑆𝑃 ∧ ¬ 𝑄 (𝑆 𝑃) ∧ ¬ 𝑅 ((𝑆 𝑃) 𝑄)))
104 simp2 1082 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ¬ 𝑆 ((𝑈 𝑉) 𝑊))
10566, 67jca 553 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → (𝑆 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑃 ((𝑇 𝑈) (𝑉 𝑊))))
106105, 63, 64jca32 557 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑆 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑃 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑄 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑇 𝑈) (𝑉 𝑊)))))
1071063adant2 1100 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑆 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑃 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑄 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑇 𝑈) (𝑉 𝑊)))))
10823, 14, 64atlem12b 35215 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑆𝐴𝑃𝐴) ∧ (𝑄𝐴𝑅𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ ((𝑆𝑃 ∧ ¬ 𝑄 (𝑆 𝑃) ∧ ¬ 𝑅 ((𝑆 𝑃) 𝑄)) ∧ ¬ 𝑆 ((𝑈 𝑉) 𝑊)) ∧ ((𝑆 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑃 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑄 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑆 𝑃) (𝑄 𝑅)) = ((𝑇 𝑈) (𝑉 𝑊)))
109100, 103, 104, 107, 108syl121anc 1371 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑆 𝑃) (𝑄 𝑅)) = ((𝑇 𝑈) (𝑉 𝑊)))
11096, 109eqtrd 2685 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑈 𝑉) 𝑊) ∧ ((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊))))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))
1111103exp 1283 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑆 ((𝑈 𝑉) 𝑊) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))))
11293, 111jaod 394 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((¬ 𝑅 ((𝑈 𝑉) 𝑊) ∨ ¬ 𝑆 ((𝑈 𝑉) 𝑊)) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊)))))
11326, 29, 133jca 1261 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑅𝐴𝑆𝐴𝑈𝐴))
11417, 18jca 553 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑉𝐴𝑊𝐴))
11523, 14, 64atlem3 35200 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑈𝐴) ∧ (𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((¬ 𝑃 ((𝑈 𝑉) 𝑊) ∨ ¬ 𝑄 ((𝑈 𝑉) 𝑊)) ∨ (¬ 𝑅 ((𝑈 𝑉) 𝑊) ∨ ¬ 𝑆 ((𝑈 𝑉) 𝑊))))
11635, 113, 114, 58, 115syl31anc 1369 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((¬ 𝑃 ((𝑈 𝑉) 𝑊) ∨ ¬ 𝑄 ((𝑈 𝑉) 𝑊)) ∨ (¬ 𝑅 ((𝑈 𝑉) 𝑊) ∨ ¬ 𝑆 ((𝑈 𝑉) 𝑊))))
11774, 112, 116mpjaod 395 . 2 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑇 𝑈) (𝑉 𝑊))) ∧ (𝑅 ((𝑇 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑇 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊))))
11842, 117sylbird 250 1 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) (𝑅 𝑆)) ((𝑇 𝑈) (𝑉 𝑊)) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑇 𝑈) (𝑉 𝑊))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823   class class class wbr 4685  cfv 5926  (class class class)co 6690  Basecbs 15904  lecple 15995  joincjn 16991  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-3or 1055  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-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-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-llines 35102  df-lplanes 35103  df-lvols 35104
This theorem is referenced by:  4at  35217
  Copyright terms: Public domain W3C validator