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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	opltne0.s	⊢ < = ( lt ‘ 𝐾 )
	opltne0.z	⊢ 0 = ( 0. ‘ 𝐾 )
Assertion	opltn0	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ) )

Proof

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