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

Metamath Proof Explorer

Theorem meetat2

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

Ref Expression
Hypotheses m.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
m.m ⊢ ∧ = ( meet ‘ 𝐾 )
m.z ⊢ 0 = ( 0. ‘ 𝐾 )
m.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion meetat2 ( ( 𝐾 ∈ 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 1 2 3 4 meetat ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 𝑃 ∨ ( 𝑋 ∧ 𝑃 ) = 0 ) )
6 eleq1a ⊢ ( 𝑃 ∈ 𝐴 → ( ( 𝑋 ∧ 𝑃 ) = 𝑃 → ( 𝑋 ∧ 𝑃 ) ∈ 𝐴 ) )
7 6 3ad2ant3 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 𝑃 → ( 𝑋 ∧ 𝑃 ) ∈ 𝐴 ) )
8 7 orim1d ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( ( 𝑋 ∧ 𝑃 ) = 𝑃 ∨ ( 𝑋 ∧ 𝑃 ) = 0 ) → ( ( 𝑋 ∧ 𝑃 ) ∈ 𝐴 ∨ ( 𝑋 ∧ 𝑃 ) = 0 ) ) )
9 5 8 mpd ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) ∈ 𝐴 ∨ ( 𝑋 ∧ 𝑃 ) = 0 ) )