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 e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. oField )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( F e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. Field )
2 isofld
 |-  ( F e. oField <-> ( F e. Field /\ F e. oRing ) )
3 2 simprbi
 |-  ( F e. oField -> F e. oRing )
4 3 adantr
 |-  ( ( F e. oField /\ ( F |`s A ) e. Field ) -> F e. oRing )
5 isfld
 |-  ( ( F |`s A ) e. Field <-> ( ( F |`s A ) e. DivRing /\ ( F |`s A ) e. CRing ) )
6 5 simprbi
 |-  ( ( F |`s A ) e. Field -> ( F |`s A ) e. CRing )
7 crngring
 |-  ( ( F |`s A ) e. CRing -> ( F |`s A ) e. Ring )
8 1 6 7 3syl
 |-  ( ( F e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. Ring )
9 suborng
 |-  ( ( F e. oRing /\ ( F |`s A ) e. Ring ) -> ( F |`s A ) e. oRing )
10 4 8 9 syl2anc
 |-  ( ( F e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. oRing )
11 isofld
 |-  ( ( F |`s A ) e. oField <-> ( ( F |`s A ) e. Field /\ ( F |`s A ) e. oRing ) )
12 1 10 11 sylanbrc
 |-  ( ( F e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. oField )