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

Theorem cdleme22e 40327
Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. 𝐹, 𝑁, 𝑂 represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. (Contributed by NM, 6-Dec-2012.)
Hypotheses
Ref Expression
cdleme22.l = (le‘𝐾)
cdleme22.j = (join‘𝐾)
cdleme22.m = (meet‘𝐾)
cdleme22.a 𝐴 = (Atoms‘𝐾)
cdleme22.h 𝐻 = (LHyp‘𝐾)
cdleme22e.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme22e.f 𝐹 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
cdleme22e.n 𝑁 = ((𝑃 𝑄) (𝐹 ((𝑆 𝑧) 𝑊)))
cdleme22e.o 𝑂 = ((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊)))
Assertion
Ref Expression
cdleme22e (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑁 (𝑂 𝑉))

Proof of Theorem cdleme22e
StepHypRef Expression
1 cdleme22e.n . . 3 𝑁 = ((𝑃 𝑄) (𝐹 ((𝑆 𝑧) 𝑊)))
2 simp1l 1196 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ HL)
32hllatd 39346 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ Lat)
4 simp21l 1289 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃𝐴)
5 simp22l 1291 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄𝐴)
6 eqid 2735 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
7 cdleme22.j . . . . . 6 = (join‘𝐾)
8 cdleme22.a . . . . . 6 𝐴 = (Atoms‘𝐾)
96, 7, 8hlatjcl 39349 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
102, 4, 5, 9syl3anc 1370 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ∈ (Base‘𝐾))
11 simp1r 1197 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑊𝐻)
12 simp33l 1299 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧𝐴)
13 cdleme22.l . . . . . . 7 = (le‘𝐾)
14 cdleme22.m . . . . . . 7 = (meet‘𝐾)
15 cdleme22.h . . . . . . 7 𝐻 = (LHyp‘𝐾)
16 cdleme22e.u . . . . . . 7 𝑈 = ((𝑃 𝑄) 𝑊)
17 cdleme22e.f . . . . . . 7 𝐹 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
1813, 7, 14, 8, 15, 16, 17, 6cdleme1b 40209 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → 𝐹 ∈ (Base‘𝐾))
192, 11, 4, 5, 12, 18syl23anc 1376 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐹 ∈ (Base‘𝐾))
20 simp23l 1293 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑆𝐴)
216, 7, 8hlatjcl 39349 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑧𝐴) → (𝑆 𝑧) ∈ (Base‘𝐾))
222, 20, 12, 21syl3anc 1370 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑆 𝑧) ∈ (Base‘𝐾))
236, 15lhpbase 39981 . . . . . . 7 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2411, 23syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑊 ∈ (Base‘𝐾))
256, 14latmcl 18498 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑆 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾))
263, 22, 24, 25syl3anc 1370 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾))
276, 7latjcl 18497 . . . . 5 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾))
283, 19, 26, 27syl3anc 1370 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾))
296, 13, 14latmle1 18522 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑧) 𝑊))) (𝑃 𝑄))
303, 10, 28, 29syl3anc 1370 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑧) 𝑊))) (𝑃 𝑄))
311, 30eqbrtrid 5183 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑁 (𝑃 𝑄))
32 simp1 1135 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
33 simp21 1205 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
34 simp23r 1294 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑇𝐴)
35 simp31 1208 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑉𝐴𝑉 𝑊))
36 simp32l 1297 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃𝑄)
37 simp32r 1298 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑉) = (𝑃 𝑄))
3813, 7, 14, 8, 15, 16cdleme22a 40323 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴𝑇𝐴) ∧ ((𝑉𝐴𝑉 𝑊) ∧ 𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄))) → 𝑉 = 𝑈)
3932, 33, 5, 34, 35, 36, 37, 38syl133anc 1392 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑉 = 𝑈)
4039oveq2d 7447 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑂 𝑉) = (𝑂 𝑈))
41 cdleme22e.o . . . . . 6 𝑂 = ((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊)))
4241oveq1i 7441 . . . . 5 (𝑂 𝑈) = (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈)
43 simp21r 1290 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ¬ 𝑃 𝑊)
4413, 7, 14, 8, 15, 16cdleme0a 40194 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
452, 11, 4, 43, 5, 36, 44syl222anc 1385 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈𝐴)
466, 7, 8hlatjcl 39349 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → (𝑇 𝑧) ∈ (Base‘𝐾))
472, 34, 12, 46syl3anc 1370 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑧) ∈ (Base‘𝐾))
486, 14latmcl 18498 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
493, 47, 24, 48syl3anc 1370 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
506, 7latjcl 18497 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
513, 19, 49, 50syl3anc 1370 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
5213, 7, 14, 8, 15, 16cdlemeulpq 40203 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴)) → 𝑈 (𝑃 𝑄))
532, 11, 4, 5, 52syl22anc 839 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 (𝑃 𝑄))
546, 13, 7, 14, 8atmod2i1 39844 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑃 𝑄)) → (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
552, 45, 10, 51, 53, 54syl131anc 1382 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
5642, 55eqtr2id 2788 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑂 𝑈))
5740, 56eqtr4d 2778 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑂 𝑉) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
5839oveq2d 7447 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑉) = (𝑇 𝑈))
5937, 58eqtr3d 2777 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) = (𝑇 𝑈))
606, 7, 8hlatjcl 39349 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
612, 34, 45, 60syl3anc 1370 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ∈ (Base‘𝐾))
626, 8atbase 39271 . . . . . . . 8 (𝑧𝐴𝑧 ∈ (Base‘𝐾))
6312, 62syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 ∈ (Base‘𝐾))
646, 13, 7latlej1 18506 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
653, 61, 63, 64syl3anc 1370 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
667, 8hlatj32 39354 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑈𝐴𝑧𝐴)) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
672, 34, 45, 12, 66syl13anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
686, 8atbase 39271 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
6945, 68syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 ∈ (Base‘𝐾))
706, 7latj32 18543 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
713, 63, 69, 49, 70syl13anc 1371 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
726, 7latj32 18543 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝐹 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)))
733, 19, 49, 69, 72syl13anc 1371 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)))
746, 7, 8hlatjcl 39349 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → (𝑃 𝑧) ∈ (Base‘𝐾))
752, 4, 12, 74syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑧) ∈ (Base‘𝐾))
7613, 7, 8hlatlej1 39357 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → 𝑃 (𝑃 𝑧))
772, 4, 12, 76syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃 (𝑃 𝑧))
786, 13, 7, 14, 8atmod3i1 39847 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑧)) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
792, 4, 75, 24, 77, 78syl131anc 1382 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
80 eqid 2735 . . . . . . . . . . . . . . . . . . . 20 (1.‘𝐾) = (1.‘𝐾)
8113, 7, 80, 8, 15lhpjat2 40004 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
822, 11, 33, 81syl21anc 838 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑊) = (1.‘𝐾))
8382oveq2d 7447 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) (𝑃 𝑊)) = ((𝑃 𝑧) (1.‘𝐾)))
84 hlol 39343 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ HL → 𝐾 ∈ OL)
852, 84syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ OL)
866, 14, 80olm11 39209 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ OL ∧ (𝑃 𝑧) ∈ (Base‘𝐾)) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
8785, 75, 86syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
8879, 83, 873eqtrd 2779 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 ((𝑃 𝑧) 𝑊)) = (𝑃 𝑧))
8988oveq1d 7446 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑧) 𝑄))
9016oveq2i 7442 . . . . . . . . . . . . . . . . . . 19 (𝑄 𝑈) = (𝑄 ((𝑃 𝑄) 𝑊))
9113, 7, 8hlatlej2 39358 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑄 (𝑃 𝑄))
922, 4, 5, 91syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄 (𝑃 𝑄))
936, 13, 7, 14, 8atmod3i1 39847 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑄𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑄 (𝑃 𝑄)) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
942, 5, 10, 24, 92, 93syl131anc 1382 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
9590, 94eqtrid 2787 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑈) = ((𝑃 𝑄) (𝑄 𝑊)))
96 simp22 1206 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
9713, 7, 80, 8, 15lhpjat2 40004 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑄 𝑊) = (1.‘𝐾))
982, 11, 96, 97syl21anc 838 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑊) = (1.‘𝐾))
9998oveq2d 7447 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (𝑄 𝑊)) = ((𝑃 𝑄) (1.‘𝐾)))
1006, 14, 80olm11 39209 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ OL ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
10185, 10, 100syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
10295, 99, 1013eqtrd 2779 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑈) = (𝑃 𝑄))
103102oveq1d 7446 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1046, 8atbase 39271 . . . . . . . . . . . . . . . . . 18 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1054, 104syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃 ∈ (Base‘𝐾))
1066, 14latmcl 18498 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1073, 75, 24, 106syl3anc 1370 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1086, 8atbase 39271 . . . . . . . . . . . . . . . . . 18 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
1095, 108syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄 ∈ (Base‘𝐾))
1106, 7latj32 18543 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1113, 105, 107, 109, 110syl13anc 1371 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
112103, 111eqtr4d 2778 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄))
1137, 8hlatj32 39354 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
1142, 4, 5, 12, 113syl13anc 1371 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
11589, 112, 1143eqtr4rd 2786 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)))
1166, 7latj32 18543 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
1173, 109, 69, 107, 116syl13anc 1371 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
118115, 117eqtrd 2775 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
119118oveq2d 7447 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1206, 7latjcl 18497 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1213, 10, 63, 120syl3anc 1370 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1226, 13, 7latlej2 18507 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧 ((𝑃 𝑄) 𝑧))
1233, 10, 63, 122syl3anc 1370 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 ((𝑃 𝑄) 𝑧))
1246, 13, 7, 14, 8atmod1i1 39840 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑧𝐴𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) ∧ 𝑧 ((𝑃 𝑄) 𝑧)) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
1252, 12, 69, 121, 123, 124syl131anc 1382 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
12617oveq1i 7441 . . . . . . . . . . . . 13 (𝐹 𝑈) = (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈)
1276, 7, 8hlatjcl 39349 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → (𝑧 𝑈) ∈ (Base‘𝐾))
1282, 12, 45, 127syl3anc 1370 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 𝑈) ∈ (Base‘𝐾))
1296, 7latjcl 18497 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
1303, 109, 107, 129syl3anc 1370 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
13113, 7, 8hlatlej2 39358 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → 𝑈 (𝑧 𝑈))
1322, 12, 45, 131syl3anc 1370 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 (𝑧 𝑈))
1336, 13, 7, 14, 8atmod2i1 39844 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑧 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑧 𝑈)) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1342, 45, 128, 130, 132, 133syl131anc 1382 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
135126, 134eqtrid 2787 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
136119, 125, 1353eqtr4rd 2786 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))))
1376, 13, 7latlej1 18506 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1383, 10, 63, 137syl3anc 1370 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1396, 13, 3, 69, 10, 121, 53, 138lattrd 18504 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 ((𝑃 𝑄) 𝑧))
1406, 13, 14latleeqm1 18525 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
1413, 69, 121, 140syl3anc 1370 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
142139, 141mpbid 232 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈)
143142oveq2d 7447 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = (𝑧 𝑈))
144136, 143eqtrd 2775 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = (𝑧 𝑈))
145144oveq1d 7446 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
14673, 145eqtrd 2775 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
14713, 7, 8hlatlej2 39358 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → 𝑧 (𝑇 𝑧))
1482, 34, 12, 147syl3anc 1370 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 (𝑇 𝑧))
1496, 13, 7, 14, 8atmod3i1 39847 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑧𝐴 ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑧 (𝑇 𝑧)) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
1502, 12, 47, 24, 148, 149syl131anc 1382 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
151 simp33 1210 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧𝐴 ∧ ¬ 𝑧 𝑊))
15213, 7, 80, 8, 15lhpjat2 40004 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)) → (𝑧 𝑊) = (1.‘𝐾))
1532, 11, 151, 152syl21anc 838 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 𝑊) = (1.‘𝐾))
154153oveq2d 7447 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) (𝑧 𝑊)) = ((𝑇 𝑧) (1.‘𝐾)))
155150, 154eqtrd 2775 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (1.‘𝐾)))
1566, 14, 80olm11 39209 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ (𝑇 𝑧) ∈ (Base‘𝐾)) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
15785, 47, 156syl2anc 584 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
158155, 157eqtr2d 2776 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑧) = (𝑧 ((𝑇 𝑧) 𝑊)))
159158oveq1d 7446 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑈) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
16071, 146, 1593eqtr4rd 2786 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑈) = ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16167, 160eqtrd 2775 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑈) 𝑧) = ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16265, 161breqtrd 5174 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16359, 162eqbrtrd 5170 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
1646, 7latjcl 18497 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1653, 51, 69, 164syl3anc 1370 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1666, 13, 14latleeqm1 18525 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾)) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
1673, 10, 165, 166syl3anc 1370 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
168163, 167mpbid 232 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄))
16957, 168eqtr2d 2776 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) = (𝑂 𝑉))
17031, 169breqtrd 5174 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑁 (𝑂 𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wne 2938   class class class wbr 5148  cfv 6563  (class class class)co 7431  Basecbs 17245  lecple 17305  joincjn 18369  meetcmee 18370  1.cp1 18482  Latclat 18489  OLcol 39156  Atomscatm 39245  HLchlt 39332  LHypclh 39967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-proset 18352  df-poset 18371  df-plt 18388  df-lub 18404  df-glb 18405  df-join 18406  df-meet 18407  df-p0 18483  df-p1 18484  df-lat 18490  df-clat 18557  df-oposet 39158  df-ol 39160  df-oml 39161  df-covers 39248  df-ats 39249  df-atl 39280  df-cvlat 39304  df-hlat 39333  df-psubsp 39486  df-pmap 39487  df-padd 39779  df-lhyp 39971
This theorem is referenced by:  cdleme26e  40342
  Copyright terms: Public domain W3C validator