Theorem 2llnm3N

Description: Two lattice lines in a lattice plane always meet. (Contributed by NM, 5-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2llnm3.l	⊢ ≤ = ( le ‘ 𝐾 )
	2llnm3.m	⊢ ∧ = ( meet ‘ 𝐾 )
	2llnm3.z	⊢ 0 = ( 0. ‘ 𝐾 )
	2llnm3.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
	2llnm3.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion	2llnm3N	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		2llnm3.l	⊢ ≤ = ( le ‘ 𝐾 )
2		2llnm3.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		2llnm3.z	⊢ 0 = ( 0. ‘ 𝐾 )
4		2llnm3.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
5		2llnm3.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6		oveq1	⊢ ( 𝑋 = 𝑌 → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑌 ) )
7	6	neeq1d	⊢ ( 𝑋 = 𝑌 → ( ( 𝑋 ∧ 𝑌 ) ≠ 0 ↔ ( 𝑌 ∧ 𝑌 ) ≠ 0 ) )
8		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝐾 ∈ HL )
9		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
10	8 9	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝐾 ∈ AtLat )
11		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) )
12		simpl3l	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≤ 𝑊 )
13		simpl3r	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ≤ 𝑊 )
14		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
15		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
16	1 2 15 4 5	2llnm2N	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Atoms ‘ 𝐾 ) )
17	8 11 12 13 14 16	syl113anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Atoms ‘ 𝐾 ) )
18	3 15	atn0	⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )
19	10 17 18	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )
20		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
21	20	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
22		simp22	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ∈ 𝑁 )
23		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24	23 4	llnbase	⊢ ( 𝑌 ∈ 𝑁 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
25	22 24	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
26	23 2	latmidm	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑌 ∧ 𝑌 ) = 𝑌 )
27	21 25 26	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑌 ∧ 𝑌 ) = 𝑌 )
28		simp1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
29	3 4	llnn0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑁 ) → 𝑌 ≠ 0 )
30	28 22 29	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ≠ 0 )
31	27 30	eqnetrd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑌 ∧ 𝑌 ) ≠ 0 )
32	7 19 31	pm2.61ne	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )