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

Theorem cdleme16b 36900
Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, first part of 3rd sentence. 𝐹 and 𝐺 represent f(s) and f(t) respectively. It is unclear how this follows from s u t u, as the authors state, and we used a different proof. (Note: the antecedent ¬ 𝑇 (𝑃 𝑄) is not used.) (Contributed by NM, 11-Oct-2012.)
Hypotheses
Ref Expression
cdleme12.l = (le‘𝐾)
cdleme12.j = (join‘𝐾)
cdleme12.m = (meet‘𝐾)
cdleme12.a 𝐴 = (Atoms‘𝐾)
cdleme12.h 𝐻 = (LHyp‘𝐾)
cdleme12.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme12.f 𝐹 = ((𝑆 𝑈) (𝑄 ((𝑃 𝑆) 𝑊)))
cdleme12.g 𝐺 = ((𝑇 𝑈) (𝑄 ((𝑃 𝑇) 𝑊)))
Assertion
Ref Expression
cdleme16b ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐹𝐺)

Proof of Theorem cdleme16b
StepHypRef Expression
1 simp11 1184 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 simp12 1185 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
3 simp13 1186 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
4 simp21 1187 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝑆𝐴 ∧ ¬ 𝑆 𝑊))
5 simp23l 1275 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑃𝑄)
6 simp31 1190 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → ¬ 𝑆 (𝑃 𝑄))
7 cdleme12.l . . . 4 = (le‘𝐾)
8 cdleme12.j . . . 4 = (join‘𝐾)
9 cdleme12.m . . . 4 = (meet‘𝐾)
10 cdleme12.a . . . 4 𝐴 = (Atoms‘𝐾)
11 cdleme12.h . . . 4 𝐻 = (LHyp‘𝐾)
12 cdleme12.u . . . 4 𝑈 = ((𝑃 𝑄) 𝑊)
13 cdleme12.f . . . 4 𝐹 = ((𝑆 𝑈) (𝑄 ((𝑃 𝑆) 𝑊)))
14 eqid 2780 . . . 4 ((𝑃 𝑆) 𝑊) = ((𝑃 𝑆) 𝑊)
157, 8, 9, 10, 11, 12, 13, 14cdleme3g 36855 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐹𝑈)
161, 2, 3, 4, 5, 6, 15syl132anc 1369 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐹𝑈)
17 simp11l 1265 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐾 ∈ HL)
1817hllatd 35985 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐾 ∈ Lat)
19 simp21l 1271 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑆𝐴)
207, 8, 9, 10, 11, 12, 13cdleme3fa 36857 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐹𝐴)
211, 2, 3, 4, 5, 6, 20syl132anc 1369 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐹𝐴)
22 eqid 2780 . . . . . . . . . . 11 (Base‘𝐾) = (Base‘𝐾)
2322, 8, 10hlatjcl 35988 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑆𝐴𝐹𝐴) → (𝑆 𝐹) ∈ (Base‘𝐾))
2417, 19, 21, 23syl3anc 1352 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝑆 𝐹) ∈ (Base‘𝐾))
25 simp22l 1273 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑇𝐴)
2622, 10atbase 35910 . . . . . . . . . 10 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
2725, 26syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑇 ∈ (Base‘𝐾))
2822, 9latmcl 17532 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑆 𝐹) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑆 𝐹) 𝑇) ∈ (Base‘𝐾))
2918, 24, 27, 28syl3anc 1352 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → ((𝑆 𝐹) 𝑇) ∈ (Base‘𝐾))
3022, 10atbase 35910 . . . . . . . . 9 (𝐹𝐴𝐹 ∈ (Base‘𝐾))
3121, 30syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐹 ∈ (Base‘𝐾))
3222, 7, 8latlej2 17541 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝑆 𝐹) 𝑇) ∈ (Base‘𝐾) ∧ 𝐹 ∈ (Base‘𝐾)) → 𝐹 (((𝑆 𝐹) 𝑇) 𝐹))
3318, 29, 31, 32syl3anc 1352 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐹 (((𝑆 𝐹) 𝑇) 𝐹))
3433adantr 473 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ 𝐹 = 𝐺) → 𝐹 (((𝑆 𝐹) 𝑇) 𝐹))
357, 8, 10hlatlej2 35997 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑆𝐴𝐹𝐴) → 𝐹 (𝑆 𝐹))
3617, 19, 21, 35syl3anc 1352 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐹 (𝑆 𝐹))
3722, 7, 8, 9, 10atmod2i1 36482 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝐹𝐴 ∧ (𝑆 𝐹) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) ∧ 𝐹 (𝑆 𝐹)) → (((𝑆 𝐹) 𝑇) 𝐹) = ((𝑆 𝐹) (𝑇 𝐹)))
3817, 21, 24, 27, 36, 37syl131anc 1364 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (((𝑆 𝐹) 𝑇) 𝐹) = ((𝑆 𝐹) (𝑇 𝐹)))
39 oveq2 6990 . . . . . . . . 9 (𝐹 = 𝐺 → (𝑇 𝐹) = (𝑇 𝐺))
4039oveq2d 6998 . . . . . . . 8 (𝐹 = 𝐺 → ((𝑆 𝐹) (𝑇 𝐹)) = ((𝑆 𝐹) (𝑇 𝐺)))
4138, 40sylan9eq 2836 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ 𝐹 = 𝐺) → (((𝑆 𝐹) 𝑇) 𝐹) = ((𝑆 𝐹) (𝑇 𝐺)))
42 simp11r 1266 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑊𝐻)
43 simp13l 1269 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑄𝐴)
44 simp22 1188 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝑇𝐴 ∧ ¬ 𝑇 𝑊))
45 simp23r 1276 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑆𝑇)
46 simp33 1192 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → ¬ 𝑈 (𝑆 𝑇))
4745, 46jca 504 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇)))
48 cdleme12.g . . . . . . . . . 10 𝐺 = ((𝑇 𝑈) (𝑄 ((𝑃 𝑇) 𝑊)))
497, 8, 9, 10, 11, 12, 13, 48cdleme12 36892 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴𝑃𝑄) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑆𝑇 ∧ ¬ 𝑈 (𝑆 𝑇)))) → ((𝑆 𝐹) (𝑇 𝐺)) = 𝑈)
5017, 42, 2, 43, 5, 4, 44, 47, 49syl233anc 1380 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → ((𝑆 𝐹) (𝑇 𝐺)) = 𝑈)
5150adantr 473 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ 𝐹 = 𝐺) → ((𝑆 𝐹) (𝑇 𝐺)) = 𝑈)
5241, 51eqtrd 2816 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ 𝐹 = 𝐺) → (((𝑆 𝐹) 𝑇) 𝐹) = 𝑈)
5334, 52breqtrd 4960 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) ∧ 𝐹 = 𝐺) → 𝐹 𝑈)
5453ex 405 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝐹 = 𝐺𝐹 𝑈))
55 hlatl 35981 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
5617, 55syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐾 ∈ AtLat)
57 simp12l 1267 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑃𝐴)
58 simp12r 1268 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → ¬ 𝑃 𝑊)
597, 8, 9, 10, 11, 12lhpat2 36666 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
6017, 42, 57, 58, 43, 5, 59syl222anc 1367 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝑈𝐴)
617, 10atcmp 35932 . . . . 5 ((𝐾 ∈ AtLat ∧ 𝐹𝐴𝑈𝐴) → (𝐹 𝑈𝐹 = 𝑈))
6256, 21, 60, 61syl3anc 1352 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝐹 𝑈𝐹 = 𝑈))
6354, 62sylibd 231 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝐹 = 𝐺𝐹 = 𝑈))
6463necon3d 2990 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → (𝐹𝑈𝐹𝐺))
6516, 64mpd 15 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ (𝑇𝐴 ∧ ¬ 𝑇 𝑊) ∧ (𝑃𝑄𝑆𝑇)) ∧ (¬ 𝑆 (𝑃 𝑄) ∧ ¬ 𝑇 (𝑃 𝑄) ∧ ¬ 𝑈 (𝑆 𝑇))) → 𝐹𝐺)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wcel 2051  wne 2969   class class class wbr 4934  cfv 6193  (class class class)co 6982  Basecbs 16345  lecple 16434  joincjn 17424  meetcmee 17425  Latclat 17525  Atomscatm 35884  AtLatcal 35885  HLchlt 35971  LHypclh 36605
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 2752  ax-rep 5053  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285
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 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-op 4451  df-uni 4718  df-iun 4799  df-iin 4800  df-br 4935  df-opab 4997  df-mpt 5014  df-id 5316  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-riota 6943  df-ov 6985  df-oprab 6986  df-mpo 6987  df-1st 7507  df-2nd 7508  df-proset 17408  df-poset 17426  df-plt 17438  df-lub 17454  df-glb 17455  df-join 17456  df-meet 17457  df-p0 17519  df-p1 17520  df-lat 17526  df-clat 17588  df-oposet 35797  df-ol 35799  df-oml 35800  df-covers 35887  df-ats 35888  df-atl 35919  df-cvlat 35943  df-hlat 35972  df-lines 36122  df-psubsp 36124  df-pmap 36125  df-padd 36417  df-lhyp 36609
This theorem is referenced by:  cdleme16d  36902  cdleme16f  36904  cdleme20l2  36942
  Copyright terms: Public domain W3C validator