Theorem 0ltat

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

	Ref	Expression
Hypotheses	0ltat.z	|- .0. = ( 0. ` K )
	0ltat.s	|- .< = ( lt ` K )
	0ltat.a	|- A = ( Atoms ` K )
Assertion	0ltat	|- ( ( K e. OP /\ P e. A ) -> .0. .< P )

Proof

Step	Hyp	Ref	Expression
1		0ltat.z	|- .0. = ( 0. ` K )
2		0ltat.s	|- .< = ( lt ` K )
3		0ltat.a	|- A = ( Atoms ` K )
4		simpl	|- ( ( K e. OP /\ P e. A ) -> K e. OP )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6	5 1	op0cl	|- ( K e. OP -> .0. e. ( Base ` K ) )
7	6	adantr	|- ( ( K e. OP /\ P e. A ) -> .0. e. ( Base ` K ) )
8	5 3	atbase	|- ( P e. A -> P e. ( Base ` K ) )
9	8	adantl	|- ( ( K e. OP /\ P e. A ) -> P e. ( Base ` K ) )
10		eqid	|- (
11	1 10 3	atcvr0	|- ( ( K e. OP /\ P e. A ) -> .0. (
12	5 2 10	cvrlt	|- ( ( ( K e. OP /\ .0. e. ( Base ` K ) /\ P e. ( Base ` K ) ) /\ .0. ( .0. .< P )
13	4 7 9 11 12	syl31anc	|- ( ( K e. OP /\ P e. A ) -> .0. .< P )