This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. )