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

Metamath Proof Explorer

Theorem atlle0

Description: An element less than or equal to zero equals zero. ( chle0 analog.) (Contributed by NM, 21-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 atl0le.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atl0le.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atl0le.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 1 2 3 atl0le ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ 𝑋 )
5 4 biantrud ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≤ 0 ↔ ( 𝑋 ≤ 0 ∧ 0 ≤ 𝑋 ) ) )
6 atlpos ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Poset )
7 6 adantr ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Poset )
8 simpr ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
9 1 3 atl0cl ⊢ ( 𝐾 ∈ AtLat → 0 ∈ 𝐵 )
10 9 adantr ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
11 1 2 posasymb ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( ( 𝑋 ≤ 0 ∧ 0 ≤ 𝑋 ) ↔ 𝑋 = 0 ) )
12 7 8 10 11 syl3anc ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ≤ 0 ∧ 0 ≤ 𝑋 ) ↔ 𝑋 = 0 ) )
13 5 12 bitrd ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≤ 0 ↔ 𝑋 = 0 ) )