Users' Mathboxes 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