dalem27 - Mathbox for Norm Megill

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

Theorem dalem27 40865

Description: Lemma for dath 40902. Show that the line 𝐺𝑃 intersects the dummy center of perspectivity 𝑐. (Contributed by NM, 8-Aug-2012.)

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

**Assertion**
Ref	Expression
dalem27	⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐺 ∨ 𝑃))

**Proof of Theorem dalem27**
Step	Hyp	Ref	Expression
1		dalem23.g	. . 3 ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))
2		dalem.ph	. . . . . 6 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
3	2	dalemkelat 40790	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Lat)
4	3	3ad2ant1 1151	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ Lat)
5	2	dalemkehl 40789	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ HL)
6	5	3ad2ant1 1151	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ HL)
7		dalem.ps	. . . . . . 7 ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))
8	7	dalemccea 40849	. . . . . 6 ⊢ (𝜓 → 𝑐 ∈ 𝐴)
9	8	3ad2ant3 1153	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ∈ 𝐴)
10	2	dalempea 40792	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
11	10	3ad2ant1 1151	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑃 ∈ 𝐴)
12		eqid 2760	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
13		dalem.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
14		dalem.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
15	12, 13, 14	hlatjcl 40533	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑐 ∨ 𝑃) ∈ (Base‘𝐾))
16	6, 9, 11, 15	syl3anc 1398	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝑐 ∨ 𝑃) ∈ (Base‘𝐾))
17	7	dalemddea 40850	. . . . . 6 ⊢ (𝜓 → 𝑑 ∈ 𝐴)
18	17	3ad2ant3 1153	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑑 ∈ 𝐴)
19	2	dalemsea 40795	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ 𝐴)
20	19	3ad2ant1 1151	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑆 ∈ 𝐴)
21	12, 13, 14	hlatjcl 40533	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑑 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑑 ∨ 𝑆) ∈ (Base‘𝐾))
22	6, 18, 20, 21	syl3anc 1398	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝑑 ∨ 𝑆) ∈ (Base‘𝐾))
23		dalem.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
24		dalem23.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
25	12, 23, 24	latmle1 18647	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑐 ∨ 𝑃) ∈ (Base‘𝐾) ∧ (𝑑 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) ≤ (𝑐 ∨ 𝑃))
26	4, 16, 22, 25	syl3anc 1398	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) ≤ (𝑐 ∨ 𝑃))
27	1, 26	eqbrtrid 5139	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ≤ (𝑐 ∨ 𝑃))
28		dalem23.o	. . . 4 ⊢ 𝑂 = (LPlanes‘𝐾)
29		dalem23.y	. . . 4 ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
30		dalem23.z	. . . 4 ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)
31	2, 23, 13, 14, 7, 24, 28, 29, 30, 1	dalem23 40862	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ∈ 𝐴)
32	2, 23, 13, 14, 28, 29	dalemply 40820	. . . . 5 ⊢ (𝜑 → 𝑃 ≤ 𝑌)
33	32	3ad2ant1 1151	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑃 ≤ 𝑌)
34	2, 23, 13, 14, 7, 24, 28, 29, 30, 1	dalem24 40863	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐺 ≤ 𝑌)
35		nbrne2 5124	. . . . 5 ⊢ ((𝑃 ≤ 𝑌 ∧ ¬ 𝐺 ≤ 𝑌) → 𝑃 ≠ 𝐺)
36	35	necomd 3010	. . . 4 ⊢ ((𝑃 ≤ 𝑌 ∧ ¬ 𝐺 ≤ 𝑌) → 𝐺 ≠ 𝑃)
37	33, 34, 36	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ≠ 𝑃)
38	23, 13, 14	hlatexch2 40562	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝐺 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝐺 ≠ 𝑃) → (𝐺 ≤ (𝑐 ∨ 𝑃) → 𝑐 ≤ (𝐺 ∨ 𝑃)))
39	6, 31, 9, 11, 37, 38	syl131anc 1410	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝐺 ≤ (𝑐 ∨ 𝑃) → 𝑐 ≤ (𝐺 ∨ 𝑃)))
40	27, 39	mpd 16	1 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐺 ∨ 𝑃))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 ‘cfv 6543 (class class class)co 7424 Basecbs 17396 lecple 17444 joincjn 18494 meetcmee 18495 Latclat 18614 Atomscatm 40429 HLchlt 40516 LPlanesclpl 40658

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-proset 18477 df-poset 18496 df-plt 18511 df-lub 18527 df-glb 18528 df-join 18529 df-meet 18530 df-p0 18606 df-lat 18615 df-clat 18682 df-oposet 40342 df-ol 40344 df-oml 40345 df-covers 40432 df-ats 40433 df-atl 40464 df-cvlat 40488 df-hlat 40517 df-llines 40664 df-lplanes 40665

This theorem is used by: dalem28 40866 dalem32 40870 dalem51 40889 dalem52 40890

W3C validator