dalem5

Description: Lemma for dath . Atom U (in plane Z = S T U ) belongs to the 3-dimensional volume formed by Y and C . (Contributed by NM, 21-Jul-2012)

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

Proof

Step	Hyp	Ref	Expression
1		dalema.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
2		dalemc.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dalemc.j	⊢ ∨ = ( join ‘ 𝐾 )
4		dalemc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dalem5.o	⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
6		dalem5.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
7		dalem5.w	⊢ 𝑊 = ( 𝑌 ∨ 𝐶 )
8		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9	1	dalemkelat	⊢ ( 𝜑 → 𝐾 ∈ Lat )
10	1 4	dalemueb	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
11	1	dalemkehl	⊢ ( 𝜑 → 𝐾 ∈ HL )
12	1	dalemrea	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
13	1 2 3 4 5 6	dalemcea	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
14	8 3 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑅 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
15	11 12 13 14	syl3anc	⊢ ( 𝜑 → ( 𝑅 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
16	1 5	dalemyeb	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
17	1 4	dalemceb	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐾 ) )
18	8 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑌 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
19	9 16 17 18	syl3anc	⊢ ( 𝜑 → ( 𝑌 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
20	7 19	eqeltrid	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21	1	dalemclrju	⊢ ( 𝜑 → 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) )
22	1	dalemuea	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
23	1	dalempea	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
24		simp313	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) → ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) )
25	1 24	sylbi	⊢ ( 𝜑 → ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) )
26	2 3 4	atnlej1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) → 𝐶 ≠ 𝑅 )
27	11 13 12 23 25 26	syl131anc	⊢ ( 𝜑 → 𝐶 ≠ 𝑅 )
28	2 3 4	hlatexch1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝐶 ≠ 𝑅 ) → ( 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) → 𝑈 ≤ ( 𝑅 ∨ 𝐶 ) ) )
29	11 13 22 12 27 28	syl131anc	⊢ ( 𝜑 → ( 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) → 𝑈 ≤ ( 𝑅 ∨ 𝐶 ) ) )
30	21 29	mpd	⊢ ( 𝜑 → 𝑈 ≤ ( 𝑅 ∨ 𝐶 ) )
31	1 3 4	dalempjqeb	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
32	1 4	dalemreb	⊢ ( 𝜑 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
33	8 2 3	latlej2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
34	9 31 32 33	syl3anc	⊢ ( 𝜑 → 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
35	34 6	breqtrrdi	⊢ ( 𝜑 → 𝑅 ≤ 𝑌 )
36	8 2 3	latjlej1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ≤ 𝑌 → ( 𝑅 ∨ 𝐶 ) ≤ ( 𝑌 ∨ 𝐶 ) ) )
37	9 32 16 17 36	syl13anc	⊢ ( 𝜑 → ( 𝑅 ≤ 𝑌 → ( 𝑅 ∨ 𝐶 ) ≤ ( 𝑌 ∨ 𝐶 ) ) )
38	35 37	mpd	⊢ ( 𝜑 → ( 𝑅 ∨ 𝐶 ) ≤ ( 𝑌 ∨ 𝐶 ) )
39	38 7	breqtrrdi	⊢ ( 𝜑 → ( 𝑅 ∨ 𝐶 ) ≤ 𝑊 )
40	8 2 9 10 15 20 30 39	lattrd	⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )

Metamath Proof Explorer

Theorem dalem5

Proof