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

Theorem cdleme27a 37656
 Description: Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 37652 with s and t swapped (this case is not mentioned by them). If s ≤ t ∨ v, then f(s) ≤ fs(t) ∨ v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.)
Hypotheses
Ref Expression
cdleme26.b 𝐵 = (Base‘𝐾)
cdleme26.l = (le‘𝐾)
cdleme26.j = (join‘𝐾)
cdleme26.m = (meet‘𝐾)
cdleme26.a 𝐴 = (Atoms‘𝐾)
cdleme26.h 𝐻 = (LHyp‘𝐾)
cdleme27.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme27.f 𝐹 = ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊)))
cdleme27.z 𝑍 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
cdleme27.n 𝑁 = ((𝑃 𝑄) (𝑍 ((𝑠 𝑧) 𝑊)))
cdleme27.d 𝐷 = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑁))
cdleme27.c 𝐶 = if(𝑠 (𝑃 𝑄), 𝐷, 𝐹)
cdleme27.g 𝐺 = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊)))
cdleme27.o 𝑂 = ((𝑃 𝑄) (𝑍 ((𝑡 𝑧) 𝑊)))
cdleme27.e 𝐸 = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑂))
cdleme27.y 𝑌 = if(𝑡 (𝑃 𝑄), 𝐸, 𝐺)
Assertion
Ref Expression
cdleme27a ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐶 (𝑌 𝑉))
Distinct variable groups:   𝑡,𝑠,𝑢,𝑧,𝐴   𝐵,𝑠,𝑡,𝑢,𝑧   𝑢,𝐹   𝑢,𝐺   𝐻,𝑠,𝑡,𝑧   ,𝑠,𝑡,𝑢,𝑧   𝐾,𝑠,𝑡,𝑧   ,𝑠,𝑡,𝑢,𝑧   ,𝑠,𝑡,𝑢,𝑧   𝑡,𝑁,𝑢   𝑂,𝑠,𝑢   𝑃,𝑠,𝑡,𝑢,𝑧   𝑄,𝑠,𝑡,𝑢,𝑧   𝑈,𝑠,𝑡,𝑢,𝑧   𝑧,𝑉   𝑊,𝑠,𝑡,𝑢,𝑧
Allowed substitution hints:   𝐶(𝑧,𝑢,𝑡,𝑠)   𝐷(𝑧,𝑢,𝑡,𝑠)   𝐸(𝑧,𝑢,𝑡,𝑠)   𝐹(𝑧,𝑡,𝑠)   𝐺(𝑧,𝑡,𝑠)   𝐻(𝑢)   𝐾(𝑢)   𝑁(𝑧,𝑠)   𝑂(𝑧,𝑡)   𝑉(𝑢,𝑡,𝑠)   𝑌(𝑧,𝑢,𝑡,𝑠)   𝑍(𝑧,𝑢,𝑡,𝑠)

Proof of Theorem cdleme27a
StepHypRef Expression
1 simp211 1308 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 simp221 1311 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
3 simp222 1312 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
4 simp213 1310 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → (𝑠𝐴 ∧ ¬ 𝑠 𝑊))
5 simp223 1313 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → (𝑡𝐴 ∧ ¬ 𝑡 𝑊))
6 simp23r 1292 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → (𝑉𝐴𝑉 𝑊))
7 simp212 1309 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → 𝑃𝑄)
8 simp1l 1194 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → 𝑠 (𝑃 𝑄))
9 simp1r 1195 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → 𝑡 (𝑃 𝑄))
107, 8, 93jca 1125 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → (𝑃𝑄𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)))
11 simp3 1135 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → (𝑡 𝑉) = (𝑃 𝑄))
12 cdleme26.b . . . . . . . 8 𝐵 = (Base‘𝐾)
13 cdleme26.l . . . . . . . 8 = (le‘𝐾)
14 cdleme26.j . . . . . . . 8 = (join‘𝐾)
15 cdleme26.m . . . . . . . 8 = (meet‘𝐾)
16 cdleme26.a . . . . . . . 8 𝐴 = (Atoms‘𝐾)
17 cdleme26.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
18 cdleme27.u . . . . . . . 8 𝑈 = ((𝑃 𝑄) 𝑊)
19 cdleme27.z . . . . . . . 8 𝑍 = ((𝑧 𝑈) (𝑄 ((𝑃 𝑧) 𝑊)))
20 cdleme27.n . . . . . . . 8 𝑁 = ((𝑃 𝑄) (𝑍 ((𝑠 𝑧) 𝑊)))
21 cdleme27.o . . . . . . . 8 𝑂 = ((𝑃 𝑄) (𝑍 ((𝑡 𝑧) 𝑊)))
22 cdleme27.d . . . . . . . 8 𝐷 = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑁))
23 cdleme27.e . . . . . . . 8 𝐸 = (𝑢𝐵𝑧𝐴 ((¬ 𝑧 𝑊 ∧ ¬ 𝑧 (𝑃 𝑄)) → 𝑢 = 𝑂))
2412, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23cdleme26ee 37649 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑠𝐴 ∧ ¬ 𝑠 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ ((𝑃𝑄𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (𝑡 𝑉) = (𝑃 𝑄))) → 𝐷 (𝐸 𝑉))
251, 2, 3, 4, 5, 6, 10, 11, 24syl332anc 1398 . . . . . 6 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) = (𝑃 𝑄)) → 𝐷 (𝐸 𝑉))
26253expia 1118 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → ((𝑡 𝑉) = (𝑃 𝑄) → 𝐷 (𝐸 𝑉)))
27 simp1r 1195 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑡 (𝑃 𝑄))
28 simp11l 1281 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐾 ∈ HL)
29283ad2ant2 1131 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝐾 ∈ HL)
30 simp13l 1285 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝑠𝐴)
31303ad2ant2 1131 . . . . . . . . 9 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑠𝐴)
32 simp23l 1291 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝑡𝐴)
33323ad2ant2 1131 . . . . . . . . 9 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑡𝐴)
34 simp3ll 1241 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝑠𝑡)
35343ad2ant2 1131 . . . . . . . . 9 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑠𝑡)
3631, 33, 353jca 1125 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → (𝑠𝐴𝑡𝐴𝑠𝑡))
37 simp21l 1287 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝑃𝐴)
38373ad2ant2 1131 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑃𝐴)
39 simp22l 1289 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝑄𝐴)
40393ad2ant2 1131 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑄𝐴)
41 simp212 1309 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑃𝑄)
42 simp3rl 1243 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝑉𝐴)
43423ad2ant2 1131 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑉𝐴)
44 simp3 1135 . . . . . . . . 9 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → (𝑡 𝑉) ≠ (𝑃 𝑄))
45 simp3lr 1242 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝑠 (𝑡 𝑉))
46453ad2ant2 1131 . . . . . . . . 9 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑠 (𝑡 𝑉))
47 simp1l 1194 . . . . . . . . 9 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝑠 (𝑃 𝑄))
4844, 46, 473jca 1125 . . . . . . . 8 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → ((𝑡 𝑉) ≠ (𝑃 𝑄) ∧ 𝑠 (𝑡 𝑉) ∧ 𝑠 (𝑃 𝑄)))
4913, 14, 15, 16, 17cdleme22b 37630 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑠𝐴𝑡𝐴𝑠𝑡)) ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑉𝐴 ∧ ((𝑡 𝑉) ≠ (𝑃 𝑄) ∧ 𝑠 (𝑡 𝑉) ∧ 𝑠 (𝑃 𝑄)))) → ¬ 𝑡 (𝑃 𝑄))
5029, 36, 38, 40, 41, 43, 48, 49syl232anc 1394 . . . . . . 7 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → ¬ 𝑡 (𝑃 𝑄))
5127, 50pm2.21dd 198 . . . . . 6 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) ∧ (𝑡 𝑉) ≠ (𝑃 𝑄)) → 𝐷 (𝐸 𝑉))
52513expia 1118 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → ((𝑡 𝑉) ≠ (𝑃 𝑄) → 𝐷 (𝐸 𝑉)))
5326, 52pm2.61dne 3076 . . . 4 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐷 (𝐸 𝑉))
54 cdleme27.c . . . . . 6 𝐶 = if(𝑠 (𝑃 𝑄), 𝐷, 𝐹)
55 iftrue 4434 . . . . . 6 (𝑠 (𝑃 𝑄) → if(𝑠 (𝑃 𝑄), 𝐷, 𝐹) = 𝐷)
5654, 55syl5eq 2848 . . . . 5 (𝑠 (𝑃 𝑄) → 𝐶 = 𝐷)
5756ad2antrr 725 . . . 4 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐶 = 𝐷)
58 cdleme27.y . . . . . . 7 𝑌 = if(𝑡 (𝑃 𝑄), 𝐸, 𝐺)
59 iftrue 4434 . . . . . . 7 (𝑡 (𝑃 𝑄) → if(𝑡 (𝑃 𝑄), 𝐸, 𝐺) = 𝐸)
6058, 59syl5eq 2848 . . . . . 6 (𝑡 (𝑃 𝑄) → 𝑌 = 𝐸)
6160oveq1d 7154 . . . . 5 (𝑡 (𝑃 𝑄) → (𝑌 𝑉) = (𝐸 𝑉))
6261ad2antlr 726 . . . 4 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑌 𝑉) = (𝐸 𝑉))
6353, 57, 623brtr4d 5065 . . 3 (((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐶 (𝑌 𝑉))
6463ex 416 . 2 ((𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐶 (𝑌 𝑉)))
65 simpr11 1254 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
66 simpr12 1255 . . . . . 6 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝑃𝑄)
67 simpll 766 . . . . . 6 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝑠 (𝑃 𝑄))
6866, 67jca 515 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑃𝑄𝑠 (𝑃 𝑄)))
69 simpr23 1259 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑡𝐴 ∧ ¬ 𝑡 𝑊))
70 simpr21 1257 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
71 simpr22 1258 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
72 simpr13 1256 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑠𝐴 ∧ ¬ 𝑠 𝑊))
73 simplr 768 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → ¬ 𝑡 (𝑃 𝑄))
74 simpr3l 1231 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑠𝑡𝑠 (𝑡 𝑉)))
75 simpr3r 1232 . . . . 5 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑉𝐴𝑉 𝑊))
76 cdleme27.g . . . . . 6 𝐺 = ((𝑡 𝑈) (𝑄 ((𝑃 𝑡) 𝑊)))
77 eqid 2801 . . . . . 6 ((𝑃 𝑄) (𝐺 ((𝑠 𝑡) 𝑊))) = ((𝑃 𝑄) (𝐺 ((𝑠 𝑡) 𝑊)))
78 eqid 2801 . . . . . . 7 (𝑢𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑢 = ((𝑃 𝑄) (𝐺 ((𝑠 𝑡) 𝑊))))) = (𝑢𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑢 = ((𝑃 𝑄) (𝐺 ((𝑠 𝑡) 𝑊)))))
7919, 20, 76, 77, 22, 78cdleme25cv 37647 . . . . . 6 𝐷 = (𝑢𝐵𝑡𝐴 ((¬ 𝑡 𝑊 ∧ ¬ 𝑡 (𝑃 𝑄)) → 𝑢 = ((𝑃 𝑄) (𝐺 ((𝑠 𝑡) 𝑊)))))
8012, 13, 14, 15, 16, 17, 18, 76, 77, 79cdleme26f 37652 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝑄𝑠 (𝑃 𝑄)) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ (¬ 𝑡 (𝑃 𝑄) ∧ (𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐷 (𝐺 𝑉))
8165, 68, 69, 70, 71, 72, 73, 74, 75, 80syl333anc 1399 . . . 4 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐷 (𝐺 𝑉))
8256ad2antrr 725 . . . 4 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐶 = 𝐷)
83 iffalse 4437 . . . . . . 7 𝑡 (𝑃 𝑄) → if(𝑡 (𝑃 𝑄), 𝐸, 𝐺) = 𝐺)
8458, 83syl5eq 2848 . . . . . 6 𝑡 (𝑃 𝑄) → 𝑌 = 𝐺)
8584oveq1d 7154 . . . . 5 𝑡 (𝑃 𝑄) → (𝑌 𝑉) = (𝐺 𝑉))
8685ad2antlr 726 . . . 4 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑌 𝑉) = (𝐺 𝑉))
8781, 82, 863brtr4d 5065 . . 3 (((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐶 (𝑌 𝑉))
8887ex 416 . 2 ((𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐶 (𝑌 𝑉)))
89 simpr11 1254 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
90 simpr12 1255 . . . . . 6 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝑃𝑄)
91 simplr 768 . . . . . 6 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝑡 (𝑃 𝑄))
9290, 91jca 515 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑃𝑄𝑡 (𝑃 𝑄)))
93 simpr13 1256 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑠𝐴 ∧ ¬ 𝑠 𝑊))
94 simpr21 1257 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
95 simpr22 1258 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
96 simpr23 1259 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑡𝐴 ∧ ¬ 𝑡 𝑊))
97 simpll 766 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → ¬ 𝑠 (𝑃 𝑄))
98 simpr3l 1231 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑠𝑡𝑠 (𝑡 𝑉)))
99 simpr3r 1232 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑉𝐴𝑉 𝑊))
100 cdleme27.f . . . . . 6 𝐹 = ((𝑠 𝑈) (𝑄 ((𝑃 𝑠) 𝑊)))
101 eqid 2801 . . . . . 6 ((𝑃 𝑄) (𝐹 ((𝑡 𝑠) 𝑊))) = ((𝑃 𝑄) (𝐹 ((𝑡 𝑠) 𝑊)))
102 eqid 2801 . . . . . . 7 (𝑢𝐵𝑠𝐴 ((¬ 𝑠 𝑊 ∧ ¬ 𝑠 (𝑃 𝑄)) → 𝑢 = ((𝑃 𝑄) (𝐹 ((𝑡 𝑠) 𝑊))))) = (𝑢𝐵𝑠𝐴 ((¬ 𝑠 𝑊 ∧ ¬ 𝑠 (𝑃 𝑄)) → 𝑢 = ((𝑃 𝑄) (𝐹 ((𝑡 𝑠) 𝑊)))))
10319, 21, 100, 101, 23, 102cdleme25cv 37647 . . . . . 6 𝐸 = (𝑢𝐵𝑠𝐴 ((¬ 𝑠 𝑊 ∧ ¬ 𝑠 (𝑃 𝑄)) → 𝑢 = ((𝑃 𝑄) (𝐹 ((𝑡 𝑠) 𝑊)))))
10412, 13, 14, 15, 16, 17, 18, 100, 101, 103cdleme26f2 37654 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝑄𝑡 (𝑃 𝑄)) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ (¬ 𝑠 (𝑃 𝑄) ∧ (𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐹 (𝐸 𝑉))
10589, 92, 93, 94, 95, 96, 97, 98, 99, 104syl333anc 1399 . . . 4 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐹 (𝐸 𝑉))
106 iffalse 4437 . . . . . 6 𝑠 (𝑃 𝑄) → if(𝑠 (𝑃 𝑄), 𝐷, 𝐹) = 𝐹)
10754, 106syl5eq 2848 . . . . 5 𝑠 (𝑃 𝑄) → 𝐶 = 𝐹)
108107ad2antrr 725 . . . 4 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐶 = 𝐹)
10961ad2antlr 726 . . . 4 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑌 𝑉) = (𝐸 𝑉))
110105, 108, 1093brtr4d 5065 . . 3 (((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐶 (𝑌 𝑉))
111110ex 416 . 2 ((¬ 𝑠 (𝑃 𝑄) ∧ 𝑡 (𝑃 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐶 (𝑌 𝑉)))
112 simpr11 1254 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
113 simpr23 1259 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑡𝐴 ∧ ¬ 𝑡 𝑊))
114 simplr 768 . . . . . 6 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → ¬ 𝑡 (𝑃 𝑄))
115 simpll 766 . . . . . 6 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → ¬ 𝑠 (𝑃 𝑄))
116 simpr12 1255 . . . . . 6 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝑃𝑄)
117114, 115, 1163jca 1125 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (¬ 𝑡 (𝑃 𝑄) ∧ ¬ 𝑠 (𝑃 𝑄) ∧ 𝑃𝑄))
118 simpr21 1257 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
119 simpr22 1258 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
120 simpr13 1256 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑠𝐴 ∧ ¬ 𝑠 𝑊))
121 simpr3l 1231 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑠𝑡𝑠 (𝑡 𝑉)))
122 simpr3r 1232 . . . . 5 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑉𝐴𝑉 𝑊))
12313, 14, 15, 16, 17, 18, 100, 76cdleme22g 37637 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊) ∧ (¬ 𝑡 (𝑃 𝑄) ∧ ¬ 𝑠 (𝑃 𝑄) ∧ 𝑃𝑄)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑠𝐴 ∧ ¬ 𝑠 𝑊) ∧ (𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐹 (𝐺 𝑉))
124112, 113, 117, 118, 119, 120, 121, 122, 123syl323anc 1397 . . . 4 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐹 (𝐺 𝑉))
125107ad2antrr 725 . . . 4 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐶 = 𝐹)
12685ad2antlr 726 . . . 4 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → (𝑌 𝑉) = (𝐺 𝑉))
127124, 125, 1263brtr4d 5065 . . 3 (((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) ∧ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊)))) → 𝐶 (𝑌 𝑉))
128127ex 416 . 2 ((¬ 𝑠 (𝑃 𝑄) ∧ ¬ 𝑡 (𝑃 𝑄)) → ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐶 (𝑌 𝑉)))
12964, 88, 111, 1284cases 1036 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑡𝐴 ∧ ¬ 𝑡 𝑊)) ∧ ((𝑠𝑡𝑠 (𝑡 𝑉)) ∧ (𝑉𝐴𝑉 𝑊))) → 𝐶 (𝑌 𝑉))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112   ≠ wne 2990  ∀wral 3109  ifcif 4428   class class class wbr 5033  ‘cfv 6328  ℩crio 7096  (class class class)co 7139  Basecbs 16478  lecple 16567  joincjn 17549  meetcmee 17550  Atomscatm 36552  HLchlt 36639  LHypclh 37273 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-riotaBAD 36242 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-1st 7675  df-2nd 7676  df-undef 7926  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-p1 17645  df-lat 17651  df-clat 17713  df-oposet 36465  df-ol 36467  df-oml 36468  df-covers 36555  df-ats 36556  df-atl 36587  df-cvlat 36611  df-hlat 36640  df-llines 36787  df-lplanes 36788  df-lvols 36789  df-lines 36790  df-psubsp 36792  df-pmap 36793  df-padd 37085  df-lhyp 37277 This theorem is referenced by:  cdleme27N  37658  cdleme28a  37659
 Copyright terms: Public domain W3C validator