# Metamath Proof Explorer

## Theorem opltn0

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

Ref Expression
Hypotheses opltne0.b
`|- B = ( Base ` K )`
opltne0.s
`|- .< = ( lt ` K )`
opltne0.z
`|- .0. = ( 0. ` K )`
Assertion opltn0
`|- ( ( K e. OP /\ X e. B ) -> ( .0. .< X <-> X =/= .0. ) )`

### Proof

Step Hyp Ref Expression
1 opltne0.b
` |-  B = ( Base ` K )`
2 opltne0.s
` |-  .< = ( lt ` K )`
3 opltne0.z
` |-  .0. = ( 0. ` K )`
4 simpl
` |-  ( ( K e. OP /\ X e. B ) -> K e. OP )`
5 1 3 op0cl
` |-  ( K e. OP -> .0. e. B )`
` |-  ( ( K e. OP /\ X e. B ) -> .0. e. B )`
7 simpr
` |-  ( ( K e. OP /\ X e. B ) -> X e. B )`
8 eqid
` |-  ( le ` K ) = ( le ` K )`
9 8 2 pltval
` |-  ( ( K e. OP /\ .0. e. B /\ X e. B ) -> ( .0. .< X <-> ( .0. ( le ` K ) X /\ .0. =/= X ) ) )`
10 4 6 7 9 syl3anc
` |-  ( ( K e. OP /\ X e. B ) -> ( .0. .< X <-> ( .0. ( le ` K ) X /\ .0. =/= X ) ) )`
11 necom
` |-  ( X =/= .0. <-> .0. =/= X )`
12 1 8 3 op0le
` |-  ( ( K e. OP /\ X e. B ) -> .0. ( le ` K ) X )`
13 12 biantrurd
` |-  ( ( K e. OP /\ X e. B ) -> ( .0. =/= X <-> ( .0. ( le ` K ) X /\ .0. =/= X ) ) )`
14 11 13 syl5rbb
` |-  ( ( K e. OP /\ X e. B ) -> ( ( .0. ( le ` K ) X /\ .0. =/= X ) <-> X =/= .0. ) )`
15 10 14 bitrd
` |-  ( ( K e. OP /\ X e. B ) -> ( .0. .< X <-> X =/= .0. ) )`