Theorem dalem51 37745

Description: Lemma for dath 37758. Construct the condition 𝜑 with 𝑐, 𝐺𝐻𝐼, and 𝑌 in place of 𝐶, 𝑌, and 𝑍 respectively. This lets us reuse the special case of Desargues's theorem where 𝑌 ≠ 𝑍, to eventually prove the case where 𝑌 = 𝑍. (Contributed by NM, 16-Aug-2012.)

Hypotheses

Ref	Expression
dalem.ph	⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
dalem.l	⊢ ≤ = (le‘𝐾)
dalem.j	⊢ ∨ = (join‘𝐾)
dalem.a	⊢ 𝐴 = (Atoms‘𝐾)
dalem.ps	⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))
dalem44.m	⊢ ∧ = (meet‘𝐾)
dalem44.o	⊢ 𝑂 = (LPlanes‘𝐾)
dalem44.y	⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
dalem44.z	⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)
dalem44.g	⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))
dalem44.h	⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))
dalem44.i	⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))

Assertion

Ref	Expression
dalem51	⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((((𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴) ∧ (𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ∧ 𝐼 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝑐 ≤ (𝐺 ∨ 𝐻) ∧ ¬ 𝑐 ≤ (𝐻 ∨ 𝐼) ∧ ¬ 𝑐 ≤ (𝐼 ∨ 𝐺)) ∧ (¬ 𝑐 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑐 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)) ∧ (𝑐 ≤ (𝐺 ∨ 𝑃) ∧ 𝑐 ≤ (𝐻 ∨ 𝑄) ∧ 𝑐 ≤ (𝐼 ∨ 𝑅)))) ∧ ((𝐺 ∨ 𝐻) ∨ 𝐼) ≠ 𝑌))

Proof of Theorem dalem51

Step	Hyp	Ref	Expression
1		dalem.ph	. . . . . . 7 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
2	1	dalemkehl 37645	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ HL)
3	2	3ad2ant1 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ HL)
4		dalem.ps	. . . . . . 7 ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))
5	4	dalemccea 37705	. . . . . 6 ⊢ (𝜓 → 𝑐 ∈ 𝐴)
6	5	3ad2ant3 1134	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ∈ 𝐴)
7	3, 6	jca 512	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴))
8		dalem.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
9		dalem.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
10		dalem.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
11		dalem44.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
12		dalem44.o	. . . . . 6 ⊢ 𝑂 = (LPlanes‘𝐾)
13		dalem44.y	. . . . . 6 ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
14		dalem44.z	. . . . . 6 ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)
15		dalem44.g	. . . . . 6 ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))
16	1, 8, 9, 10, 4, 11, 12, 13, 14, 15	dalem23 37718	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ∈ 𝐴)
17		dalem44.h	. . . . . 6 ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))
18	1, 8, 9, 10, 4, 11, 12, 13, 14, 17	dalem29 37723	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐻 ∈ 𝐴)
19		dalem44.i	. . . . . 6 ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))
20	1, 8, 9, 10, 4, 11, 12, 13, 14, 19	dalem34 37728	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐼 ∈ 𝐴)
21	16, 18, 20	3jca 1127	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ∧ 𝐼 ∈ 𝐴))
22	1	dalempea 37648	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
23	1	dalemqea 37649	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
24	1	dalemrea 37650	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ 𝐴)
25	22, 23, 24	3jca 1127	. . . . 5 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
26	25	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
27	7, 21, 26	3jca 1127	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴) ∧ (𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ∧ 𝐼 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)))
28	1, 8, 9, 10, 4, 11, 12, 13, 14, 15, 17, 19	dalem42 37736	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂)
29	1	dalemyeo 37654	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑂)
30	29	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑌 ∈ 𝑂)
31	28, 30	jca 512	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂 ∧ 𝑌 ∈ 𝑂))
32	1, 8, 9, 10, 4, 11, 12, 13, 14, 15, 17, 19	dalem45 37739	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐺 ∨ 𝐻))
33	1, 8, 9, 10, 4, 11, 12, 13, 14, 15, 17, 19	dalem46 37740	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐻 ∨ 𝐼))
34	1, 8, 9, 10, 4, 11, 12, 13, 14, 15, 17, 19	dalem47 37741	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐼 ∨ 𝐺))
35	32, 33, 34	3jca 1127	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (¬ 𝑐 ≤ (𝐺 ∨ 𝐻) ∧ ¬ 𝑐 ≤ (𝐻 ∨ 𝐼) ∧ ¬ 𝑐 ≤ (𝐼 ∨ 𝐺)))
36	1, 8, 9, 10, 4, 11, 12, 13, 14, 15, 17, 19	dalem48 37742	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑃 ∨ 𝑄))
37	1, 8, 9, 10, 4, 11, 12, 13, 14, 15, 17, 19	dalem49 37743	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑄 ∨ 𝑅))
38	1, 8, 9, 10, 4, 11, 12, 13, 14, 15, 17, 19	dalem50 37744	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑅 ∨ 𝑃))
39	36, 37, 38	3jca 1127	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (¬ 𝑐 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑐 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)))
40	39	3adant2 1130	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (¬ 𝑐 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑐 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)))
41	1, 8, 9, 10, 4, 11, 12, 13, 14, 15	dalem27 37721	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐺 ∨ 𝑃))
42	1, 8, 9, 10, 4, 11, 12, 13, 14, 17	dalem32 37726	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐻 ∨ 𝑄))
43	1, 8, 9, 10, 4, 11, 12, 13, 14, 19	dalem36 37730	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐼 ∨ 𝑅))
44	41, 42, 43	3jca 1127	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝑐 ≤ (𝐺 ∨ 𝑃) ∧ 𝑐 ≤ (𝐻 ∨ 𝑄) ∧ 𝑐 ≤ (𝐼 ∨ 𝑅)))
45	35, 40, 44	3jca 1127	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((¬ 𝑐 ≤ (𝐺 ∨ 𝐻) ∧ ¬ 𝑐 ≤ (𝐻 ∨ 𝐼) ∧ ¬ 𝑐 ≤ (𝐼 ∨ 𝐺)) ∧ (¬ 𝑐 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑐 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)) ∧ (𝑐 ≤ (𝐺 ∨ 𝑃) ∧ 𝑐 ≤ (𝐻 ∨ 𝑄) ∧ 𝑐 ≤ (𝐼 ∨ 𝑅))))
46	27, 31, 45	3jca 1127	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (((𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴) ∧ (𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ∧ 𝐼 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝑐 ≤ (𝐺 ∨ 𝐻) ∧ ¬ 𝑐 ≤ (𝐻 ∨ 𝐼) ∧ ¬ 𝑐 ≤ (𝐼 ∨ 𝐺)) ∧ (¬ 𝑐 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑐 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)) ∧ (𝑐 ≤ (𝐺 ∨ 𝑃) ∧ 𝑐 ≤ (𝐻 ∨ 𝑄) ∧ 𝑐 ≤ (𝐼 ∨ 𝑅)))))
47	1, 8, 9, 10, 4, 11, 12, 13, 14, 15, 17, 19	dalem43 37737	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∨ 𝐼) ≠ 𝑌)
48	46, 47	jca 512	1 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((((𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴) ∧ (𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ∧ 𝐼 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝑐 ≤ (𝐺 ∨ 𝐻) ∧ ¬ 𝑐 ≤ (𝐻 ∨ 𝐼) ∧ ¬ 𝑐 ≤ (𝐼 ∨ 𝐺)) ∧ (¬ 𝑐 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑐 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)) ∧ (𝑐 ≤ (𝐺 ∨ 𝑃) ∧ 𝑐 ≤ (𝐻 ∨ 𝑄) ∧ 𝑐 ≤ (𝐼 ∨ 𝑅)))) ∧ ((𝐺 ∨ 𝐻) ∨ 𝐼) ≠ 𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943   class class class wbr 5073  ‘cfv 6426  (class class class)co 7267  Basecbs 16922  lecple 16979  joincjn 18039  meetcmee 18040  Atomscatm 37285  HLchlt 37372  LPlanesclpl 37514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5208  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5074  df-opab 5136  df-mpt 5157  df-id 5484  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-f1 6431  df-fo 6432  df-f1o 6433  df-fv 6434  df-riota 7224  df-ov 7270  df-oprab 7271  df-proset 18023  df-poset 18041  df-plt 18058  df-lub 18074  df-glb 18075  df-join 18076  df-meet 18077  df-p0 18153  df-lat 18160  df-clat 18227  df-oposet 37198  df-ol 37200  df-oml 37201  df-covers 37288  df-ats 37289  df-atl 37320  df-cvlat 37344  df-hlat 37373  df-llines 37520  df-lplanes 37521  df-lvols 37522

This theorem is referenced by:  dalem53  37747  dalem54  37748