Theorem dalem23

Description: Lemma for dath . Show that auxiliary atom G is 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	⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
	dalem23.m	⊢ ∧ = ( meet ‘ 𝐾 )
	dalem23.o	⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
	dalem23.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
	dalem23.z	⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
	dalem23.g	⊢ 𝐺 = ( ( 𝑐 ∨ 𝑃 ) ∧ ( 𝑑 ∨ 𝑆 ) )
Assertion	dalem23	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐺 ∈ 𝐴 )

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	dalemkehl	⊢ ( 𝜑 → 𝐾 ∈ HL )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 ∈ HL )
13	5	dalemccea	⊢ ( 𝜓 → 𝑐 ∈ 𝐴 )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑐 ∈ 𝐴 )
15	1	dalempea	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑃 ∈ 𝐴 )
17	5	dalemddea	⊢ ( 𝜓 → 𝑑 ∈ 𝐴 )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑑 ∈ 𝐴 )
19	1	dalemsea	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑆 ∈ 𝐴 )
21	3 4	hlatj4	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑐 ∨ 𝑃 ) ∨ ( 𝑑 ∨ 𝑆 ) ) = ( ( 𝑐 ∨ 𝑑 ) ∨ ( 𝑃 ∨ 𝑆 ) ) )
22	12 14 16 18 20 21	syl122anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑃 ) ∨ ( 𝑑 ∨ 𝑆 ) ) = ( ( 𝑐 ∨ 𝑑 ) ∨ ( 𝑃 ∨ 𝑆 ) ) )
23	22	3adant2	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑃 ) ∨ ( 𝑑 ∨ 𝑆 ) ) = ( ( 𝑐 ∨ 𝑑 ) ∨ ( 𝑃 ∨ 𝑆 ) ) )
24	1 2 3 4 5 7 8 9	dalem22	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∨ ( 𝑃 ∨ 𝑆 ) ) ∈ 𝑂 )
25	23 24	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑃 ) ∨ ( 𝑑 ∨ 𝑆 ) ) ∈ 𝑂 )
26	11	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐾 ∈ HL )
27	1 2 3 4 7 8	dalemply	⊢ ( 𝜑 → 𝑃 ≤ 𝑌 )
28	5	dalem-ccly	⊢ ( 𝜓 → ¬ 𝑐 ≤ 𝑌 )
29		nbrne2	⊢ ( ( 𝑃 ≤ 𝑌 ∧ ¬ 𝑐 ≤ 𝑌 ) → 𝑃 ≠ 𝑐 )
30	27 28 29	syl2an	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑃 ≠ 𝑐 )
31	30	necomd	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑐 ≠ 𝑃 )
32		eqid	⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
33	3 4 32	llni2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑐 ≠ 𝑃 ) → ( 𝑐 ∨ 𝑃 ) ∈ ( LLines ‘ 𝐾 ) )
34	12 14 16 31 33	syl31anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑃 ) ∈ ( LLines ‘ 𝐾 ) )
35	34	3adant2	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑃 ) ∈ ( LLines ‘ 𝐾 ) )
36	17	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑑 ∈ 𝐴 )
37	19	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑆 ∈ 𝐴 )
38	1 2 3 4 9	dalemsly	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑆 ≤ 𝑌 )
39	38	3adant3	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑆 ≤ 𝑌 )
40	5	dalem-ddly	⊢ ( 𝜓 → ¬ 𝑑 ≤ 𝑌 )
41	40	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ¬ 𝑑 ≤ 𝑌 )
42		nbrne2	⊢ ( ( 𝑆 ≤ 𝑌 ∧ ¬ 𝑑 ≤ 𝑌 ) → 𝑆 ≠ 𝑑 )
43	39 41 42	syl2anc	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑆 ≠ 𝑑 )
44	43	necomd	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝑑 ≠ 𝑆 )
45	3 4 32	llni2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑑 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑑 ≠ 𝑆 ) → ( 𝑑 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
46	26 36 37 44 45	syl31anc	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑑 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
47	3 6 4 32 7	2llnmj	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑐 ∨ 𝑃 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑑 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) → ( ( ( 𝑐 ∨ 𝑃 ) ∧ ( 𝑑 ∨ 𝑆 ) ) ∈ 𝐴 ↔ ( ( 𝑐 ∨ 𝑃 ) ∨ ( 𝑑 ∨ 𝑆 ) ) ∈ 𝑂 ) )
48	26 35 46 47	syl3anc	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( ( 𝑐 ∨ 𝑃 ) ∧ ( 𝑑 ∨ 𝑆 ) ) ∈ 𝐴 ↔ ( ( 𝑐 ∨ 𝑃 ) ∨ ( 𝑑 ∨ 𝑆 ) ) ∈ 𝑂 ) )
49	25 48	mpbird	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑃 ) ∧ ( 𝑑 ∨ 𝑆 ) ) ∈ 𝐴 )
50	10 49	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐺 ∈ 𝐴 )