Theorem orng0le1

Description: In an ordered ring, the ring unity is positive. (Contributed by Thierry Arnoux, 21-Jan-2018)

	Ref	Expression
Hypotheses	orng0le1.1	|- .0. = ( 0g ` F )
	orng0le1.2	|- .1. = ( 1r ` F )
	orng0le1.3	|- .<_ = ( le ` F )
Assertion	orng0le1	|- ( F e. oRing -> .0. .<_ .1. )

Proof

Step	Hyp	Ref	Expression
1		orng0le1.1	|- .0. = ( 0g ` F )
2		orng0le1.2	|- .1. = ( 1r ` F )
3		orng0le1.3	|- .<_ = ( le ` F )
4		orngring	|- ( F e. oRing -> F e. Ring )
5		eqid	|- ( Base ` F ) = ( Base ` F )
6	5 2	ringidcl	|- ( F e. Ring -> .1. e. ( Base ` F ) )
7	4 6	syl	|- ( F e. oRing -> .1. e. ( Base ` F ) )
8		eqid	|- ( .r ` F ) = ( .r ` F )
9	5 3 1 8	orngsqr	|- ( ( F e. oRing /\ .1. e. ( Base ` F ) ) -> .0. .<_ ( .1. ( .r ` F ) .1. ) )
10	7 9	mpdan	|- ( F e. oRing -> .0. .<_ ( .1. ( .r ` F ) .1. ) )
11	5 8 2	ringlidm	|- ( ( F e. Ring /\ .1. e. ( Base ` F ) ) -> ( .1. ( .r ` F ) .1. ) = .1. )
12	4 6 11	syl2anc2	|- ( F e. oRing -> ( .1. ( .r ` F ) .1. ) = .1. )
13	10 12	breqtrd	|- ( F e. oRing -> .0. .<_ .1. )