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 36134
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 1240 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ HL)
3 hllat 35153 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ Lat)
42, 3syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ Lat)
5 simp21l 1375 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃𝐴)
6 simp22l 1377 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄𝐴)
7 eqid 2760 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
8 cdleme22.j . . . . . 6 = (join‘𝐾)
9 cdleme22.a . . . . . 6 𝐴 = (Atoms‘𝐾)
107, 8, 9hlatjcl 35156 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
112, 5, 6, 10syl3anc 1477 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ∈ (Base‘𝐾))
12 simp1r 1241 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑊𝐻)
13 simp33l 1385 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧𝐴)
14 cdleme22.l . . . . . . 7 = (le‘𝐾)
15 cdleme22.m . . . . . . 7 = (meet‘𝐾)
16 cdleme22.h . . . . . . 7 𝐻 = (LHyp‘𝐾)
17 cdleme22e.u . . . . . . 7 𝑈 = ((𝑃 𝑄) 𝑊)
18 cdleme22e.f . . . . . . 7 𝐹 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
1914, 8, 15, 9, 16, 17, 18, 7cdleme1b 36016 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → 𝐹 ∈ (Base‘𝐾))
202, 12, 5, 6, 13, 19syl23anc 1484 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐹 ∈ (Base‘𝐾))
21 simp23l 1379 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑆𝐴)
227, 8, 9hlatjcl 35156 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑧𝐴) → (𝑆 𝑧) ∈ (Base‘𝐾))
232, 21, 13, 22syl3anc 1477 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑆 𝑧) ∈ (Base‘𝐾))
247, 16lhpbase 35787 . . . . . . 7 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2512, 24syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑊 ∈ (Base‘𝐾))
267, 15latmcl 17253 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑆 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾))
274, 23, 25, 26syl3anc 1477 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾))
287, 8latjcl 17252 . . . . 5 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑆 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾))
294, 20, 27, 28syl3anc 1477 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾))
307, 14, 15latmle1 17277 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑆 𝑧) 𝑊)) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑧) 𝑊))) (𝑃 𝑄))
314, 11, 29, 30syl3anc 1477 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑧) 𝑊))) (𝑃 𝑄))
321, 31syl5eqbr 4839 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑁 (𝑃 𝑄))
33 simp1 1131 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
34 simp21 1249 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
35 simp23r 1380 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑇𝐴)
36 simp31 1252 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑉𝐴𝑉 𝑊))
37 simp32l 1383 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃𝑄)
38 simp32r 1384 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑉) = (𝑃 𝑄))
3914, 8, 15, 9, 16, 17cdleme22a 36130 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴𝑇𝐴) ∧ ((𝑉𝐴𝑉 𝑊) ∧ 𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄))) → 𝑉 = 𝑈)
4033, 34, 6, 35, 36, 37, 38, 39syl133anc 1500 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑉 = 𝑈)
4140oveq2d 6829 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑂 𝑉) = (𝑂 𝑈))
42 cdleme22e.o . . . . . 6 𝑂 = ((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊)))
4342oveq1i 6823 . . . . 5 (𝑂 𝑈) = (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈)
44 simp21r 1376 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ¬ 𝑃 𝑊)
4514, 8, 15, 9, 16, 17cdleme0a 36001 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
462, 12, 5, 44, 6, 37, 45syl222anc 1493 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈𝐴)
477, 8, 9hlatjcl 35156 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → (𝑇 𝑧) ∈ (Base‘𝐾))
482, 35, 13, 47syl3anc 1477 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑧) ∈ (Base‘𝐾))
497, 15latmcl 17253 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
504, 48, 25, 49syl3anc 1477 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
517, 8latjcl 17252 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
524, 20, 50, 51syl3anc 1477 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
5314, 8, 15, 9, 16, 17cdlemeulpq 36010 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴)) → 𝑈 (𝑃 𝑄))
542, 12, 5, 6, 53syl22anc 1478 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 (𝑃 𝑄))
557, 14, 8, 15, 9atmod2i1 35650 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑃 𝑄)) → (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
562, 46, 11, 52, 54, 55syl131anc 1490 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (((𝑃 𝑄) (𝐹 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
5743, 56syl5req 2807 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑂 𝑈))
5841, 57eqtr4d 2797 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑂 𝑉) = ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)))
5940oveq2d 6829 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑉) = (𝑇 𝑈))
6038, 59eqtr3d 2796 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) = (𝑇 𝑈))
617, 8, 9hlatjcl 35156 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
622, 35, 46, 61syl3anc 1477 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ∈ (Base‘𝐾))
637, 9atbase 35079 . . . . . . . 8 (𝑧𝐴𝑧 ∈ (Base‘𝐾))
6413, 63syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 ∈ (Base‘𝐾))
657, 14, 8latlej1 17261 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
664, 62, 64, 65syl3anc 1477 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
678, 9hlatj32 35161 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑈𝐴𝑧𝐴)) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
682, 35, 46, 13, 67syl13anc 1479 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
697, 9atbase 35079 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
7046, 69syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 ∈ (Base‘𝐾))
717, 8latj32 17298 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
724, 64, 70, 50, 71syl13anc 1479 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
737, 8latj32 17298 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝐹 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)))
744, 20, 50, 70, 73syl13anc 1479 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)))
757, 8, 9hlatjcl 35156 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → (𝑃 𝑧) ∈ (Base‘𝐾))
762, 5, 13, 75syl3anc 1477 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑧) ∈ (Base‘𝐾))
7714, 8, 9hlatlej1 35164 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → 𝑃 (𝑃 𝑧))
782, 5, 13, 77syl3anc 1477 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃 (𝑃 𝑧))
797, 14, 8, 15, 9atmod3i1 35653 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑧)) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
802, 5, 76, 25, 78, 79syl131anc 1490 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
81 eqid 2760 . . . . . . . . . . . . . . . . . . . 20 (1.‘𝐾) = (1.‘𝐾)
8214, 8, 81, 9, 16lhpjat2 35810 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
832, 12, 34, 82syl21anc 1476 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑊) = (1.‘𝐾))
8483oveq2d 6829 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) (𝑃 𝑊)) = ((𝑃 𝑧) (1.‘𝐾)))
85 hlol 35151 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ HL → 𝐾 ∈ OL)
862, 85syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝐾 ∈ OL)
877, 15, 81olm11 35017 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ OL ∧ (𝑃 𝑧) ∈ (Base‘𝐾)) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
8886, 76, 87syl2anc 696 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
8980, 84, 883eqtrd 2798 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 ((𝑃 𝑧) 𝑊)) = (𝑃 𝑧))
9089oveq1d 6828 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑧) 𝑄))
9117oveq2i 6824 . . . . . . . . . . . . . . . . . . 19 (𝑄 𝑈) = (𝑄 ((𝑃 𝑄) 𝑊))
9214, 8, 9hlatlej2 35165 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑄 (𝑃 𝑄))
932, 5, 6, 92syl3anc 1477 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄 (𝑃 𝑄))
947, 14, 8, 15, 9atmod3i1 35653 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑄𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑄 (𝑃 𝑄)) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
952, 6, 11, 25, 93, 94syl131anc 1490 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
9691, 95syl5eq 2806 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑈) = ((𝑃 𝑄) (𝑄 𝑊)))
97 simp22 1250 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
9814, 8, 81, 9, 16lhpjat2 35810 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑄 𝑊) = (1.‘𝐾))
992, 12, 97, 98syl21anc 1476 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑊) = (1.‘𝐾))
10099oveq2d 6829 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (𝑄 𝑊)) = ((𝑃 𝑄) (1.‘𝐾)))
1017, 15, 81olm11 35017 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ OL ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
10286, 11, 101syl2anc 696 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
10396, 100, 1023eqtrd 2798 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 𝑈) = (𝑃 𝑄))
104103oveq1d 6828 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1057, 9atbase 35079 . . . . . . . . . . . . . . . . . 18 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1065, 105syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑃 ∈ (Base‘𝐾))
1077, 15latmcl 17253 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1084, 76, 25, 107syl3anc 1477 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1097, 9atbase 35079 . . . . . . . . . . . . . . . . . 18 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
1106, 109syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑄 ∈ (Base‘𝐾))
1117, 8latj32 17298 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1124, 106, 108, 110, 111syl13anc 1479 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
113104, 112eqtr4d 2797 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄))
1148, 9hlatj32 35161 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
1152, 5, 6, 13, 114syl13anc 1479 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
11690, 113, 1153eqtr4rd 2805 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)))
1177, 8latj32 17298 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
1184, 110, 70, 108, 117syl13anc 1479 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
119116, 118eqtrd 2794 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
120119oveq2d 6829 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1217, 8latjcl 17252 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1224, 11, 64, 121syl3anc 1477 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1237, 14, 8latlej2 17262 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧 ((𝑃 𝑄) 𝑧))
1244, 11, 64, 123syl3anc 1477 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 ((𝑃 𝑄) 𝑧))
1257, 14, 8, 15, 9atmod1i1 35646 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑧𝐴𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) ∧ 𝑧 ((𝑃 𝑄) 𝑧)) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
1262, 13, 70, 122, 124, 125syl131anc 1490 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
12718oveq1i 6823 . . . . . . . . . . . . 13 (𝐹 𝑈) = (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈)
1287, 8, 9hlatjcl 35156 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → (𝑧 𝑈) ∈ (Base‘𝐾))
1292, 13, 46, 128syl3anc 1477 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 𝑈) ∈ (Base‘𝐾))
1307, 8latjcl 17252 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
1314, 110, 108, 130syl3anc 1477 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
13214, 8, 9hlatlej2 35165 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → 𝑈 (𝑧 𝑈))
1332, 13, 46, 132syl3anc 1477 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 (𝑧 𝑈))
1347, 14, 8, 15, 9atmod2i1 35650 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑧 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑧 𝑈)) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1352, 46, 129, 131, 133, 134syl131anc 1490 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
136127, 135syl5eq 2806 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
137120, 126, 1363eqtr4rd 2805 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))))
1387, 14, 8latlej1 17261 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1394, 11, 64, 138syl3anc 1477 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1407, 14, 4, 70, 11, 122, 54, 139lattrd 17259 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑈 ((𝑃 𝑄) 𝑧))
1417, 14, 15latleeqm1 17280 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
1424, 70, 122, 141syl3anc 1477 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
143140, 142mpbid 222 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈)
144143oveq2d 6829 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = (𝑧 𝑈))
145137, 144eqtrd 2794 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝐹 𝑈) = (𝑧 𝑈))
146145oveq1d 6828 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
14774, 146eqtrd 2794 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
14814, 8, 9hlatlej2 35165 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → 𝑧 (𝑇 𝑧))
1492, 35, 13, 148syl3anc 1477 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧 (𝑇 𝑧))
1507, 14, 8, 15, 9atmod3i1 35653 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑧𝐴 ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑧 (𝑇 𝑧)) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
1512, 13, 48, 25, 149, 150syl131anc 1490 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
152 simp33 1254 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧𝐴 ∧ ¬ 𝑧 𝑊))
15314, 8, 81, 9, 16lhpjat2 35810 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)) → (𝑧 𝑊) = (1.‘𝐾))
1542, 12, 152, 153syl21anc 1476 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 𝑊) = (1.‘𝐾))
155154oveq2d 6829 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) (𝑧 𝑊)) = ((𝑇 𝑧) (1.‘𝐾)))
156151, 155eqtrd 2794 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (1.‘𝐾)))
1577, 15, 81olm11 35017 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ (𝑇 𝑧) ∈ (Base‘𝐾)) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
15886, 48, 157syl2anc 696 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
159156, 158eqtr2d 2795 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑧) = (𝑧 ((𝑇 𝑧) 𝑊)))
160159oveq1d 6828 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑈) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
16172, 147, 1603eqtr4rd 2805 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑧) 𝑈) = ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16268, 161eqtrd 2794 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑇 𝑈) 𝑧) = ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16366, 162breqtrd 4830 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑇 𝑈) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
16460, 163eqbrtrd 4826 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈))
1657, 8latjcl 17252 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝐹 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1664, 52, 70, 165syl3anc 1477 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1677, 14, 15latleeqm1 17280 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾)) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
1684, 11, 166, 167syl3anc 1477 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
169164, 168mpbid 222 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → ((𝑃 𝑄) ((𝐹 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄))
17058, 169eqtr2d 2795 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → (𝑃 𝑄) = (𝑂 𝑉))
17132, 170breqtrd 4830 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((𝑉𝐴𝑉 𝑊) ∧ (𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑁 (𝑂 𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932   class class class wbr 4804  cfv 6049  (class class class)co 6813  Basecbs 16059  lecple 16150  joincjn 17145  meetcmee 17146  1.cp1 17239  Latclat 17246  OLcol 34964  Atomscatm 35053  HLchlt 35140  LHypclh 35773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-1st 7333  df-2nd 7334  df-preset 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 34966  df-ol 34968  df-oml 34969  df-covers 35056  df-ats 35057  df-atl 35088  df-cvlat 35112  df-hlat 35141  df-psubsp 35292  df-pmap 35293  df-padd 35585  df-lhyp 35777
This theorem is referenced by:  cdleme26e  36149
  Copyright terms: Public domain W3C validator