This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )