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

Theorem cdleme11c 36039
Description: Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 36048. (Contributed by NM, 13-Jun-2012.)
Hypotheses
Ref Expression
cdleme11.l = (le‘𝐾)
cdleme11.j = (join‘𝐾)
cdleme11.m = (meet‘𝐾)
cdleme11.a 𝐴 = (Atoms‘𝐾)
cdleme11.h 𝐻 = (LHyp‘𝐾)
cdleme11.u 𝑈 = ((𝑃 𝑄) 𝑊)
Assertion
Ref Expression
cdleme11c ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → ¬ 𝑃 (𝑆 𝑇))

Proof of Theorem cdleme11c
StepHypRef Expression
1 simp3l 1251 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → ¬ 𝑆 (𝑃 𝑄))
2 simp11l 1376 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝐾 ∈ HL)
3 simp12l 1378 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑃𝐴)
4 simp11 1253 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
5 simp12 1254 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
6 simp13 1255 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑄𝐴)
7 simp23 1258 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑃𝑄)
8 cdleme11.l . . . . . . . . 9 = (le‘𝐾)
9 cdleme11.j . . . . . . . . 9 = (join‘𝐾)
10 cdleme11.m . . . . . . . . 9 = (meet‘𝐾)
11 cdleme11.a . . . . . . . . 9 𝐴 = (Atoms‘𝐾)
12 cdleme11.h . . . . . . . . 9 𝐻 = (LHyp‘𝐾)
13 cdleme11.u . . . . . . . . 9 𝑈 = ((𝑃 𝑄) 𝑊)
148, 9, 10, 11, 12, 13lhpat2 35823 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
154, 5, 6, 7, 14syl112anc 1486 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑈𝐴)
168, 9, 11hlatlej1 35153 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → 𝑃 (𝑃 𝑈))
172, 3, 15, 16syl3anc 1483 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑃 (𝑃 𝑈))
1817adantr 468 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ 𝑃 (𝑆 𝑇)) → 𝑃 (𝑃 𝑈))
196, 7jca 503 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑄𝐴𝑃𝑄))
20 simp21 1256 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑆𝐴 ∧ ¬ 𝑆 𝑊))
21 simp22 1257 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑇𝐴)
22 simp3r 1252 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑈 (𝑆 𝑇))
2321, 22jca 503 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑇𝐴𝑈 (𝑆 𝑇)))
248, 9, 10, 11, 12, 13cdleme11a 36038 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴𝑈 (𝑆 𝑇)))) → (𝑆 𝑈) = (𝑆 𝑇))
254, 5, 19, 20, 23, 24syl122anc 1491 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑆 𝑈) = (𝑆 𝑇))
2625breq2d 4856 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃 (𝑆 𝑈) ↔ 𝑃 (𝑆 𝑇)))
27 simp21l 1382 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑆𝐴)
288, 9, 10, 11, 12, 13cdleme0b 35990 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) → 𝑈𝑃)
294, 5, 6, 28syl3anc 1483 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑈𝑃)
3029necomd 3033 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑃𝑈)
318, 9, 11hlatexch2 35174 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑆𝐴𝑈𝐴) ∧ 𝑃𝑈) → (𝑃 (𝑆 𝑈) → 𝑆 (𝑃 𝑈)))
322, 3, 27, 15, 30, 31syl131anc 1495 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃 (𝑆 𝑈) → 𝑆 (𝑃 𝑈)))
3326, 32sylbird 251 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃 (𝑆 𝑇) → 𝑆 (𝑃 𝑈)))
3433imp 395 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ 𝑃 (𝑆 𝑇)) → 𝑆 (𝑃 𝑈))
358, 9, 11hlatlej2 35154 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑄 (𝑃 𝑄))
362, 3, 6, 35syl3anc 1483 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑄 (𝑃 𝑄))
378, 9, 10, 11, 12, 13cdleme0cp 35992 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴)) → (𝑃 𝑈) = (𝑃 𝑄))
384, 5, 6, 37syl12anc 856 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃 𝑈) = (𝑃 𝑄))
3936, 38breqtrrd 4872 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑄 (𝑃 𝑈))
4039adantr 468 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ 𝑃 (𝑆 𝑇)) → 𝑄 (𝑃 𝑈))
412hllatd 35142 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝐾 ∈ Lat)
42 eqid 2806 . . . . . . . . . . 11 (Base‘𝐾) = (Base‘𝐾)
4342, 11atbase 35067 . . . . . . . . . 10 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
4427, 43syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑆 ∈ (Base‘𝐾))
4542, 11atbase 35067 . . . . . . . . . 10 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
466, 45syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑄 ∈ (Base‘𝐾))
4742, 9, 11hlatjcl 35145 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → (𝑃 𝑈) ∈ (Base‘𝐾))
482, 3, 15, 47syl3anc 1483 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃 𝑈) ∈ (Base‘𝐾))
4942, 8, 9latjle12 17263 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑈) ∈ (Base‘𝐾))) → ((𝑆 (𝑃 𝑈) ∧ 𝑄 (𝑃 𝑈)) ↔ (𝑆 𝑄) (𝑃 𝑈)))
5041, 44, 46, 48, 49syl13anc 1484 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → ((𝑆 (𝑃 𝑈) ∧ 𝑄 (𝑃 𝑈)) ↔ (𝑆 𝑄) (𝑃 𝑈)))
5150adantr 468 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ 𝑃 (𝑆 𝑇)) → ((𝑆 (𝑃 𝑈) ∧ 𝑄 (𝑃 𝑈)) ↔ (𝑆 𝑄) (𝑃 𝑈)))
5234, 40, 51mpbi2and 694 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ 𝑃 (𝑆 𝑇)) → (𝑆 𝑄) (𝑃 𝑈))
5342, 11atbase 35067 . . . . . . . . . 10 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
543, 53syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑃 ∈ (Base‘𝐾))
5542, 8, 9latnlej1r 17271 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ ¬ 𝑆 (𝑃 𝑄)) → 𝑆𝑄)
5641, 44, 54, 46, 1, 55syl131anc 1495 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → 𝑆𝑄)
578, 9, 11ps-1 35255 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑆𝐴𝑄𝐴𝑆𝑄) ∧ (𝑃𝐴𝑈𝐴)) → ((𝑆 𝑄) (𝑃 𝑈) ↔ (𝑆 𝑄) = (𝑃 𝑈)))
582, 27, 6, 56, 3, 15, 57syl132anc 1500 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → ((𝑆 𝑄) (𝑃 𝑈) ↔ (𝑆 𝑄) = (𝑃 𝑈)))
5958adantr 468 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ 𝑃 (𝑆 𝑇)) → ((𝑆 𝑄) (𝑃 𝑈) ↔ (𝑆 𝑄) = (𝑃 𝑈)))
6052, 59mpbid 223 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ 𝑃 (𝑆 𝑇)) → (𝑆 𝑄) = (𝑃 𝑈))
6118, 60breqtrrd 4872 . . . 4 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ 𝑃 (𝑆 𝑇)) → 𝑃 (𝑆 𝑄))
6261ex 399 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃 (𝑆 𝑇) → 𝑃 (𝑆 𝑄)))
638, 9, 11hlatexch2 35174 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑆𝐴𝑄𝐴) ∧ 𝑃𝑄) → (𝑃 (𝑆 𝑄) → 𝑆 (𝑃 𝑄)))
642, 3, 27, 6, 7, 63syl131anc 1495 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃 (𝑆 𝑄) → 𝑆 (𝑃 𝑄)))
6562, 64syld 47 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → (𝑃 (𝑆 𝑇) → 𝑆 (𝑃 𝑄)))
661, 65mtod 189 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑇𝐴𝑃𝑄) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) → ¬ 𝑃 (𝑆 𝑇))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2978   class class class wbr 4844  cfv 6097  (class class class)co 6870  Basecbs 16064  lecple 16156  joincjn 17145  meetcmee 17146  Latclat 17246  Atomscatm 35041  HLchlt 35128  LHypclh 35762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-1st 7394  df-2nd 7395  df-proset 17129  df-poset 17147  df-plt 17159  df-lub 17175  df-glb 17176  df-join 17177  df-meet 17178  df-p0 17240  df-p1 17241  df-lat 17247  df-clat 17309  df-oposet 34954  df-ol 34956  df-oml 34957  df-covers 35044  df-ats 35045  df-atl 35076  df-cvlat 35100  df-hlat 35129  df-psubsp 35281  df-pmap 35282  df-padd 35574  df-lhyp 35766
This theorem is referenced by:  cdleme11dN  36040  cdleme11e  36041
  Copyright terms: Public domain W3C validator