dalem45 - Mathbox for Norm Megill

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

Theorem dalem45 39704

Description: Lemma for dath 39723. Dummy center of perspectivity 𝑐 is not on the line 𝐺𝐻. (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
dalem45	⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐺 ∨ 𝐻))

**Proof of Theorem dalem45**
Step	Hyp	Ref	Expression
1		dalem.ph	. . . 4 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
2	1	dalemkelat 39611	. . 3 ⊢ (𝜑 → 𝐾 ∈ Lat)
3	2	3ad2ant1 1133	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ Lat)
4		dalem.ps	. . . 4 ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))
5		dalem.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
6	4, 5	dalemcceb 39676	. . 3 ⊢ (𝜓 → 𝑐 ∈ (Base‘𝐾))
7	6	3ad2ant3 1135	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ∈ (Base‘𝐾))
8	1	dalemkehl 39610	. . . 4 ⊢ (𝜑 → 𝐾 ∈ HL)
9	8	3ad2ant1 1133	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ HL)
10		dalem.l	. . . 4 ⊢ ≤ = (le‘𝐾)
11		dalem.j	. . . 4 ⊢ ∨ = (join‘𝐾)
12		dalem44.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
13		dalem44.o	. . . 4 ⊢ 𝑂 = (LPlanes‘𝐾)
14		dalem44.y	. . . 4 ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
15		dalem44.z	. . . 4 ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)
16		dalem44.g	. . . 4 ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))
17	1, 10, 11, 5, 4, 12, 13, 14, 15, 16	dalem23 39683	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ∈ 𝐴)
18		dalem44.h	. . . 4 ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))
19	1, 10, 11, 5, 4, 12, 13, 14, 15, 18	dalem29 39688	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐻 ∈ 𝐴)
20		eqid 2729	. . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾)
21	20, 11, 5	hlatjcl 39353	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴) → (𝐺 ∨ 𝐻) ∈ (Base‘𝐾))
22	9, 17, 19, 21	syl3anc 1373	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝐺 ∨ 𝐻) ∈ (Base‘𝐾))
23		dalem44.i	. . . 4 ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))
24	1, 10, 11, 5, 4, 12, 13, 14, 15, 23	dalem34 39693	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐼 ∈ 𝐴)
25	20, 5	atbase 39275	. . 3 ⊢ (𝐼 ∈ 𝐴 → 𝐼 ∈ (Base‘𝐾))
26	24, 25	syl 17	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐼 ∈ (Base‘𝐾))
27	1, 10, 11, 5, 4, 12, 13, 14, 15, 16, 18, 23	dalem44 39703	. 2 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ ((𝐺 ∨ 𝐻) ∨ 𝐼))
28	20, 10, 11	latnlej2l 18401	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑐 ∈ (Base‘𝐾) ∧ (𝐺 ∨ 𝐻) ∈ (Base‘𝐾) ∧ 𝐼 ∈ (Base‘𝐾)) ∧ ¬ 𝑐 ≤ ((𝐺 ∨ 𝐻) ∨ 𝐼)) → ¬ 𝑐 ≤ (𝐺 ∨ 𝐻))
29	3, 7, 22, 26, 27, 28	syl131anc 1385	1 ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐺 ∨ 𝐻))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 class class class wbr 5102 ‘cfv 6499 (class class class)co 7369 Basecbs 17155 lecple 17203 joincjn 18252 meetcmee 18253 Latclat 18372 Atomscatm 39249 HLchlt 39336 LPlanesclpl 39479

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-proset 18235 df-poset 18254 df-plt 18269 df-lub 18285 df-glb 18286 df-join 18287 df-meet 18288 df-p0 18364 df-lat 18373 df-clat 18440 df-oposet 39162 df-ol 39164 df-oml 39165 df-covers 39252 df-ats 39253 df-atl 39284 df-cvlat 39308 df-hlat 39337 df-llines 39485 df-lplanes 39486 df-lvols 39487

This theorem is referenced by: dalem46 39705 dalem51 39710 dalem52 39711

W3C validator