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

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 ( ( 𝐹 ∈ oField ∧ ( 𝐹 ↾s 𝐴 ) ∈ Field ) → ( 𝐹 ↾s 𝐴 ) ∈ oField )

Proof

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