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

Theorem cdleme21ct 36943
Description: Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)
Hypotheses
Ref Expression
cdleme21.l = (le‘𝐾)
cdleme21.j = (join‘𝐾)
cdleme21.m = (meet‘𝐾)
cdleme21.a 𝐴 = (Atoms‘𝐾)
cdleme21.h 𝐻 = (LHyp‘𝐾)
cdleme21.u 𝑈 = ((𝑃 𝑄) 𝑊)
Assertion
Ref Expression
cdleme21ct ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑈 (𝑇 𝑧))

Proof of Theorem cdleme21ct
StepHypRef Expression
1 simp11 1184 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 simp12 1185 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
3 simp13 1186 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑄𝐴)
4 simp21l 1271 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑆𝐴)
5 simp231 1298 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑃𝑄)
6 simp232 1299 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑆 (𝑃 𝑄))
7 simp3ll 1225 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑧𝐴)
8 simp3r 1183 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑃 𝑧) = (𝑆 𝑧))
9 cdleme21.l . . . 4 = (le‘𝐾)
10 cdleme21.j . . . 4 = (join‘𝐾)
11 cdleme21.m . . . 4 = (meet‘𝐾)
12 cdleme21.a . . . 4 𝐴 = (Atoms‘𝐾)
13 cdleme21.h . . . 4 𝐻 = (LHyp‘𝐾)
14 cdleme21.u . . . 4 𝑈 = ((𝑃 𝑄) 𝑊)
159, 10, 11, 12, 13, 14cdleme21c 36941 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ (𝑆𝐴𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑈 (𝑆 𝑧))
161, 2, 3, 4, 5, 6, 7, 8, 15syl332anc 1382 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑈 (𝑆 𝑧))
17 simp233 1300 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑈 (𝑆 𝑇))
18 simp11l 1265 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝐾 ∈ HL)
19 hlcvl 35973 . . . . . . . . 9 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2018, 19syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝐾 ∈ CvLat)
21 simp11r 1266 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑊𝐻)
22 simp12l 1267 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑃𝐴)
23 simp12r 1268 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑃 𝑊)
249, 10, 11, 12, 13, 14cdleme0a 36825 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
2518, 21, 22, 23, 3, 5, 24syl222anc 1367 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑈𝐴)
26 simp22l 1273 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑇𝐴)
2718hllatd 35978 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝐾 ∈ Lat)
28 eqid 2773 . . . . . . . . . . . . 13 (Base‘𝐾) = (Base‘𝐾)
2928, 10, 12hlatjcl 35981 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
3018, 22, 3, 29syl3anc 1352 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑃 𝑄) ∈ (Base‘𝐾))
3128, 13lhpbase 36612 . . . . . . . . . . . 12 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3221, 31syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑊 ∈ (Base‘𝐾))
3328, 9, 11latmle2 17558 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑊) 𝑊)
3427, 30, 32, 33syl3anc 1352 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ((𝑃 𝑄) 𝑊) 𝑊)
3514, 34syl5eqbr 4961 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑈 𝑊)
36 simp21r 1272 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑆 𝑊)
37 nbrne2 4946 . . . . . . . . 9 ((𝑈 𝑊 ∧ ¬ 𝑆 𝑊) → 𝑈𝑆)
3835, 36, 37syl2anc 576 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑈𝑆)
39 simp22r 1274 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑇 𝑊)
40 nbrne2 4946 . . . . . . . . 9 ((𝑈 𝑊 ∧ ¬ 𝑇 𝑊) → 𝑈𝑇)
4135, 39, 40syl2anc 576 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑈𝑇)
429, 10, 12cvlatexch3 35952 . . . . . . . 8 ((𝐾 ∈ CvLat ∧ (𝑈𝐴𝑆𝐴𝑇𝐴) ∧ (𝑈𝑆𝑈𝑇)) → (𝑈 (𝑆 𝑇) → (𝑈 𝑆) = (𝑈 𝑇)))
4320, 25, 4, 26, 38, 41, 42syl132anc 1369 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑈 (𝑆 𝑇) → (𝑈 𝑆) = (𝑈 𝑇)))
4417, 43mpd 15 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑈 𝑆) = (𝑈 𝑇))
4544adantr 473 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) ∧ 𝑈 (𝑇 𝑧)) → (𝑈 𝑆) = (𝑈 𝑇))
46 simp3lr 1226 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑧 𝑊)
47 nbrne2 4946 . . . . . . . 8 ((𝑈 𝑊 ∧ ¬ 𝑧 𝑊) → 𝑈𝑧)
4835, 46, 47syl2anc 576 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑈𝑧)
499, 10, 12cvlatexch3 35952 . . . . . . 7 ((𝐾 ∈ CvLat ∧ (𝑈𝐴𝑇𝐴𝑧𝐴) ∧ (𝑈𝑇𝑈𝑧)) → (𝑈 (𝑇 𝑧) → (𝑈 𝑇) = (𝑈 𝑧)))
5020, 25, 26, 7, 41, 48, 49syl132anc 1369 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑈 (𝑇 𝑧) → (𝑈 𝑇) = (𝑈 𝑧)))
5150imp 398 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) ∧ 𝑈 (𝑇 𝑧)) → (𝑈 𝑇) = (𝑈 𝑧))
5245, 51eqtrd 2809 . . . 4 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) ∧ 𝑈 (𝑇 𝑧)) → (𝑈 𝑆) = (𝑈 𝑧))
5352ex 405 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑈 (𝑇 𝑧) → (𝑈 𝑆) = (𝑈 𝑧)))
549, 10, 12hlatlej2 35990 . . . . 5 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑆𝐴) → 𝑆 (𝑈 𝑆))
5518, 25, 4, 54syl3anc 1352 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑆 (𝑈 𝑆))
56 breq2 4930 . . . 4 ((𝑈 𝑆) = (𝑈 𝑧) → (𝑆 (𝑈 𝑆) ↔ 𝑆 (𝑈 𝑧)))
5755, 56syl5ibcom 237 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ((𝑈 𝑆) = (𝑈 𝑧) → 𝑆 (𝑈 𝑧)))
589, 10, 12cdleme21a 36939 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑆𝐴 ∧ ¬ 𝑆 (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑆𝑧)
5918, 22, 3, 4, 6, 7, 8, 58syl322anc 1379 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → 𝑆𝑧)
609, 10, 12cvlatexch2 35951 . . . 4 ((𝐾 ∈ CvLat ∧ (𝑆𝐴𝑈𝐴𝑧𝐴) ∧ 𝑆𝑧) → (𝑆 (𝑈 𝑧) → 𝑈 (𝑆 𝑧)))
6120, 4, 25, 7, 59, 60syl131anc 1364 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑆 (𝑈 𝑧) → 𝑈 (𝑆 𝑧)))
6253, 57, 613syld 60 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → (𝑈 (𝑇 𝑧) → 𝑈 (𝑆 𝑧)))
6316, 62mtod 190 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄) ∧ 𝑈 (𝑆 𝑇))) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 𝑊) ∧ (𝑃 𝑧) = (𝑆 𝑧))) → ¬ 𝑈 (𝑇 𝑧))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387  w3a 1069   = wceq 1508  wcel 2051  wne 2962   class class class wbr 4926  cfv 6186  (class class class)co 6975  Basecbs 16338  lecple 16427  joincjn 17425  meetcmee 17426  Latclat 17526  Atomscatm 35877  CvLatclc 35879  HLchlt 35964  LHypclh 36598
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-proset 17409  df-poset 17427  df-plt 17439  df-lub 17455  df-glb 17456  df-join 17457  df-meet 17458  df-p0 17520  df-p1 17521  df-lat 17527  df-clat 17589  df-oposet 35790  df-ol 35792  df-oml 35793  df-covers 35880  df-ats 35881  df-atl 35912  df-cvlat 35936  df-hlat 35965  df-lhyp 36602
This theorem is referenced by:  cdleme21e  36945
  Copyright terms: Public domain W3C validator