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

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

Proof of Theorem 4atlem11
StepHypRef Expression
1 3anass 1092 . . . 4 ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) ↔ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ (𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))))
2 simpl11 1245 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝐾 ∈ HL)
32hllatd 39073 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝐾 ∈ Lat)
4 simpl2l 1223 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑅𝐴)
5 eqid 2726 . . . . . . . 8 (Base‘𝐾) = (Base‘𝐾)
6 4at.a . . . . . . . 8 𝐴 = (Atoms‘𝐾)
75, 6atbase 38998 . . . . . . 7 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
84, 7syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑅 ∈ (Base‘𝐾))
9 simpl2r 1224 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑆𝐴)
105, 6atbase 38998 . . . . . . 7 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
119, 10syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑆 ∈ (Base‘𝐾))
12 simpl12 1246 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑃𝐴)
13 simpl31 1251 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑈𝐴)
14 4at.j . . . . . . . . 9 = (join‘𝐾)
155, 14, 6hlatjcl 39076 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → (𝑃 𝑈) ∈ (Base‘𝐾))
162, 12, 13, 15syl3anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑃 𝑈) ∈ (Base‘𝐾))
17 simpl32 1252 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑉𝐴)
18 simpl33 1253 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑊𝐴)
195, 14, 6hlatjcl 39076 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑉𝐴𝑊𝐴) → (𝑉 𝑊) ∈ (Base‘𝐾))
202, 17, 18, 19syl3anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑉 𝑊) ∈ (Base‘𝐾))
215, 14latjcl 18457 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ (𝑉 𝑊) ∈ (Base‘𝐾)) → ((𝑃 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))
223, 16, 20, 21syl3anc 1368 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑃 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))
23 4at.l . . . . . . 7 = (le‘𝐾)
245, 23, 14latjle12 18468 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾) ∧ ((𝑃 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))) → ((𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) ↔ (𝑅 𝑆) ((𝑃 𝑈) (𝑉 𝑊))))
253, 8, 11, 22, 24syl13anc 1369 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) ↔ (𝑅 𝑆) ((𝑃 𝑈) (𝑉 𝑊))))
2625anbi2d 628 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ (𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) ↔ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ (𝑅 𝑆) ((𝑃 𝑈) (𝑉 𝑊)))))
271, 26bitrid 282 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) ↔ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ (𝑅 𝑆) ((𝑃 𝑈) (𝑉 𝑊)))))
28 simpl13 1247 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑄𝐴)
295, 6atbase 38998 . . . . 5 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
3028, 29syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑄 ∈ (Base‘𝐾))
315, 14, 6hlatjcl 39076 . . . . 5 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) → (𝑅 𝑆) ∈ (Base‘𝐾))
322, 4, 9, 31syl3anc 1368 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑅 𝑆) ∈ (Base‘𝐾))
335, 23, 14latjle12 18468 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑅 𝑆) ∈ (Base‘𝐾) ∧ ((𝑃 𝑈) (𝑉 𝑊)) ∈ (Base‘𝐾))) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ (𝑅 𝑆) ((𝑃 𝑈) (𝑉 𝑊))) ↔ (𝑄 (𝑅 𝑆)) ((𝑃 𝑈) (𝑉 𝑊))))
343, 30, 32, 22, 33syl13anc 1369 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ (𝑅 𝑆) ((𝑃 𝑈) (𝑉 𝑊))) ↔ (𝑄 (𝑅 𝑆)) ((𝑃 𝑈) (𝑉 𝑊))))
3527, 34bitrd 278 . 2 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) ↔ (𝑄 (𝑅 𝑆)) ((𝑃 𝑈) (𝑉 𝑊))))
36 simpl1 1188 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴))
37 simpl2 1189 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑅𝐴𝑆𝐴))
3817, 18jca 510 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑉𝐴𝑊𝐴))
39 simpr 483 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)))
4023, 14, 64atlem3a 39307 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑄 ((𝑃 𝑉) 𝑊) ∨ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∨ ¬ 𝑆 ((𝑃 𝑉) 𝑊)))
4136, 37, 38, 39, 40syl31anc 1370 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑄 ((𝑃 𝑉) 𝑊) ∨ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∨ ¬ 𝑆 ((𝑃 𝑉) 𝑊)))
42 simp1l 1194 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
43 simp1r 1195 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)))
44 simp2 1134 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ¬ 𝑄 ((𝑃 𝑉) 𝑊))
45 simp3 1135 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))))
4623, 14, 64atlem11b 39318 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ ((𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ ¬ 𝑄 ((𝑃 𝑉) 𝑊)) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))
4742, 43, 44, 45, 46syl121anc 1372 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑄 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))
48473exp 1116 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑄 ((𝑃 𝑉) 𝑊) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))))
4923ad2ant1 1130 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝐾 ∈ HL)
50123ad2ant1 1130 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑃𝐴)
51283ad2ant1 1130 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑄𝐴)
5243ad2ant1 1130 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑅𝐴)
5393ad2ant1 1130 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑆𝐴)
5414, 6hlatj4 39083 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑅) (𝑄 𝑆)))
5549, 50, 51, 52, 53, 54syl122anc 1376 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑅) (𝑄 𝑆)))
5649, 50, 523jca 1125 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴))
5751, 53jca 510 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑄𝐴𝑆𝐴))
58 simp1l3 1265 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑈𝐴𝑉𝐴𝑊𝐴))
59 simp1r2 1267 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ¬ 𝑅 (𝑃 𝑄))
6023, 14, 64atlem0be 39305 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ ¬ 𝑅 (𝑃 𝑄)) → 𝑃𝑅)
6149, 50, 51, 52, 59, 60syl131anc 1380 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑃𝑅)
62 simp1r1 1266 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑃𝑄)
6323, 14, 64atlem0ae 39304 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ¬ 𝑄 (𝑃 𝑅))
6449, 50, 51, 52, 62, 59, 63syl132anc 1385 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ¬ 𝑄 (𝑃 𝑅))
65 simp1r3 1268 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ¬ 𝑆 ((𝑃 𝑄) 𝑅))
6614, 6hlatj32 39081 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ((𝑃 𝑄) 𝑅) = ((𝑃 𝑅) 𝑄))
6749, 50, 51, 52, 66syl13anc 1369 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) 𝑅) = ((𝑃 𝑅) 𝑄))
6867breq2d 5156 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑆 ((𝑃 𝑄) 𝑅) ↔ 𝑆 ((𝑃 𝑅) 𝑄)))
6965, 68mtbid 323 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ¬ 𝑆 ((𝑃 𝑅) 𝑄))
7061, 64, 693jca 1125 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑃𝑅 ∧ ¬ 𝑄 (𝑃 𝑅) ∧ ¬ 𝑆 ((𝑃 𝑅) 𝑄)))
71 simp2 1134 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ¬ 𝑅 ((𝑃 𝑉) 𝑊))
72 simp32 1207 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑅 ((𝑃 𝑈) (𝑉 𝑊)))
73 simp31 1206 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑄 ((𝑃 𝑈) (𝑉 𝑊)))
74 simp33 1208 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))
7523, 14, 64atlem11b 39318 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴) ∧ (𝑄𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ ((𝑃𝑅 ∧ ¬ 𝑄 (𝑃 𝑅) ∧ ¬ 𝑆 ((𝑃 𝑅) 𝑄)) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊)) ∧ (𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑅) (𝑄 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))
7656, 57, 58, 70, 71, 72, 73, 74, 75syl323anc 1397 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑅) (𝑄 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))
7755, 76eqtrd 2766 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))
78773exp 1116 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑅 ((𝑃 𝑉) 𝑊) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))))
795, 6atbase 38998 . . . . . . . . . 10 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
8012, 79syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑃 ∈ (Base‘𝐾))
815, 14latj4rot 18508 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑆 𝑃) (𝑄 𝑅)))
823, 80, 30, 8, 11, 81syl122anc 1376 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑆 𝑃) (𝑄 𝑅)))
8314, 6hlatjcom 39077 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑃𝐴) → (𝑆 𝑃) = (𝑃 𝑆))
842, 9, 12, 83syl3anc 1368 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑆 𝑃) = (𝑃 𝑆))
8584oveq1d 7429 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑆 𝑃) (𝑄 𝑅)) = ((𝑃 𝑆) (𝑄 𝑅)))
8682, 85eqtrd 2766 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑆) (𝑄 𝑅)))
87863ad2ant1 1130 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑆) (𝑄 𝑅)))
882, 12, 93jca 1125 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴))
8928, 4jca 510 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑄𝐴𝑅𝐴))
90 simpl3 1190 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑈𝐴𝑉𝐴𝑊𝐴))
9188, 89, 903jca 1125 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) ∧ (𝑄𝐴𝑅𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
92913ad2ant1 1130 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) ∧ (𝑄𝐴𝑅𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)))
9323, 14, 64noncolr1 39165 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑆𝑃 ∧ ¬ 𝑄 (𝑆 𝑃) ∧ ¬ 𝑅 ((𝑆 𝑃) 𝑄)))
9436, 37, 39, 93syl3anc 1368 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑆𝑃 ∧ ¬ 𝑄 (𝑆 𝑃) ∧ ¬ 𝑅 ((𝑆 𝑃) 𝑄)))
95 necom 2984 . . . . . . . . . . 11 (𝑆𝑃𝑃𝑆)
9695a1i 11 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑆𝑃𝑃𝑆))
9784breq2d 5156 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑄 (𝑆 𝑃) ↔ 𝑄 (𝑃 𝑆)))
9897notbid 317 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑄 (𝑆 𝑃) ↔ ¬ 𝑄 (𝑃 𝑆)))
9984oveq1d 7429 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑆 𝑃) 𝑄) = ((𝑃 𝑆) 𝑄))
10099breq2d 5156 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑅 ((𝑆 𝑃) 𝑄) ↔ 𝑅 ((𝑃 𝑆) 𝑄)))
101100notbid 317 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑅 ((𝑆 𝑃) 𝑄) ↔ ¬ 𝑅 ((𝑃 𝑆) 𝑄)))
10296, 98, 1013anbi123d 1433 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑆𝑃 ∧ ¬ 𝑄 (𝑆 𝑃) ∧ ¬ 𝑅 ((𝑆 𝑃) 𝑄)) ↔ (𝑃𝑆 ∧ ¬ 𝑄 (𝑃 𝑆) ∧ ¬ 𝑅 ((𝑃 𝑆) 𝑄))))
10394, 102mpbid 231 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑃𝑆 ∧ ¬ 𝑄 (𝑃 𝑆) ∧ ¬ 𝑅 ((𝑃 𝑆) 𝑄)))
1041033ad2ant1 1130 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑃𝑆 ∧ ¬ 𝑄 (𝑃 𝑆) ∧ ¬ 𝑅 ((𝑃 𝑆) 𝑄)))
105 simp2 1134 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ¬ 𝑆 ((𝑃 𝑉) 𝑊))
106 simpr3 1193 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))
107 simpr1 1191 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑄 ((𝑃 𝑈) (𝑉 𝑊)))
108 simpr2 1192 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → 𝑅 ((𝑃 𝑈) (𝑉 𝑊)))
109106, 107, 1083jca 1125 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑆 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊))))
1101093adant2 1128 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → (𝑆 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊))))
11123, 14, 64atlem11b 39318 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) ∧ (𝑄𝐴𝑅𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ ((𝑃𝑆 ∧ ¬ 𝑄 (𝑃 𝑆) ∧ ¬ 𝑅 ((𝑃 𝑆) 𝑄)) ∧ ¬ 𝑆 ((𝑃 𝑉) 𝑊)) ∧ (𝑆 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑆) (𝑄 𝑅)) = ((𝑃 𝑈) (𝑉 𝑊)))
11292, 104, 105, 110, 111syl121anc 1372 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑆) (𝑄 𝑅)) = ((𝑃 𝑈) (𝑉 𝑊)))
11387, 112eqtrd 2766 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) ∧ ¬ 𝑆 ((𝑃 𝑉) 𝑊) ∧ (𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊)))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))
1141133exp 1116 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (¬ 𝑆 ((𝑃 𝑉) 𝑊) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))))
11548, 78, 1143jaod 1426 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((¬ 𝑄 ((𝑃 𝑉) 𝑊) ∨ ¬ 𝑅 ((𝑃 𝑉) 𝑊) ∨ ¬ 𝑆 ((𝑃 𝑉) 𝑊)) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊)))))
11641, 115mpd 15 . 2 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑄 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑅 ((𝑃 𝑈) (𝑉 𝑊)) ∧ 𝑆 ((𝑃 𝑈) (𝑉 𝑊))) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊))))
11735, 116sylbird 259 1 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑈𝐴𝑉𝐴𝑊𝐴)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑄 (𝑅 𝑆)) ((𝑃 𝑈) (𝑉 𝑊)) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑈) (𝑉 𝑊))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3o 1083  w3a 1084   = wceq 1534  wcel 2099  wne 2930   class class class wbr 5144  cfv 6544  (class class class)co 7414  Basecbs 17206  lecple 17266  joincjn 18329  Latclat 18449  Atomscatm 38972  HLchlt 39059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7736
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366  df-rab 3421  df-v 3465  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-iun 4996  df-br 5145  df-opab 5207  df-mpt 5228  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7370  df-ov 7417  df-oprab 7418  df-proset 18313  df-poset 18331  df-plt 18348  df-lub 18364  df-glb 18365  df-join 18366  df-meet 18367  df-p0 18443  df-lat 18450  df-clat 18517  df-oposet 38885  df-ol 38887  df-oml 38888  df-covers 38975  df-ats 38976  df-atl 39007  df-cvlat 39031  df-hlat 39060  df-llines 39208  df-lplanes 39209  df-lvols 39210
This theorem is referenced by:  4atlem12b  39321
  Copyright terms: Public domain W3C validator