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

Theorem cdleme22eALTN 36154
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.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdleme22.l = (le‘𝐾)
cdleme22.j = (join‘𝐾)
cdleme22.m = (meet‘𝐾)
cdleme22.a 𝐴 = (Atoms‘𝐾)
cdleme22.h 𝐻 = (LHyp‘𝐾)
cdleme22eALT.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme22eALT.f 𝐹 = ((𝑦 𝑈) (𝑄 ((𝑃 𝑦) 𝑊)))
cdleme22eALT.g 𝐺 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
cdleme22eALT.n 𝑁 = ((𝑃 𝑄) (𝐹 ((𝑆 𝑦) 𝑊)))
cdleme22eALT.o 𝑂 = ((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊)))
Assertion
Ref Expression
cdleme22eALTN (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑁 (𝑂 𝑉))

Proof of Theorem cdleme22eALTN
StepHypRef Expression
1 cdleme22eALT.n . . 3 𝑁 = ((𝑃 𝑄) (𝐹 ((𝑆 𝑦) 𝑊)))
2 simp11 1246 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐾 ∈ HL)
3 hllat 35172 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ Lat)
42, 3syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐾 ∈ Lat)
5 simp21l 1375 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑃𝐴)
6 simp22l 1377 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑄𝐴)
7 eqid 2761 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
8 cdleme22.j . . . . . 6 = (join‘𝐾)
9 cdleme22.a . . . . . 6 𝐴 = (Atoms‘𝐾)
107, 8, 9hlatjcl 35175 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
112, 5, 6, 10syl3anc 1477 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) ∈ (Base‘𝐾))
12 simp12 1247 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑊𝐻)
13 simp3ll 1311 . . . . . . 7 ((𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑦𝐴)
14133ad2ant3 1130 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑦𝐴)
15 cdleme22.l . . . . . . 7 = (le‘𝐾)
16 cdleme22.m . . . . . . 7 = (meet‘𝐾)
17 cdleme22.h . . . . . . 7 𝐻 = (LHyp‘𝐾)
18 cdleme22eALT.u . . . . . . 7 𝑈 = ((𝑃 𝑄) 𝑊)
19 cdleme22eALT.f . . . . . . 7 𝐹 = ((𝑦 𝑈) (𝑄 ((𝑃 𝑦) 𝑊)))
2015, 8, 16, 9, 17, 18, 19, 7cdleme1b 36035 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑦𝐴)) → 𝐹 ∈ (Base‘𝐾))
212, 12, 5, 6, 14, 20syl23anc 1484 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐹 ∈ (Base‘𝐾))
22 simp31 1252 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑆𝐴)
237, 8, 9hlatjcl 35175 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑦𝐴) → (𝑆 𝑦) ∈ (Base‘𝐾))
242, 22, 14, 23syl3anc 1477 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑆 𝑦) ∈ (Base‘𝐾))
257, 17lhpbase 35806 . . . . . . 7 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2612, 25syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑊 ∈ (Base‘𝐾))
277, 16latmcl 17274 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑆 𝑦) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑆 𝑦) 𝑊) ∈ (Base‘𝐾))
284, 24, 26, 27syl3anc 1477 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑆 𝑦) 𝑊) ∈ (Base‘𝐾))
297, 8latjcl 17273 . . . . 5 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑆 𝑦) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑆 𝑦) 𝑊)) ∈ (Base‘𝐾))
304, 21, 28, 29syl3anc 1477 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐹 ((𝑆 𝑦) 𝑊)) ∈ (Base‘𝐾))
317, 15, 16latmle1 17298 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑆 𝑦) 𝑊)) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑦) 𝑊))) (𝑃 𝑄))
324, 11, 30, 31syl3anc 1477 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑦) 𝑊))) (𝑃 𝑄))
331, 32syl5eqbr 4840 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑁 (𝑃 𝑄))
34 simp21 1249 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
35 simp13 1248 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑇𝐴)
36 simp321 1408 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑉𝐴)
37 simp322 1409 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑉 𝑊)
3836, 37jca 555 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑉𝐴𝑉 𝑊))
39 simp23 1251 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑃𝑄)
40 simp323 1410 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑉) = (𝑃 𝑄))
4115, 8, 16, 9, 17, 18cdleme22a 36149 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴𝑇𝐴) ∧ ((𝑉𝐴𝑉 𝑊) ∧ 𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄))) → 𝑉 = 𝑈)
422, 12, 34, 6, 35, 38, 39, 40, 41syl233anc 1506 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑉 = 𝑈)
4342oveq2d 6831 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑂 𝑉) = (𝑂 𝑈))
44 cdleme22eALT.o . . . . 5 𝑂 = ((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊)))
4544oveq1i 6825 . . . 4 (𝑂 𝑈) = (((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊))) 𝑈)
46 simp21r 1376 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ¬ 𝑃 𝑊)
4715, 8, 16, 9, 17, 18cdleme0a 36020 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
482, 12, 5, 46, 6, 39, 47syl222anc 1493 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈𝐴)
49 simp3rl 1313 . . . . . . . 8 ((𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧𝐴)
50493ad2ant3 1130 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑧𝐴)
51 cdleme22eALT.g . . . . . . . 8 𝐺 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
5215, 8, 16, 9, 17, 18, 51, 7cdleme1b 36035 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → 𝐺 ∈ (Base‘𝐾))
532, 12, 5, 6, 50, 52syl23anc 1484 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐺 ∈ (Base‘𝐾))
547, 8, 9hlatjcl 35175 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → (𝑇 𝑧) ∈ (Base‘𝐾))
552, 35, 50, 54syl3anc 1477 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑧) ∈ (Base‘𝐾))
567, 16latmcl 17274 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
574, 55, 26, 56syl3anc 1477 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
587, 8latjcl 17273 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝐺 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝐺 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
594, 53, 57, 58syl3anc 1477 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐺 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
6015, 8, 16, 9, 17, 18cdlemeulpq 36029 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴)) → 𝑈 (𝑃 𝑄))
612, 12, 5, 6, 60syl22anc 1478 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈 (𝑃 𝑄))
627, 15, 8, 16, 9atmod2i1 35669 . . . . 5 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐺 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑃 𝑄)) → (((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)))
632, 48, 11, 59, 61, 62syl131anc 1490 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)))
6445, 63syl5req 2808 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑂 𝑈))
6542oveq2d 6831 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑉) = (𝑇 𝑈))
6640, 65eqtr3d 2797 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) = (𝑇 𝑈))
677, 8, 9hlatjcl 35175 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
682, 35, 48, 67syl3anc 1477 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑈) ∈ (Base‘𝐾))
697, 9atbase 35098 . . . . . . . 8 (𝑧𝐴𝑧 ∈ (Base‘𝐾))
7050, 69syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑧 ∈ (Base‘𝐾))
717, 15, 8latlej1 17282 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
724, 68, 70, 71syl3anc 1477 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
738, 9hlatj32 35180 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑈𝐴𝑧𝐴)) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
742, 35, 48, 50, 73syl13anc 1479 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
757, 9atbase 35098 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
7648, 75syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈 ∈ (Base‘𝐾))
777, 8latj32 17319 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
784, 70, 76, 57, 77syl13anc 1479 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
797, 8latj32 17319 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝐺 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐺 𝑈) ((𝑇 𝑧) 𝑊)))
804, 53, 57, 76, 79syl13anc 1479 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐺 𝑈) ((𝑇 𝑧) 𝑊)))
817, 8, 9hlatjcl 35175 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → (𝑃 𝑧) ∈ (Base‘𝐾))
822, 5, 50, 81syl3anc 1477 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑧) ∈ (Base‘𝐾))
8315, 8, 9hlatlej1 35183 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → 𝑃 (𝑃 𝑧))
842, 5, 50, 83syl3anc 1477 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑃 (𝑃 𝑧))
857, 15, 8, 16, 9atmod3i1 35672 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑧)) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
862, 5, 82, 26, 84, 85syl131anc 1490 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
87 eqid 2761 . . . . . . . . . . . . . . . . . . . 20 (1.‘𝐾) = (1.‘𝐾)
8815, 8, 87, 9, 17lhpjat2 35829 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
892, 12, 34, 88syl21anc 1476 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑊) = (1.‘𝐾))
9089oveq2d 6831 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑧) (𝑃 𝑊)) = ((𝑃 𝑧) (1.‘𝐾)))
91 hlol 35170 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ HL → 𝐾 ∈ OL)
922, 91syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐾 ∈ OL)
937, 16, 87olm11 35036 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ OL ∧ (𝑃 𝑧) ∈ (Base‘𝐾)) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
9492, 82, 93syl2anc 696 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
9586, 90, 943eqtrd 2799 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 ((𝑃 𝑧) 𝑊)) = (𝑃 𝑧))
9695oveq1d 6830 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑧) 𝑄))
9718oveq2i 6826 . . . . . . . . . . . . . . . . . . 19 (𝑄 𝑈) = (𝑄 ((𝑃 𝑄) 𝑊))
9815, 8, 9hlatlej2 35184 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑄 (𝑃 𝑄))
992, 5, 6, 98syl3anc 1477 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑄 (𝑃 𝑄))
1007, 15, 8, 16, 9atmod3i1 35672 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑄𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑄 (𝑃 𝑄)) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
1012, 6, 11, 26, 99, 100syl131anc 1490 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
10297, 101syl5eq 2807 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 𝑈) = ((𝑃 𝑄) (𝑄 𝑊)))
103 simp22 1250 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
10415, 8, 87, 9, 17lhpjat2 35829 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑄 𝑊) = (1.‘𝐾))
1052, 12, 103, 104syl21anc 1476 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 𝑊) = (1.‘𝐾))
106105oveq2d 6831 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) (𝑄 𝑊)) = ((𝑃 𝑄) (1.‘𝐾)))
1077, 16, 87olm11 35036 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ OL ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
10892, 11, 107syl2anc 696 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
109102, 106, 1083eqtrd 2799 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 𝑈) = (𝑃 𝑄))
110109oveq1d 6830 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1117, 9atbase 35098 . . . . . . . . . . . . . . . . . 18 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1125, 111syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑃 ∈ (Base‘𝐾))
1137, 16latmcl 17274 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1144, 82, 26, 113syl3anc 1477 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1157, 9atbase 35098 . . . . . . . . . . . . . . . . . 18 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
1166, 115syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑄 ∈ (Base‘𝐾))
1177, 8latj32 17319 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1184, 112, 114, 116, 117syl13anc 1479 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
119110, 118eqtr4d 2798 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄))
1208, 9hlatj32 35180 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
1212, 5, 6, 50, 120syl13anc 1479 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
12296, 119, 1213eqtr4rd 2806 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) 𝑧) = ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)))
1237, 8latj32 17319 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
1244, 116, 76, 114, 123syl13anc 1479 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
125122, 124eqtrd 2795 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) 𝑧) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
126125oveq2d 6831 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1277, 8latjcl 17273 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1284, 11, 70, 127syl3anc 1477 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1297, 15, 8latlej2 17283 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧 ((𝑃 𝑄) 𝑧))
1304, 11, 70, 129syl3anc 1477 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑧 ((𝑃 𝑄) 𝑧))
1317, 15, 8, 16, 9atmod1i1 35665 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑧𝐴𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) ∧ 𝑧 ((𝑃 𝑄) 𝑧)) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
1322, 50, 76, 128, 130, 131syl131anc 1490 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
13351oveq1i 6825 . . . . . . . . . . . . 13 (𝐺 𝑈) = (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈)
1347, 8, 9hlatjcl 35175 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → (𝑧 𝑈) ∈ (Base‘𝐾))
1352, 50, 48, 134syl3anc 1477 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 𝑈) ∈ (Base‘𝐾))
1367, 8latjcl 17273 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
1374, 116, 114, 136syl3anc 1477 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
13815, 8, 9hlatlej2 35184 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → 𝑈 (𝑧 𝑈))
1392, 50, 48, 138syl3anc 1477 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈 (𝑧 𝑈))
1407, 15, 8, 16, 9atmod2i1 35669 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑧 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑧 𝑈)) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1412, 48, 135, 137, 139, 140syl131anc 1490 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
142133, 141syl5eq 2807 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐺 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
143126, 132, 1423eqtr4rd 2806 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐺 𝑈) = (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))))
1447, 15, 8latlej1 17282 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1454, 11, 70, 144syl3anc 1477 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1467, 15, 4, 76, 11, 128, 61, 145lattrd 17280 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈 ((𝑃 𝑄) 𝑧))
1477, 15, 16latleeqm1 17301 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
1484, 76, 128, 147syl3anc 1477 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
149146, 148mpbid 222 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈)
150149oveq2d 6831 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = (𝑧 𝑈))
151143, 150eqtrd 2795 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐺 𝑈) = (𝑧 𝑈))
152151oveq1d 6830 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝐺 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
15380, 152eqtrd 2795 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
15415, 8, 9hlatlej2 35184 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → 𝑧 (𝑇 𝑧))
1552, 35, 50, 154syl3anc 1477 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑧 (𝑇 𝑧))
1567, 15, 8, 16, 9atmod3i1 35672 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑧𝐴 ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑧 (𝑇 𝑧)) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
1572, 50, 55, 26, 155, 156syl131anc 1490 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
158 simp33r 1386 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧𝐴 ∧ ¬ 𝑧 𝑊))
15915, 8, 87, 9, 17lhpjat2 35829 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)) → (𝑧 𝑊) = (1.‘𝐾))
1602, 12, 158, 159syl21anc 1476 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 𝑊) = (1.‘𝐾))
161160oveq2d 6831 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) (𝑧 𝑊)) = ((𝑇 𝑧) (1.‘𝐾)))
1627, 16, 87olm11 35036 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ (𝑇 𝑧) ∈ (Base‘𝐾)) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
16392, 55, 162syl2anc 696 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
164157, 161, 1633eqtrrd 2800 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑧) = (𝑧 ((𝑇 𝑧) 𝑊)))
165164oveq1d 6830 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) 𝑈) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
16678, 153, 1653eqtr4rd 2806 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) 𝑈) = ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈))
16774, 166eqtrd 2795 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑈) 𝑧) = ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈))
16872, 167breqtrd 4831 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑈) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈))
16966, 168eqbrtrd 4827 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈))
1707, 8latjcl 17273 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝐺 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1714, 59, 76, 170syl3anc 1477 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1727, 15, 16latleeqm1 17301 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾)) → ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
1734, 11, 171, 172syl3anc 1477 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
174169, 173mpbid 222 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄))
17543, 64, 1743eqtr2rd 2802 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) = (𝑂 𝑉))
17633, 175breqtrd 4831 1 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑁 (𝑂 𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2140  wne 2933   class class class wbr 4805  cfv 6050  (class class class)co 6815  Basecbs 16080  lecple 16171  joincjn 17166  meetcmee 17167  1.cp1 17260  Latclat 17267  OLcol 34983  Atomscatm 35072  HLchlt 35159  LHypclh 35792
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 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
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 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-iun 4675  df-iin 4676  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-1st 7335  df-2nd 7336  df-preset 17150  df-poset 17168  df-plt 17180  df-lub 17196  df-glb 17197  df-join 17198  df-meet 17199  df-p0 17261  df-p1 17262  df-lat 17268  df-clat 17330  df-oposet 34985  df-ol 34987  df-oml 34988  df-covers 35075  df-ats 35076  df-atl 35107  df-cvlat 35131  df-hlat 35160  df-psubsp 35311  df-pmap 35312  df-padd 35604  df-lhyp 35796
This theorem is referenced by:  cdleme26eALTN  36170
  Copyright terms: Public domain W3C validator