Theorem dalem21

Description: Lemma for dath . Show that lines c d and P S intersect at an atom. (Contributed by NM, 2-Aug-2012)

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

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		dalem21.m	⊢ ∧ = ( meet ‘ 𝐾 )
7		dalem21.o	⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
8		dalem21.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
9		dalem21.z	⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
10	1	dalemkehl	⊢ ( 𝜑 → 𝐾 ∈ HL )
11	10	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐾 ∈ HL )
12	1 2 3 4 5	dalemcjden	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑑 ) ∈ ( LLines ‘ 𝐾 ) )
13	12	3adant2	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑑 ) ∈ ( LLines ‘ 𝐾 ) )
14	1 2 3 4 7 8	dalempjsen	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
15	14	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
16	1 2 3 4 7 8	dalemply	⊢ ( 𝜑 → 𝑃 ≤ 𝑌 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑃 ≤ 𝑌 )
18	1 2 3 4 9	dalemsly	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑆 ≤ 𝑌 )
19	1	dalemkelat	⊢ ( 𝜑 → 𝐾 ∈ Lat )
20	1 4	dalempeb	⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
21	1 4	dalemseb	⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
22	1 7	dalemyeb	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
23		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24	23 2 3	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ 𝑌 ∧ 𝑆 ≤ 𝑌 ) ↔ ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ) )
25	19 20 21 22 24	syl13anc	⊢ ( 𝜑 → ( ( 𝑃 ≤ 𝑌 ∧ 𝑆 ≤ 𝑌 ) ↔ ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( ( 𝑃 ≤ 𝑌 ∧ 𝑆 ≤ 𝑌 ) ↔ ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ) )
27	17 18 26	mpbi2and	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 )
28	27	3adant3	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 )
29	5	dalem-ccly	⊢ ( 𝜓 → ¬ 𝑐 ≤ 𝑌 )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ 𝑐 ≤ 𝑌 )
31	19	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 ∈ Lat )
32	5 4	dalemcceb	⊢ ( 𝜓 → 𝑐 ∈ ( Base ‘ 𝐾 ) )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑐 ∈ ( Base ‘ 𝐾 ) )
34	5	dalemddea	⊢ ( 𝜓 → 𝑑 ∈ 𝐴 )
35	23 4	atbase	⊢ ( 𝑑 ∈ 𝐴 → 𝑑 ∈ ( Base ‘ 𝐾 ) )
36	34 35	syl	⊢ ( 𝜓 → 𝑑 ∈ ( Base ‘ 𝐾 ) )
37	36	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑑 ∈ ( Base ‘ 𝐾 ) )
38	23 2 3	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑐 ∈ ( Base ‘ 𝐾 ) ∧ 𝑑 ∈ ( Base ‘ 𝐾 ) ) → 𝑐 ≤ ( 𝑐 ∨ 𝑑 ) )
39	31 33 37 38	syl3anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑐 ≤ ( 𝑐 ∨ 𝑑 ) )
40		eqid	⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
41	23 40	llnbase	⊢ ( ( 𝑐 ∨ 𝑑 ) ∈ ( LLines ‘ 𝐾 ) → ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) )
42	12 41	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) )
43	22	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
44	23 2	lattr	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑐 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑐 ≤ ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 ) → 𝑐 ≤ 𝑌 ) )
45	31 33 42 43 44	syl13anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ≤ ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 ) → 𝑐 ≤ 𝑌 ) )
46	39 45	mpand	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 → 𝑐 ≤ 𝑌 ) )
47	30 46	mtod	⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 )
48	47	3adant2	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ¬ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 )
49		nbrne2	⊢ ( ( ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ∧ ¬ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 ) → ( 𝑃 ∨ 𝑆 ) ≠ ( 𝑐 ∨ 𝑑 ) )
50	28 48 49	syl2anc	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑆 ) ≠ ( 𝑐 ∨ 𝑑 ) )
51	50	necomd	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑑 ) ≠ ( 𝑃 ∨ 𝑆 ) )
52		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
53	10 52	syl	⊢ ( 𝜑 → 𝐾 ∈ AtLat )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 ∈ AtLat )
55	1	dalempea	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
56	1	dalemsea	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
57	23 3 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
58	10 55 56 57	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
59	58	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
60	23 6	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
61	31 42 59 60	syl3anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
62	1 2 3 4 7 8	dalemcea	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
63	62	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ 𝐴 )
64	5	dalemclccjdd	⊢ ( 𝜓 → 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) )
65	64	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) )
66	1	dalemclpjs	⊢ ( 𝜑 → 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) )
67	66	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) )
68	1 4	dalemceb	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐾 ) )
69	68	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ ( Base ‘ 𝐾 ) )
70	23 2 6	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ∧ 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) ↔ 𝐶 ≤ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) )
71	31 69 42 59 70	syl13anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ∧ 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) ↔ 𝐶 ≤ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) )
72	65 67 71	mpbi2and	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ≤ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) )
73		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
74	23 2 73 4	atlen0	⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ 𝐴 ) ∧ 𝐶 ≤ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≠ ( 0. ‘ 𝐾 ) )
75	54 61 63 72 74	syl31anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≠ ( 0. ‘ 𝐾 ) )
76	75	3adant2	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≠ ( 0. ‘ 𝐾 ) )
77	6 73 4 40	2llnmat	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑐 ∨ 𝑑 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) ∧ ( ( 𝑐 ∨ 𝑑 ) ≠ ( 𝑃 ∨ 𝑆 ) ∧ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≠ ( 0. ‘ 𝐾 ) ) ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ 𝐴 )
78	11 13 15 51 76 77	syl32anc	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ 𝐴 )