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 )