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𝐹 )
orng0le1.2 1 = ( 1r𝐹 )
orng0le1.3 = ( le ‘ 𝐹 )
Assertion orng0le1 ( 𝐹 ∈ oRing → 0 1 )

Proof

Step Hyp Ref Expression
1 orng0le1.1 0 = ( 0g𝐹 )
2 orng0le1.2 1 = ( 1r𝐹 )
3 orng0le1.3 = ( le ‘ 𝐹 )
4 orngring ( 𝐹 ∈ oRing → 𝐹 ∈ Ring )
5 eqid ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
6 5 2 ringidcl ( 𝐹 ∈ Ring → 1 ∈ ( Base ‘ 𝐹 ) )
7 4 6 syl ( 𝐹 ∈ oRing → 1 ∈ ( Base ‘ 𝐹 ) )
8 eqid ( .r𝐹 ) = ( .r𝐹 )
9 5 3 1 8 orngsqr ( ( 𝐹 ∈ oRing ∧ 1 ∈ ( Base ‘ 𝐹 ) ) → 0 ( 1 ( .r𝐹 ) 1 ) )
10 7 9 mpdan ( 𝐹 ∈ oRing → 0 ( 1 ( .r𝐹 ) 1 ) )
11 5 8 2 ringlidm ( ( 𝐹 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝐹 ) ) → ( 1 ( .r𝐹 ) 1 ) = 1 )
12 4 6 11 syl2anc2 ( 𝐹 ∈ oRing → ( 1 ( .r𝐹 ) 1 ) = 1 )
13 10 12 breqtrd ( 𝐹 ∈ oRing → 0 1 )