Metamath Proof Explorer

Theorem meetat

Description: The meet of any element with an atom is either the atom or zero. (Contributed by NM, 28-Aug-2012)

Ref Expression
Hypotheses m.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
m.m ⊢ ∧ = ( meet ‘ 𝐾 )
m.z ⊢ 0 = ( 0. ‘ 𝐾 )
m.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion meetat ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 𝑃 ∨ ( 𝑋 ∧ 𝑃 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 m.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 m.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 m.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 m.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 ollat ⊢ ( 𝐾 ∈ OL → 𝐾 ∈ Lat )
6 5 3ad2ant1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ Lat )
7 simp2 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
8 simp3 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
9 1 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
10 8 9 syl ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
11 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12 1 11 2 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑃 ) ( le ‘ 𝐾 ) 𝑃 )
13 6 7 10 12 syl3anc ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∧ 𝑃 ) ( le ‘ 𝐾 ) 𝑃 )
14 olop ⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP )
15 14 3ad2ant1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ OP )
16 1 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑃 ) ∈ 𝐵 )
17 6 7 10 16 syl3anc ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∧ 𝑃 ) ∈ 𝐵 )
18 1 11 3 4 leatb ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∧ 𝑃 ) ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) ( le ‘ 𝐾 ) 𝑃 ↔ ( ( 𝑋 ∧ 𝑃 ) = 𝑃 ∨ ( 𝑋 ∧ 𝑃 ) = 0 ) ) )
19 15 17 8 18 syl3anc ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) ( le ‘ 𝐾 ) 𝑃 ↔ ( ( 𝑋 ∧ 𝑃 ) = 𝑃 ∨ ( 𝑋 ∧ 𝑃 ) = 0 ) ) )
20 13 19 mpbid ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 𝑃 ∨ ( 𝑋 ∧ 𝑃 ) = 0 ) )