Theorem atl0le

Description: Orthoposet zero is less than or equal to any element. ( ch0le analog.) (Contributed by NM, 12-Oct-2011)

	Ref	Expression
Hypotheses	atl0le.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	atl0le.l	⊢ ≤ = ( le ‘ 𝐾 )
	atl0le.z	⊢ 0 = ( 0. ‘ 𝐾 )
Assertion	atl0le	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		atl0le.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		atl0le.l	⊢ ≤ = ( le ‘ 𝐾 )
3		atl0le.z	⊢ 0 = ( 0. ‘ 𝐾 )
4		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
5		simpl	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ AtLat )
6		simpr	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
8	1 7 4	atl0dm	⊢ ( 𝐾 ∈ AtLat → 𝐵 ∈ dom ( glb ‘ 𝐾 ) )
9	8	adantr	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 𝐵 ∈ dom ( glb ‘ 𝐾 ) )
10	1 4 2 3 5 6 9	p0le	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ 𝑋 )