dalem27

Description: Lemma for dath . Show that the line G P intersects the dummy center of perspectivity c . (Contributed by NM, 8-Aug-2012)

	Ref	Expression
Hypotheses	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	dalem27	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑐 ≤ ( 𝐺 ∨ 𝑃 ) )

Proof

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

Metamath Proof Explorer

Theorem dalem27

Proof