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 )