dalem17

Description: Lemma for dath . When planes Y and Z are equal, the center of perspectivity C is in Y . (Contributed by NM, 1-Aug-2012)

	Ref	Expression
Hypotheses	dalema.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
	dalemc.l	⊢ ≤ = ( le ‘ 𝐾 )
	dalemc.j	⊢ ∨ = ( join ‘ 𝐾 )
	dalemc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dalem17.o	⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
	dalem17.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
	dalem17.z	⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
Assertion	dalem17	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝐶 ≤ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		dalema.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
2		dalemc.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dalemc.j	⊢ ∨ = ( join ‘ 𝐾 )
4		dalemc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dalem17.o	⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
6		dalem17.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
7		dalem17.z	⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
8	1	dalemclrju	⊢ ( 𝜑 → 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) )
10	1	dalemkelat	⊢ ( 𝜑 → 𝐾 ∈ Lat )
11	1 3 4	dalempjqeb	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
12	1 4	dalemreb	⊢ ( 𝜑 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
13		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14	13 2 3	latlej2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
15	10 11 12 14	syl3anc	⊢ ( 𝜑 → 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
16	15 6	breqtrrdi	⊢ ( 𝜑 → 𝑅 ≤ 𝑌 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑅 ≤ 𝑌 )
18	1 3 4	dalemsjteb	⊢ ( 𝜑 → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
19	1 4	dalemueb	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
20	13 2 3	latlej2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → 𝑈 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
21	10 18 19 20	syl3anc	⊢ ( 𝜑 → 𝑈 ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) )
22	21 7	breqtrrdi	⊢ ( 𝜑 → 𝑈 ≤ 𝑍 )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑈 ≤ 𝑍 )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑌 = 𝑍 )
25	23 24	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑈 ≤ 𝑌 )
26	1 5	dalemyeb	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
27	13 2 3	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ≤ 𝑌 ∧ 𝑈 ≤ 𝑌 ) ↔ ( 𝑅 ∨ 𝑈 ) ≤ 𝑌 ) )
28	10 12 19 26 27	syl13anc	⊢ ( 𝜑 → ( ( 𝑅 ≤ 𝑌 ∧ 𝑈 ≤ 𝑌 ) ↔ ( 𝑅 ∨ 𝑈 ) ≤ 𝑌 ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( ( 𝑅 ≤ 𝑌 ∧ 𝑈 ≤ 𝑌 ) ↔ ( 𝑅 ∨ 𝑈 ) ≤ 𝑌 ) )
30	17 25 29	mpbi2and	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( 𝑅 ∨ 𝑈 ) ≤ 𝑌 )
31	1 4	dalemceb	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐾 ) )
32	1	dalemkehl	⊢ ( 𝜑 → 𝐾 ∈ HL )
33	1	dalemrea	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
34	1	dalemuea	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
35	13 3 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
36	32 33 34 35	syl3anc	⊢ ( 𝜑 → ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
37	13 2	lattr	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ 𝑈 ) ≤ 𝑌 ) → 𝐶 ≤ 𝑌 ) )
38	10 31 36 26 37	syl13anc	⊢ ( 𝜑 → ( ( 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ 𝑈 ) ≤ 𝑌 ) → 𝐶 ≤ 𝑌 ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( ( 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ 𝑈 ) ≤ 𝑌 ) → 𝐶 ≤ 𝑌 ) )
40	9 30 39	mp2and	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝐶 ≤ 𝑌 )

Metamath Proof Explorer

Theorem dalem17

Proof