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

Theorem cdleme20l 39851
Description: Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. 𝐷, 𝐹, π‘Œ, 𝐺 represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.)
Hypotheses
Ref Expression
cdleme19.l ≀ = (leβ€˜πΎ)
cdleme19.j ∨ = (joinβ€˜πΎ)
cdleme19.m ∧ = (meetβ€˜πΎ)
cdleme19.a 𝐴 = (Atomsβ€˜πΎ)
cdleme19.h 𝐻 = (LHypβ€˜πΎ)
cdleme19.u π‘ˆ = ((𝑃 ∨ 𝑄) ∧ π‘Š)
cdleme19.f 𝐹 = ((𝑆 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ π‘Š)))
cdleme19.g 𝐺 = ((𝑇 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑇) ∧ π‘Š)))
cdleme19.d 𝐷 = ((𝑅 ∨ 𝑆) ∧ π‘Š)
cdleme19.y π‘Œ = ((𝑅 ∨ 𝑇) ∧ π‘Š)
cdleme20.v 𝑉 = ((𝑆 ∨ 𝑇) ∧ π‘Š)
Assertion
Ref Expression
cdleme20l ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ 𝐷)))

Proof of Theorem cdleme20l
StepHypRef Expression
1 cdleme19.l . . . 4 ≀ = (leβ€˜πΎ)
2 cdleme19.j . . . 4 ∨ = (joinβ€˜πΎ)
3 cdleme19.m . . . 4 ∧ = (meetβ€˜πΎ)
4 cdleme19.a . . . 4 𝐴 = (Atomsβ€˜πΎ)
5 cdleme19.h . . . 4 𝐻 = (LHypβ€˜πΎ)
6 cdleme19.u . . . 4 π‘ˆ = ((𝑃 ∨ 𝑄) ∧ π‘Š)
7 cdleme19.f . . . 4 𝐹 = ((𝑆 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ π‘Š)))
8 cdleme19.g . . . 4 𝐺 = ((𝑇 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑇) ∧ π‘Š)))
9 cdleme19.d . . . 4 𝐷 = ((𝑅 ∨ 𝑆) ∧ π‘Š)
10 cdleme19.y . . . 4 π‘Œ = ((𝑅 ∨ 𝑇) ∧ π‘Š)
11 cdleme20.v . . . 4 𝑉 = ((𝑆 ∨ 𝑇) ∧ π‘Š)
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11cdleme20i 39846 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) ≀ (𝑃 ∨ 𝑄))
13 simp11l 1281 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝐾 ∈ HL)
14 simp11 1200 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
15 simp12 1201 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š))
16 simp13 1202 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š))
17 simp21l 1287 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝑅 ∈ 𝐴)
18 simp22l 1289 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝑆 ∈ 𝐴)
19 simp22r 1290 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ Β¬ 𝑆 ≀ π‘Š)
20 simp31l 1293 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝑃 β‰  𝑄)
21 simp321 1320 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄))
22 simp323 1322 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝑅 ≀ (𝑃 ∨ 𝑄))
231, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11cdleme20l1 39849 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄))) β†’ (𝐹 ∨ 𝐷) ∈ (LLinesβ€˜πΎ))
2414, 15, 16, 17, 18, 19, 20, 21, 22, 23syl333anc 1399 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝐹 ∨ 𝐷) ∈ (LLinesβ€˜πΎ))
25 simp23l 1291 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝑇 ∈ 𝐴)
26 simp23r 1292 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ Β¬ 𝑇 ≀ π‘Š)
27 simp322 1321 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄))
28 eqid 2725 . . . . . 6 ((𝑇 ∨ 𝑆) ∧ π‘Š) = ((𝑇 ∨ 𝑆) ∧ π‘Š)
291, 2, 3, 4, 5, 6, 8, 7, 10, 9, 28cdleme20l1 39849 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄))) β†’ (𝐺 ∨ π‘Œ) ∈ (LLinesβ€˜πΎ))
3014, 15, 16, 17, 25, 26, 20, 27, 22, 29syl333anc 1399 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝐺 ∨ π‘Œ) ∈ (LLinesβ€˜πΎ))
31 simp12l 1283 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝑃 ∈ 𝐴)
32 simp13l 1285 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝑄 ∈ 𝐴)
33 eqid 2725 . . . . . 6 (LLinesβ€˜πΎ) = (LLinesβ€˜πΎ)
342, 4, 33llni2 39041 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 β‰  𝑄) β†’ (𝑃 ∨ 𝑄) ∈ (LLinesβ€˜πΎ))
3513, 31, 32, 20, 34syl31anc 1370 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝑃 ∨ 𝑄) ∈ (LLinesβ€˜πΎ))
361, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11cdleme20l2 39850 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) ∈ 𝐴)
37 simp22 1204 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š))
38 simp21 1203 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š))
391, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11cdleme20k 39848 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ((𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š)) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄))) β†’ (𝐹 ∨ 𝐷) β‰  (𝑃 ∨ 𝑄))
4014, 31, 32, 37, 38, 21, 22, 39syl322anc 1395 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝐹 ∨ 𝐷) β‰  (𝑃 ∨ 𝑄))
411, 2, 3, 4, 33llnexchb2 39398 . . . 4 ((𝐾 ∈ HL ∧ ((𝐹 ∨ 𝐷) ∈ (LLinesβ€˜πΎ) ∧ (𝐺 ∨ π‘Œ) ∈ (LLinesβ€˜πΎ) ∧ (𝑃 ∨ 𝑄) ∈ (LLinesβ€˜πΎ)) ∧ (((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) ∈ 𝐴 ∧ (𝐹 ∨ 𝐷) β‰  (𝑃 ∨ 𝑄))) β†’ (((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) ≀ (𝑃 ∨ 𝑄) ↔ ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) = ((𝐹 ∨ 𝐷) ∧ (𝑃 ∨ 𝑄))))
4213, 24, 30, 35, 36, 40, 41syl132anc 1385 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) ≀ (𝑃 ∨ 𝑄) ↔ ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) = ((𝐹 ∨ 𝐷) ∧ (𝑃 ∨ 𝑄))))
4312, 42mpbid 231 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) = ((𝐹 ∨ 𝐷) ∧ (𝑃 ∨ 𝑄)))
4413hllatd 38892 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝐾 ∈ Lat)
45 eqid 2725 . . . . 5 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
4645, 2, 4hlatjcl 38895 . . . 4 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
4713, 31, 32, 46syl3anc 1368 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
48 simp11r 1282 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ π‘Š ∈ 𝐻)
491, 2, 3, 4, 5, 6, 7, 45cdleme1b 39755 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝐹 ∈ (Baseβ€˜πΎ))
5013, 48, 31, 32, 18, 49syl23anc 1374 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝐹 ∈ (Baseβ€˜πΎ))
511, 2, 3, 4, 5, 9, 45cdlemedb 39826 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) β†’ 𝐷 ∈ (Baseβ€˜πΎ))
5213, 48, 17, 18, 51syl22anc 837 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ 𝐷 ∈ (Baseβ€˜πΎ))
5345, 2latjcl 18430 . . . 4 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Baseβ€˜πΎ) ∧ 𝐷 ∈ (Baseβ€˜πΎ)) β†’ (𝐹 ∨ 𝐷) ∈ (Baseβ€˜πΎ))
5444, 50, 52, 53syl3anc 1368 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ (𝐹 ∨ 𝐷) ∈ (Baseβ€˜πΎ))
5545, 3latmcom 18454 . . 3 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ (𝐹 ∨ 𝐷) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ 𝐷)) = ((𝐹 ∨ 𝐷) ∧ (𝑃 ∨ 𝑄)))
5644, 47, 54, 55syl3anc 1368 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ 𝐷)) = ((𝐹 ∨ 𝐷) ∧ (𝑃 ∨ 𝑄)))
5743, 56eqtr4d 2768 1 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ ((𝑅 ∈ 𝐴 ∧ Β¬ 𝑅 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ Β¬ 𝑆 ≀ π‘Š) ∧ (𝑇 ∈ 𝐴 ∧ Β¬ 𝑇 ≀ π‘Š)) ∧ ((𝑃 β‰  𝑄 ∧ 𝑆 β‰  𝑇) ∧ (Β¬ 𝑆 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ (𝑃 ∨ 𝑄) ∧ 𝑅 ≀ (𝑃 ∨ 𝑄)) ∧ (Β¬ 𝑅 ≀ (𝑆 ∨ 𝑇) ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇)))) β†’ ((𝐹 ∨ 𝐷) ∧ (𝐺 ∨ π‘Œ)) = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2930   class class class wbr 5143  β€˜cfv 6543  (class class class)co 7416  Basecbs 17179  lecple 17239  joincjn 18302  meetcmee 18303  Latclat 18422  Atomscatm 38791  HLchlt 38878  LLinesclln 39020  LHypclh 39513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7991  df-2nd 7992  df-proset 18286  df-poset 18304  df-plt 18321  df-lub 18337  df-glb 18338  df-join 18339  df-meet 18340  df-p0 18416  df-p1 18417  df-lat 18423  df-clat 18490  df-oposet 38704  df-ol 38706  df-oml 38707  df-covers 38794  df-ats 38795  df-atl 38826  df-cvlat 38850  df-hlat 38879  df-llines 39027  df-lplanes 39028  df-lvols 39029  df-lines 39030  df-psubsp 39032  df-pmap 39033  df-padd 39325  df-lhyp 39517
This theorem is referenced by:  cdleme20m  39852
  Copyright terms: Public domain W3C validator