Theorem 0ltat

Description: An atom is greater than zero. (Contributed by NM, 4-Jul-2012)

	Ref	Expression
Hypotheses	0ltat.z	⊢ 0 = ( 0. ‘ 𝐾 )
	0ltat.s	⊢ < = ( lt ‘ 𝐾 )
	0ltat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	0ltat	⊢ ( ( 𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴 ) → 0 < 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		0ltat.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		0ltat.s	⊢ < = ( lt ‘ 𝐾 )
3		0ltat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		simpl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ OP )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6	5 1	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
7	6	adantr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴 ) → 0 ∈ ( Base ‘ 𝐾 ) )
8	5 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
9	8	adantl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
10		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
11	1 10 3	atcvr0	⊢ ( ( 𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴 ) → 0 ( ⋖ ‘ 𝐾 ) 𝑃 )
12	5 2 10	cvrlt	⊢ ( ( ( 𝐾 ∈ OP ∧ 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ∧ 0 ( ⋖ ‘ 𝐾 ) 𝑃 ) → 0 < 𝑃 )
13	4 7 9 11 12	syl31anc	⊢ ( ( 𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴 ) → 0 < 𝑃 )