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

Metamath Proof Explorer

Theorem atlltn0

Description: A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses atlltne0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
atlltne0.s ⊢ < = ( lt ‘ 𝐾 )
atlltne0.z ⊢ 0 = ( 0. ‘ 𝐾 )
Assertion atlltn0 ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ) )

Proof

Step Hyp Ref Expression
1 atlltne0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atlltne0.s ⊢ < = ( lt ‘ 𝐾 )
3 atlltne0.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 simpl ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ AtLat )
5 1 3 atl0cl ⊢ ( 𝐾 ∈ AtLat → 0 ∈ 𝐵 )
6 5 adantr ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
7 simpr ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 8 2 pltval ⊢ ( ( 𝐾 ∈ AtLat ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ ( 0 ( le ‘ 𝐾 ) 𝑋 ∧ 0 ≠ 𝑋 ) ) )
10 4 6 7 9 syl3anc ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ ( 0 ( le ‘ 𝐾 ) 𝑋 ∧ 0 ≠ 𝑋 ) ) )
11 necom ⊢ ( 𝑋 ≠ 0 ↔ 0 ≠ 𝑋 )
12 1 8 3 atl0le ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → 0 ( le ‘ 𝐾 ) 𝑋 )
13 12 biantrurd ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( 0 ≠ 𝑋 ↔ ( 0 ( le ‘ 𝐾 ) 𝑋 ∧ 0 ≠ 𝑋 ) ) )
14 11 13 bitr2id ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ( le ‘ 𝐾 ) 𝑋 ∧ 0 ≠ 𝑋 ) ↔ 𝑋 ≠ 0 ) )
15 10 14 bitrd ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ) )