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

Metamath Proof Explorer

Theorem 2llnmeqat

Description: An atom equals the intersection of two majorizing lines. (Contributed by NM, 3-Apr-2013)

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

Proof

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