Metamath Proof Explorer

Theorem fldsdrgfld

Description: A sub-division-ring of a field is itself a field, so it is a subfield. We can therefore use SubDRing to express subfields. (Contributed by Thierry Arnoux, 11-Jan-2025)

		Ref	Expression
	Assertion	fldsdrgfld	$⊢ (F \in Field \land A \in SubDRing (F)) \to F ↾_{𝑠} A \in Field$

Proof

Step	Hyp	Ref	Expression
1		issdrg	$⊢ A \in SubDRing (F) \leftrightarrow (F \in DivRing \land A \in SubRing (F) \land F ↾_{𝑠} A \in DivRing)$
2	1	simp3bi	$⊢ A \in SubDRing (F) \to F ↾_{𝑠} A \in DivRing$
3	2	adantl	$⊢ (F \in Field \land A \in SubDRing (F)) \to F ↾_{𝑠} A \in DivRing$
4		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
5	4	simprbi	$⊢ F \in Field \to F \in CRing$
6	1	simp2bi	$⊢ A \in SubDRing (F) \to A \in SubRing (F)$
7		eqid	$⊢ F ↾_{𝑠} A = F ↾_{𝑠} A$
8	7	subrgcrng	$⊢ (F \in CRing \land A \in SubRing (F)) \to F ↾_{𝑠} A \in CRing$
9	5 6 8	syl2an	$⊢ (F \in Field \land A \in SubDRing (F)) \to F ↾_{𝑠} A \in CRing$
10		isfld	$⊢ F ↾_{𝑠} A \in Field \leftrightarrow (F ↾_{𝑠} A \in DivRing \land F ↾_{𝑠} A \in CRing)$
11	3 9 10	sylanbrc	$⊢ (F \in Field \land A \in SubDRing (F)) \to F ↾_{𝑠} A \in Field$