Theorem llnmlplnN

Description: The intersection of a line with a plane not containing it is an atom. (Contributed by NM, 29-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	llnmlpln.l	⊢ ≤ = ( le ‘ 𝐾 )
	llnmlpln.m	⊢ ∧ = ( meet ‘ 𝐾 )
	llnmlpln.z	⊢ 0 = ( 0. ‘ 𝐾 )
	llnmlpln.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	llnmlpln.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
	llnmlpln.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion	llnmlplnN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		llnmlpln.l	⊢ ≤ = ( le ‘ 𝐾 )
2		llnmlpln.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		llnmlpln.z	⊢ 0 = ( 0. ‘ 𝐾 )
4		llnmlpln.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		llnmlpln.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
6		llnmlpln.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
7		simprl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ¬ 𝑋 ≤ 𝑌 )
8		simp11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝐾 ∈ HL )
9	8	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝐾 ∈ Lat )
10		simp12	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑋 ∈ 𝑁 )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 5	llnbase	⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
13	10 12	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
14		simp13	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑌 ∈ 𝑃 )
15	11 6	lplnbase	⊢ ( 𝑌 ∈ 𝑃 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
16	14 15	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
17	11 2	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
18	9 13 16 17	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
19		simp2r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )
20		simp3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )
21	11 1 3 4 5	llnle	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑋 ∧ 𝑌 ) ≠ 0 ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ) → ∃ 𝑢 ∈ 𝑁 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) )
22	8 18 19 20 21	syl22anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ∃ 𝑢 ∈ 𝑁 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) )
23	9	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝐾 ∈ Lat )
24	18	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
25	13	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
26	11 1 2	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
27	9 13 16 26	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
28	27	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
29	11 5	llnbase	⊢ ( 𝑢 ∈ 𝑁 → 𝑢 ∈ ( Base ‘ 𝐾 ) )
30	29	ad2antrl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 ∈ ( Base ‘ 𝐾 ) )
31		simprr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) )
32	11 1 23 30 24 25 31 28	lattrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 ≤ 𝑋 )
33		simpl11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝐾 ∈ HL )
34		simprl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 ∈ 𝑁 )
35		simpl12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑋 ∈ 𝑁 )
36	1 5	llncmp	⊢ ( ( 𝐾 ∈ HL ∧ 𝑢 ∈ 𝑁 ∧ 𝑋 ∈ 𝑁 ) → ( 𝑢 ≤ 𝑋 ↔ 𝑢 = 𝑋 ) )
37	33 34 35 36	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → ( 𝑢 ≤ 𝑋 ↔ 𝑢 = 𝑋 ) )
38	32 37	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 = 𝑋 )
39	38 31	eqbrtrrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑋 ≤ ( 𝑋 ∧ 𝑌 ) )
40	11 1 23 24 25 28 39	latasymd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → ( 𝑋 ∧ 𝑌 ) = 𝑋 )
41	22 40	rexlimddv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) = 𝑋 )
42	11 1 2	latleeqm1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
43	9 13 16 42	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
44	41 43	mpbird	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑋 ≤ 𝑌 )
45	44	3expia	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 → 𝑋 ≤ 𝑌 ) )
46	7 45	mt3d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )