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 \in oField \land F ↾_{𝑠} A \in Field) \to F ↾_{𝑠} A \in oField$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (F \in oField \land F ↾_{𝑠} A \in Field) \to F ↾_{𝑠} A \in Field$
2		isofld	$⊢ F \in oField \leftrightarrow (F \in Field \land F \in oRing)$
3	2	simprbi	$⊢ F \in oField \to F \in oRing$
4	3	adantr	$⊢ (F \in oField \land F ↾_{𝑠} A \in Field) \to F \in oRing$
5		isfld	$⊢ F ↾_{𝑠} A \in Field \leftrightarrow (F ↾_{𝑠} A \in DivRing \land F ↾_{𝑠} A \in CRing)$
6	5	simprbi	$⊢ F ↾_{𝑠} A \in Field \to F ↾_{𝑠} A \in CRing$
7		crngring	$⊢ F ↾_{𝑠} A \in CRing \to F ↾_{𝑠} A \in Ring$
8	1 6 7	3syl	$⊢ (F \in oField \land F ↾_{𝑠} A \in Field) \to F ↾_{𝑠} A \in Ring$
9		suborng	$⊢ (F \in oRing \land F ↾_{𝑠} A \in Ring) \to F ↾_{𝑠} A \in oRing$
10	4 8 9	syl2anc	$⊢ (F \in oField \land F ↾_{𝑠} A \in Field) \to F ↾_{𝑠} A \in oRing$
11		isofld	$⊢ F ↾_{𝑠} A \in oField \leftrightarrow (F ↾_{𝑠} A \in Field \land F ↾_{𝑠} A \in oRing)$
12	1 10 11	sylanbrc	$⊢ (F \in oField \land F ↾_{𝑠} A \in Field) \to F ↾_{𝑠} A \in oField$

Metamath Proof Explorer