Theorem atl0cl

Description: An atomic lattice has a zero element. We can use this in place of op0cl for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atl0cl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	atl0cl.z	⊢ 0 = ( 0. ‘ 𝐾 )
Assertion	atl0cl	⊢ ( 𝐾 ∈ AtLat → 0 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		atl0cl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		atl0cl.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
4	1 3 2	p0val	⊢ ( 𝐾 ∈ AtLat → 0 = ( ( glb ‘ 𝐾 ) ‘ 𝐵 ) )
5		id	⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ AtLat )
6		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
7	1 6 3	atl0dm	⊢ ( 𝐾 ∈ AtLat → 𝐵 ∈ dom ( glb ‘ 𝐾 ) )
8	1 3 5 7	glbcl	⊢ ( 𝐾 ∈ AtLat → ( ( glb ‘ 𝐾 ) ‘ 𝐵 ) ∈ 𝐵 )
9	4 8	eqeltrd	⊢ ( 𝐾 ∈ AtLat → 0 ∈ 𝐵 )