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 40044
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 1200 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐾 ∈ HL)
32hllatd 39062 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐾 ∈ Lat)
4 simp21l 1287 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑃𝐴)
5 simp22l 1289 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑄𝐴)
6 eqid 2726 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
7 cdleme22.j . . . . . 6 = (join‘𝐾)
8 cdleme22.a . . . . . 6 𝐴 = (Atoms‘𝐾)
96, 7, 8hlatjcl 39065 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
102, 4, 5, 9syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) ∈ (Base‘𝐾))
11 simp12 1201 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑊𝐻)
12 simp3ll 1241 . . . . . . 7 ((𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑦𝐴)
13123ad2ant3 1132 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑦𝐴)
14 cdleme22.l . . . . . . 7 = (le‘𝐾)
15 cdleme22.m . . . . . . 7 = (meet‘𝐾)
16 cdleme22.h . . . . . . 7 𝐻 = (LHyp‘𝐾)
17 cdleme22eALT.u . . . . . . 7 𝑈 = ((𝑃 𝑄) 𝑊)
18 cdleme22eALT.f . . . . . . 7 𝐹 = ((𝑦 𝑈) (𝑄 ((𝑃 𝑦) 𝑊)))
1914, 7, 15, 8, 16, 17, 18, 6cdleme1b 39925 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑦𝐴)) → 𝐹 ∈ (Base‘𝐾))
202, 11, 4, 5, 13, 19syl23anc 1374 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐹 ∈ (Base‘𝐾))
21 simp31 1206 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑆𝐴)
226, 7, 8hlatjcl 39065 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑦𝐴) → (𝑆 𝑦) ∈ (Base‘𝐾))
232, 21, 13, 22syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑆 𝑦) ∈ (Base‘𝐾))
246, 16lhpbase 39697 . . . . . . 7 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2511, 24syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑊 ∈ (Base‘𝐾))
266, 15latmcl 18465 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑆 𝑦) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑆 𝑦) 𝑊) ∈ (Base‘𝐾))
273, 23, 25, 26syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑆 𝑦) 𝑊) ∈ (Base‘𝐾))
286, 7latjcl 18464 . . . . 5 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑆 𝑦) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑆 𝑦) 𝑊)) ∈ (Base‘𝐾))
293, 20, 27, 28syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐹 ((𝑆 𝑦) 𝑊)) ∈ (Base‘𝐾))
306, 14, 15latmle1 18489 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑆 𝑦) 𝑊)) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑦) 𝑊))) (𝑃 𝑄))
313, 10, 29, 30syl3anc 1368 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) (𝐹 ((𝑆 𝑦) 𝑊))) (𝑃 𝑄))
321, 31eqbrtrid 5188 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑁 (𝑃 𝑄))
33 simp21 1203 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
34 simp13 1202 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑇𝐴)
35 simp321 1320 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑉𝐴)
36 simp322 1321 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑉 𝑊)
3735, 36jca 510 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑉𝐴𝑉 𝑊))
38 simp23 1205 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑃𝑄)
39 simp323 1322 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑉) = (𝑃 𝑄))
4014, 7, 15, 8, 16, 17cdleme22a 40039 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑄𝐴𝑇𝐴) ∧ ((𝑉𝐴𝑉 𝑊) ∧ 𝑃𝑄 ∧ (𝑇 𝑉) = (𝑃 𝑄))) → 𝑉 = 𝑈)
412, 11, 33, 5, 34, 37, 38, 39, 40syl233anc 1396 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑉 = 𝑈)
4241oveq2d 7440 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑂 𝑉) = (𝑂 𝑈))
43 cdleme22eALT.o . . . . 5 𝑂 = ((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊)))
4443oveq1i 7434 . . . 4 (𝑂 𝑈) = (((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊))) 𝑈)
45 simp21r 1288 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ¬ 𝑃 𝑊)
4614, 7, 15, 8, 16, 17cdleme0a 39910 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
472, 11, 4, 45, 5, 38, 46syl222anc 1383 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈𝐴)
48 simp3rl 1243 . . . . . . . 8 ((𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊))) → 𝑧𝐴)
49483ad2ant3 1132 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑧𝐴)
50 cdleme22eALT.g . . . . . . . 8 𝐺 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
5114, 7, 15, 8, 16, 17, 50, 6cdleme1b 39925 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → 𝐺 ∈ (Base‘𝐾))
522, 11, 4, 5, 49, 51syl23anc 1374 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐺 ∈ (Base‘𝐾))
536, 7, 8hlatjcl 39065 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → (𝑇 𝑧) ∈ (Base‘𝐾))
542, 34, 49, 53syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑧) ∈ (Base‘𝐾))
556, 15latmcl 18465 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
563, 54, 25, 55syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))
576, 7latjcl 18464 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝐺 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝐺 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
583, 52, 56, 57syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐺 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾))
5914, 7, 15, 8, 16, 17cdlemeulpq 39919 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴)) → 𝑈 (𝑃 𝑄))
602, 11, 4, 5, 59syl22anc 837 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈 (𝑃 𝑄))
616, 14, 7, 15, 8atmod2i1 39560 . . . . 5 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐺 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑃 𝑄)) → (((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)))
622, 47, 10, 58, 60, 61syl131anc 1380 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (((𝑃 𝑄) (𝐺 ((𝑇 𝑧) 𝑊))) 𝑈) = ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)))
6344, 62eqtr2id 2779 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑂 𝑈))
6441oveq2d 7440 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑉) = (𝑇 𝑈))
6539, 64eqtr3d 2768 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) = (𝑇 𝑈))
666, 7, 8hlatjcl 39065 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴) → (𝑇 𝑈) ∈ (Base‘𝐾))
672, 34, 47, 66syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑈) ∈ (Base‘𝐾))
686, 8atbase 38987 . . . . . . . 8 (𝑧𝐴𝑧 ∈ (Base‘𝐾))
6949, 68syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑧 ∈ (Base‘𝐾))
706, 14, 7latlej1 18473 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑇 𝑈) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
713, 67, 69, 70syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑈) ((𝑇 𝑈) 𝑧))
727, 8hlatj32 39070 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑈𝐴𝑧𝐴)) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
732, 34, 47, 49, 72syl13anc 1369 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑈) 𝑧) = ((𝑇 𝑧) 𝑈))
746, 8atbase 38987 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
7547, 74syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈 ∈ (Base‘𝐾))
766, 7latj32 18510 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
773, 69, 75, 56, 76syl13anc 1369 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
786, 7latj32 18510 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝐺 ∈ (Base‘𝐾) ∧ ((𝑇 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐺 𝑈) ((𝑇 𝑧) 𝑊)))
793, 52, 56, 75, 78syl13anc 1369 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝐺 𝑈) ((𝑇 𝑧) 𝑊)))
806, 7, 8hlatjcl 39065 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → (𝑃 𝑧) ∈ (Base‘𝐾))
812, 4, 49, 80syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑧) ∈ (Base‘𝐾))
8214, 7, 8hlatlej1 39073 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑧𝐴) → 𝑃 (𝑃 𝑧))
832, 4, 49, 82syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑃 (𝑃 𝑧))
846, 14, 7, 15, 8atmod3i1 39563 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑧)) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
852, 4, 81, 25, 83, 84syl131anc 1380 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑧) (𝑃 𝑊)))
86 eqid 2726 . . . . . . . . . . . . . . . . . . . 20 (1.‘𝐾) = (1.‘𝐾)
8714, 7, 86, 8, 16lhpjat2 39720 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
882, 11, 33, 87syl21anc 836 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑊) = (1.‘𝐾))
8988oveq2d 7440 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑧) (𝑃 𝑊)) = ((𝑃 𝑧) (1.‘𝐾)))
90 hlol 39059 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ HL → 𝐾 ∈ OL)
912, 90syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝐾 ∈ OL)
926, 15, 86olm11 38925 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ OL ∧ (𝑃 𝑧) ∈ (Base‘𝐾)) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
9391, 81, 92syl2anc 582 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑧) (1.‘𝐾)) = (𝑃 𝑧))
9485, 89, 933eqtrd 2770 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 ((𝑃 𝑧) 𝑊)) = (𝑃 𝑧))
9594oveq1d 7439 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑧) 𝑄))
9617oveq2i 7435 . . . . . . . . . . . . . . . . . . 19 (𝑄 𝑈) = (𝑄 ((𝑃 𝑄) 𝑊))
9714, 7, 8hlatlej2 39074 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑄 (𝑃 𝑄))
982, 4, 5, 97syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑄 (𝑃 𝑄))
996, 14, 7, 15, 8atmod3i1 39563 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑄𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑄 (𝑃 𝑄)) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
1002, 5, 10, 25, 98, 99syl131anc 1380 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 ((𝑃 𝑄) 𝑊)) = ((𝑃 𝑄) (𝑄 𝑊)))
10196, 100eqtrid 2778 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 𝑈) = ((𝑃 𝑄) (𝑄 𝑊)))
102 simp22 1204 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
10314, 7, 86, 8, 16lhpjat2 39720 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑄 𝑊) = (1.‘𝐾))
1042, 11, 102, 103syl21anc 836 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 𝑊) = (1.‘𝐾))
105104oveq2d 7440 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) (𝑄 𝑊)) = ((𝑃 𝑄) (1.‘𝐾)))
1066, 15, 86olm11 38925 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ OL ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
10791, 10, 106syl2anc 582 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) (1.‘𝐾)) = (𝑃 𝑄))
108101, 105, 1073eqtrd 2770 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 𝑈) = (𝑃 𝑄))
109108oveq1d 7439 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1106, 8atbase 38987 . . . . . . . . . . . . . . . . . 18 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1114, 110syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑃 ∈ (Base‘𝐾))
1126, 15latmcl 18465 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑃 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1133, 81, 25, 112syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))
1146, 8atbase 38987 . . . . . . . . . . . . . . . . . 18 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
1155, 114syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑄 ∈ (Base‘𝐾))
1166, 7latj32 18510 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
1173, 111, 113, 115, 116syl13anc 1369 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄) = ((𝑃 𝑄) ((𝑃 𝑧) 𝑊)))
118109, 117eqtr4d 2769 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑃 ((𝑃 𝑧) 𝑊)) 𝑄))
1197, 8hlatj32 39070 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑧𝐴)) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
1202, 4, 5, 49, 119syl13anc 1369 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) 𝑧) = ((𝑃 𝑧) 𝑄))
12195, 118, 1203eqtr4rd 2777 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) 𝑧) = ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)))
1226, 7latj32 18510 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
1233, 115, 75, 113, 122syl13anc 1369 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑄 𝑈) ((𝑃 𝑧) 𝑊)) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
124121, 123eqtrd 2766 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) 𝑧) = ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈))
125124oveq2d 7440 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1266, 7latjcl 18464 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1273, 10, 69, 126syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾))
1286, 14, 7latlej2 18474 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧 ((𝑃 𝑄) 𝑧))
1293, 10, 69, 128syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑧 ((𝑃 𝑄) 𝑧))
1306, 14, 7, 15, 8atmod1i1 39556 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑧𝐴𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) ∧ 𝑧 ((𝑃 𝑄) 𝑧)) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
1312, 49, 75, 127, 129, 130syl131anc 1380 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = ((𝑧 𝑈) ((𝑃 𝑄) 𝑧)))
13250oveq1i 7434 . . . . . . . . . . . . 13 (𝐺 𝑈) = (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈)
1336, 7, 8hlatjcl 39065 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → (𝑧 𝑈) ∈ (Base‘𝐾))
1342, 49, 47, 133syl3anc 1368 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 𝑈) ∈ (Base‘𝐾))
1356, 7latjcl 18464 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑧) 𝑊) ∈ (Base‘𝐾)) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
1363, 115, 113, 135syl3anc 1368 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾))
13714, 7, 8hlatlej2 39074 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧𝐴𝑈𝐴) → 𝑈 (𝑧 𝑈))
1382, 49, 47, 137syl3anc 1368 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈 (𝑧 𝑈))
1396, 14, 7, 15, 8atmod2i1 39560 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑧 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ((𝑃 𝑧) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑈 (𝑧 𝑈)) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
1402, 47, 134, 136, 138, 139syl131anc 1380 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊))) 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
141132, 140eqtrid 2778 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐺 𝑈) = ((𝑧 𝑈) ((𝑄 ((𝑃 𝑧) 𝑊)) 𝑈)))
142125, 131, 1413eqtr4rd 2777 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐺 𝑈) = (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))))
1436, 14, 7latlej1 18473 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1443, 10, 69, 143syl3anc 1368 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) ((𝑃 𝑄) 𝑧))
1456, 14, 3, 75, 10, 127, 60, 144lattrd 18471 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑈 ((𝑃 𝑄) 𝑧))
1466, 14, 15latleeqm1 18492 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑧) ∈ (Base‘𝐾)) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
1473, 75, 127, 146syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑈 ((𝑃 𝑄) 𝑧) ↔ (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈))
148145, 147mpbid 231 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑈 ((𝑃 𝑄) 𝑧)) = 𝑈)
149148oveq2d 7440 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 (𝑈 ((𝑃 𝑄) 𝑧))) = (𝑧 𝑈))
150142, 149eqtrd 2766 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝐺 𝑈) = (𝑧 𝑈))
151150oveq1d 7439 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝐺 𝑈) ((𝑇 𝑧) 𝑊)) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
15279, 151eqtrd 2766 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) = ((𝑧 𝑈) ((𝑇 𝑧) 𝑊)))
15314, 7, 8hlatlej2 39074 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑇𝐴𝑧𝐴) → 𝑧 (𝑇 𝑧))
1542, 34, 49, 153syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑧 (𝑇 𝑧))
1556, 14, 7, 15, 8atmod3i1 39563 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑧𝐴 ∧ (𝑇 𝑧) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑧 (𝑇 𝑧)) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
1562, 49, 54, 25, 154, 155syl131anc 1380 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 ((𝑇 𝑧) 𝑊)) = ((𝑇 𝑧) (𝑧 𝑊)))
157 simp33r 1298 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧𝐴 ∧ ¬ 𝑧 𝑊))
15814, 7, 86, 8, 16lhpjat2 39720 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)) → (𝑧 𝑊) = (1.‘𝐾))
1592, 11, 157, 158syl21anc 836 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑧 𝑊) = (1.‘𝐾))
160159oveq2d 7440 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) (𝑧 𝑊)) = ((𝑇 𝑧) (1.‘𝐾)))
1616, 15, 86olm11 38925 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ (𝑇 𝑧) ∈ (Base‘𝐾)) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
16291, 54, 161syl2anc 582 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) (1.‘𝐾)) = (𝑇 𝑧))
163156, 160, 1623eqtrrd 2771 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑧) = (𝑧 ((𝑇 𝑧) 𝑊)))
164163oveq1d 7439 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) 𝑈) = ((𝑧 ((𝑇 𝑧) 𝑊)) 𝑈))
16577, 152, 1643eqtr4rd 2777 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑧) 𝑈) = ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈))
16673, 165eqtrd 2766 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑇 𝑈) 𝑧) = ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈))
16771, 166breqtrd 5179 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑇 𝑈) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈))
16865, 167eqbrtrd 5175 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈))
1696, 7latjcl 18464 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝐺 ((𝑇 𝑧) 𝑊)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1703, 58, 75, 169syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾))
1716, 14, 15latleeqm1 18492 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ∈ (Base‘𝐾)) → ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
1723, 10, 170, 171syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈) ↔ ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄)))
173168, 172mpbid 231 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → ((𝑃 𝑄) ((𝐺 ((𝑇 𝑧) 𝑊)) 𝑈)) = (𝑃 𝑄))
17442, 63, 1733eqtr2rd 2773 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → (𝑃 𝑄) = (𝑂 𝑉))
17532, 174breqtrd 5179 1 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐴) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑃𝑄) ∧ (𝑆𝐴 ∧ (𝑉𝐴𝑉 𝑊 ∧ (𝑇 𝑉) = (𝑃 𝑄)) ∧ ((𝑦𝐴 ∧ ¬ 𝑦 𝑊) ∧ (𝑧𝐴 ∧ ¬ 𝑧 𝑊)))) → 𝑁 (𝑂 𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930   class class class wbr 5153  cfv 6554  (class class class)co 7424  Basecbs 17213  lecple 17273  joincjn 18336  meetcmee 18337  1.cp1 18449  Latclat 18456  OLcol 38872  Atomscatm 38961  HLchlt 39048  LHypclh 39683
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 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-1st 8003  df-2nd 8004  df-proset 18320  df-poset 18338  df-plt 18355  df-lub 18371  df-glb 18372  df-join 18373  df-meet 18374  df-p0 18450  df-p1 18451  df-lat 18457  df-clat 18524  df-oposet 38874  df-ol 38876  df-oml 38877  df-covers 38964  df-ats 38965  df-atl 38996  df-cvlat 39020  df-hlat 39049  df-psubsp 39202  df-pmap 39203  df-padd 39495  df-lhyp 39687
This theorem is referenced by:  cdleme26eALTN  40060
  Copyright terms: Public domain W3C validator