Metamath Proof Explorer

Theorem subofld

Description: Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018)

Ref Expression
Assertion subofld ⊢ F ∈ oField ∧ F ↾ 𝑠 A ∈ Field → F ↾ 𝑠 A ∈ oField

Proof

Step Hyp Ref Expression
1 simpr ⊢ F ∈ oField ∧ F ↾ 𝑠 A ∈ Field → F ↾ 𝑠 A ∈ Field
2 isofld ⊢ F ∈ oField ↔ F ∈ Field ∧ F ∈ oRing
3 2 simprbi ⊢ F ∈ oField → F ∈ oRing
4 3 adantr ⊢ F ∈ oField ∧ F ↾ 𝑠 A ∈ Field → F ∈ oRing
5 isfld ⊢ F ↾ 𝑠 A ∈ Field ↔ F ↾ 𝑠 A ∈ DivRing ∧ F ↾ 𝑠 A ∈ CRing
6 5 simprbi ⊢ F ↾ 𝑠 A ∈ Field → F ↾ 𝑠 A ∈ CRing
7 crngring ⊢ F ↾ 𝑠 A ∈ CRing → F ↾ 𝑠 A ∈ Ring
8 1 6 7 3syl ⊢ F ∈ oField ∧ F ↾ 𝑠 A ∈ Field → F ↾ 𝑠 A ∈ Ring
9 suborng ⊢ F ∈ oRing ∧ F ↾ 𝑠 A ∈ Ring → F ↾ 𝑠 A ∈ oRing
10 4 8 9 syl2anc ⊢ F ∈ oField ∧ F ↾ 𝑠 A ∈ Field → F ↾ 𝑠 A ∈ oRing
11 isofld ⊢ F ↾ 𝑠 A ∈ oField ↔ F ↾ 𝑠 A ∈ Field ∧ F ↾ 𝑠 A ∈ oRing
12 1 10 11 sylanbrc ⊢ F ∈ oField ∧ F ↾ 𝑠 A ∈ Field → F ↾ 𝑠 A ∈ oField