Metamath Proof Explorer

Theorem 2llnm4

Description: Two lattice lines that majorize the same atom always meet. (Contributed by NM, 20-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 2llnm4.l ⊢ ≤ = ( le ‘ 𝐾 )
2 2llnm4.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 2llnm4.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 2llnm4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 2llnm4.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
6 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
7 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝐾 ∈ AtLat )
8 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9 8 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝐾 ∈ Lat )
10 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝑋 ∈ 𝑁 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 5 llnbase ⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
13 10 12 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
14 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝑌 ∈ 𝑁 )
15 11 5 llnbase ⊢ ( 𝑌 ∈ 𝑁 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
16 14 15 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
17 11 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
18 9 13 16 17 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
19 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝑃 ∈ 𝐴 )
20 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) )
21 11 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
22 19 21 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
23 11 1 2 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ↔ 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ) )
24 9 22 13 16 23 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ↔ 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ) )
25 20 24 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) )
26 11 1 3 4 atlen0 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )
27 7 18 19 25 26 syl31anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )