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