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