Metamath Proof Explorer


Theorem orng0le1

Description: In an ordered ring, the ring unit 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. )