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 39817
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 1195 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ HL)
32hllatd 38836 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ Lat)
4 simp21l 1288 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃𝐴)
5 simp22l 1290 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄𝐴)
6 eqid 2728 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
7 cdleme22.j . . . . . 6 = (join‘𝐾)
8 cdleme22.a . . . . . 6 𝐴 = (Atoms‘𝐾)
96, 7, 8hlatjcl 38839 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
102, 4, 5, 9syl3anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ∈ (Base‘𝐾))
11 simp1r 1196 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑊𝐻)
12 simp33l 1298 . . . . . 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 39699 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → 𝐹 ∈ (Base‘𝐾))
192, 11, 4, 5, 12, 18syl23anc 1375 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐹 ∈ (Base‘𝐾))
20 simp23l 1292 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑆𝐴)
216, 7, 8hlatjcl 38839 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑧𝐴) → (𝑆 𝑧) ∈ (Base‘𝐾))
222, 20, 12, 21syl3anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑆 𝑧) ∈ (Base‘𝐾))
236, 15lhpbase 39471 . . . . . . 7 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2411, 23syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑊 ∈ (Base‘𝐾))
256, 14latmcl 18431 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑆 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾))
263, 22, 24, 25syl3anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾))
276, 7latjcl 18430 . . . . 5 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾))
283, 19, 26, 27syl3anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾))
296, 13, 14latmle1 18455 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑧) 𝑊))) (𝑃 𝑄))
303, 10, 28, 29syl3anc 1369 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑧) 𝑊))) (𝑃 𝑄))
311, 30eqbrtrid 5183 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑁 (𝑃 𝑄))
32 simp1 1134 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
33 simp21 1204 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
34 simp23r 1293 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑇𝐴)
35 simp31 1207 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑉𝐴𝑉 𝑊))
36 simp32l 1296 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃𝑄)
37 simp32r 1297 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑉) = (𝑃 𝑄))
3813, 7, 14, 8, 15, 16cdleme22a 39813 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴𝑇𝐴) ∧ ((𝑉𝐴𝑉 𝑊) ∧ 𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄))) → 𝑉 = 𝑈)
3932, 33, 5, 34, 35, 36, 37, 38syl133anc 1391 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑉 = 𝑈)
4039oveq2d 7436 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑂 𝑉) = (𝑂 𝑈))
41 cdleme22e.o . . . . . 6 𝑂 = ((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊)))
4241oveq1i 7430 . . . . 5 (𝑂 𝑈) = (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈)
43 simp21r 1289 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ¬ 𝑃 𝑊)
4413, 7, 14, 8, 15, 16cdleme0a 39684 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
452, 11, 4, 43, 5, 36, 44syl222anc 1384 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈𝐴)
466, 7, 8hlatjcl 38839 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → (𝑇 𝑧) ∈ (Base‘𝐾))
472, 34, 12, 46syl3anc 1369 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑧) ∈ (Base‘𝐾))
486, 14latmcl 18431 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
493, 47, 24, 48syl3anc 1369 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
506, 7latjcl 18430 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
513, 19, 49, 50syl3anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
5213, 7, 14, 8, 15, 16cdlemeulpq 39693 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴)) → 𝑈 (𝑃 𝑄))
532, 11, 4, 5, 52syl22anc 838 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 (𝑃 𝑄))
546, 13, 7, 14, 8atmod2i1 39334 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑃 𝑄)) → (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
552, 45, 10, 51, 53, 54syl131anc 1381 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
5642, 55eqtr2id 2781 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑂 𝑈))
5740, 56eqtr4d 2771 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑂 𝑉) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
5839oveq2d 7436 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑉) = (𝑇 𝑈))
5937, 58eqtr3d 2770 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) = (𝑇 𝑈))
606, 7, 8hlatjcl 38839 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
612, 34, 45, 60syl3anc 1369 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ∈ (Base‘𝐾))
626, 8atbase 38761 . . . . . . . 8 (𝑧𝐴𝑧 ∈ (Base‘𝐾))
6312, 62syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 ∈ (Base‘𝐾))
646, 13, 7latlej1 18439 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
653, 61, 63, 64syl3anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
667, 8hlatj32 38844 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑈𝐴𝑧𝐴)) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
672, 34, 45, 12, 66syl13anc 1370 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
686, 8atbase 38761 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
6945, 68syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 ∈ (Base‘𝐾))
706, 7latj32 18476 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
713, 63, 69, 49, 70syl13anc 1370 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
726, 7latj32 18476 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝐹 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)))
733, 19, 49, 69, 72syl13anc 1370 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)))
746, 7, 8hlatjcl 38839 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → (𝑃 𝑧) ∈ (Base‘𝐾))
752, 4, 12, 74syl3anc 1369 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑧) ∈ (Base‘𝐾))
7613, 7, 8hlatlej1 38847 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → 𝑃 (𝑃 𝑧))
772, 4, 12, 76syl3anc 1369 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃 (𝑃 𝑧))
786, 13, 7, 14, 8atmod3i1 39337 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑧)) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
792, 4, 75, 24, 77, 78syl131anc 1381 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
80 eqid 2728 . . . . . . . . . . . . . . . . . . . 20 (1.‘𝐾) = (1.‘𝐾)
8113, 7, 80, 8, 15lhpjat2 39494 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
822, 11, 33, 81syl21anc 837 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑊) = (1.‘𝐾))
8382oveq2d 7436 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) (𝑃 𝑊)) = ((𝑃 𝑧) (1.‘𝐾)))
84 hlol 38833 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ HL → 𝐾 ∈ OL)
852, 84syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ OL)
866, 14, 80olm11 38699 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ OL ∧ (𝑃 𝑧) ∈ (Base‘𝐾)) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
8785, 75, 86syl2anc 583 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
8879, 83, 873eqtrd 2772 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 ((𝑃 𝑧) 𝑊)) = (𝑃 𝑧))
8988oveq1d 7435 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑧) 𝑄))
9016oveq2i 7431 . . . . . . . . . . . . . . . . . . 19 (𝑄 𝑈) = (𝑄 ((𝑃 𝑄) 𝑊))
9113, 7, 8hlatlej2 38848 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑄 (𝑃 𝑄))
922, 4, 5, 91syl3anc 1369 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄 (𝑃 𝑄))
936, 13, 7, 14, 8atmod3i1 39337 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑄𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑄 (𝑃 𝑄)) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
942, 5, 10, 24, 92, 93syl131anc 1381 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
9590, 94eqtrid 2780 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑈) = ((𝑃 𝑄) (𝑄 𝑊)))
96 simp22 1205 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
9713, 7, 80, 8, 15lhpjat2 39494 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑄 𝑊) = (1.‘𝐾))
982, 11, 96, 97syl21anc 837 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑊) = (1.‘𝐾))
9998oveq2d 7436 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (𝑄 𝑊)) = ((𝑃 𝑄) (1.‘𝐾)))
1006, 14, 80olm11 38699 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ OL ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
10185, 10, 100syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
10295, 99, 1013eqtrd 2772 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑈) = (𝑃 𝑄))
103102oveq1d 7435 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1046, 8atbase 38761 . . . . . . . . . . . . . . . . . 18 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1054, 104syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃 ∈ (Base‘𝐾))
1066, 14latmcl 18431 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1073, 75, 24, 106syl3anc 1369 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1086, 8atbase 38761 . . . . . . . . . . . . . . . . . 18 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
1095, 108syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄 ∈ (Base‘𝐾))
1106, 7latj32 18476 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1113, 105, 107, 109, 110syl13anc 1370 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
112103, 111eqtr4d 2771 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄))
1137, 8hlatj32 38844 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
1142, 4, 5, 12, 113syl13anc 1370 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
11589, 112, 1143eqtr4rd 2779 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)))
1166, 7latj32 18476 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
1173, 109, 69, 107, 116syl13anc 1370 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
118115, 117eqtrd 2768 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
119118oveq2d 7436 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1206, 7latjcl 18430 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1213, 10, 63, 120syl3anc 1369 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1226, 13, 7latlej2 18440 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧 ((𝑃 𝑄) 𝑧))
1233, 10, 63, 122syl3anc 1369 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 ((𝑃 𝑄) 𝑧))
1246, 13, 7, 14, 8atmod1i1 39330 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑧𝐴𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) ∧ 𝑧 ((𝑃 𝑄) 𝑧)) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
1252, 12, 69, 121, 123, 124syl131anc 1381 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
12617oveq1i 7430 . . . . . . . . . . . . 13 (𝐹 𝑈) = (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈)
1276, 7, 8hlatjcl 38839 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → (𝑧 𝑈) ∈ (Base‘𝐾))
1282, 12, 45, 127syl3anc 1369 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 𝑈) ∈ (Base‘𝐾))
1296, 7latjcl 18430 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
1303, 109, 107, 129syl3anc 1369 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
13113, 7, 8hlatlej2 38848 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → 𝑈 (𝑧 𝑈))
1322, 12, 45, 131syl3anc 1369 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 (𝑧 𝑈))
1336, 13, 7, 14, 8atmod2i1 39334 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑧 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑧 𝑈)) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1342, 45, 128, 130, 132, 133syl131anc 1381 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
135126, 134eqtrid 2780 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
136119, 125, 1353eqtr4rd 2779 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))))
1376, 13, 7latlej1 18439 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1383, 10, 63, 137syl3anc 1369 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1396, 13, 3, 69, 10, 121, 53, 138lattrd 18437 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 ((𝑃 𝑄) 𝑧))
1406, 13, 14latleeqm1 18458 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
1413, 69, 121, 140syl3anc 1369 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
142139, 141mpbid 231 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈)
143142oveq2d 7436 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = (𝑧 𝑈))
144136, 143eqtrd 2768 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = (𝑧 𝑈))
145144oveq1d 7435 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
14673, 145eqtrd 2768 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
14713, 7, 8hlatlej2 38848 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → 𝑧 (𝑇 𝑧))
1482, 34, 12, 147syl3anc 1369 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 (𝑇 𝑧))
1496, 13, 7, 14, 8atmod3i1 39337 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑧𝐴 ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑧 (𝑇 𝑧)) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
1502, 12, 47, 24, 148, 149syl131anc 1381 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
151 simp33 1209 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧𝐴 ∧ ¬ 𝑧 𝑊))
15213, 7, 80, 8, 15lhpjat2 39494 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)) → (𝑧 𝑊) = (1.‘𝐾))
1532, 11, 151, 152syl21anc 837 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 𝑊) = (1.‘𝐾))
154153oveq2d 7436 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) (𝑧 𝑊)) = ((𝑇 𝑧) (1.‘𝐾)))
155150, 154eqtrd 2768 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (1.‘𝐾)))
1566, 14, 80olm11 38699 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ (𝑇 𝑧) ∈ (Base‘𝐾)) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
15785, 47, 156syl2anc 583 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
158155, 157eqtr2d 2769 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑧) = (𝑧 ((𝑇 𝑧) 𝑊)))
159158oveq1d 7435 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑈) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
16071, 146, 1593eqtr4rd 2779 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑈) = ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16167, 160eqtrd 2768 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑈) 𝑧) = ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16265, 161breqtrd 5174 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16359, 162eqbrtrd 5170 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
1646, 7latjcl 18430 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1653, 51, 69, 164syl3anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1666, 13, 14latleeqm1 18458 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾)) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
1673, 10, 165, 166syl3anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
168163, 167mpbid 231 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄))
16957, 168eqtr2d 2769 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) = (𝑂 𝑉))
17031, 169breqtrd 5174 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑁 (𝑂 𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2937   class class class wbr 5148  cfv 6548  (class class class)co 7420  Basecbs 17179  lecple 17239  joincjn 18302  meetcmee 18303  1.cp1 18415  Latclat 18422  OLcol 38646  Atomscatm 38735  HLchlt 38822  LHypclh 39457
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 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 7993  df-2nd 7994  df-proset 18286  df-poset 18304  df-plt 18321  df-lub 18337  df-glb 18338  df-join 18339  df-meet 18340  df-p0 18416  df-p1 18417  df-lat 18423  df-clat 18490  df-oposet 38648  df-ol 38650  df-oml 38651  df-covers 38738  df-ats 38739  df-atl 38770  df-cvlat 38794  df-hlat 38823  df-psubsp 38976  df-pmap 38977  df-padd 39269  df-lhyp 39461
This theorem is referenced by:  cdleme26e  39832
  Copyright terms: Public domain W3C validator