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 ) )