fldextfld2

Description: A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023)

		Ref	Expression
	Assertion	fldextfld2	$⊢ E /_{FldExt} F \to F \in Field$

Step	Hyp	Ref	Expression
1		opabssxp	$⊢ \{⟨e, f⟩ \| ((e \in Field \land f \in Field) \land (f = e ↾_{𝑠} {Base}_{f} \land {Base}_{f} \in SubRing (e)))\} \subseteq Field \times Field$
2		df-br	$⊢ E /_{FldExt} F \leftrightarrow ⟨E, F⟩ \in /_{FldExt}$
3	2	biimpi	$⊢ E /_{FldExt} F \to ⟨E, F⟩ \in /_{FldExt}$
4		df-fldext	$⊢ /_{FldExt} = \{⟨e, f⟩ \| ((e \in Field \land f \in Field) \land (f = e ↾_{𝑠} {Base}_{f} \land {Base}_{f} \in SubRing (e)))\}$
5	3 4	eleqtrdi	$⊢ E /_{FldExt} F \to ⟨E, F⟩ \in \{⟨e, f⟩ \| ((e \in Field \land f \in Field) \land (f = e ↾_{𝑠} {Base}_{f} \land {Base}_{f} \in SubRing (e)))\}$
6	1 5	sselid	$⊢ E /_{FldExt} F \to ⟨E, F⟩ \in (Field \times Field)$
7		opelxp2	$⊢ ⟨E, F⟩ \in (Field \times Field) \to F \in Field$
8	6 7	syl	$⊢ E /_{FldExt} F \to F \in Field$

Metamath Proof Explorer