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 ‘ 𝐹 )
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 )