fldextid

Description: The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023)

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

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{F} = {Base}_{F}$
2	1	ressid	$⊢ F \in Field \to F ↾_{𝑠} {Base}_{F} = F$
3	2	eqcomd	$⊢ F \in Field \to F = F ↾_{𝑠} {Base}_{F}$
4		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
5	4	simplbi	$⊢ F \in Field \to F \in DivRing$
6		drngring	$⊢ F \in DivRing \to F \in Ring$
7	1	subrgid	$⊢ F \in Ring \to {Base}_{F} \in SubRing (F)$
8	5 6 7	3syl	$⊢ F \in Field \to {Base}_{F} \in SubRing (F)$
9		brfldext	$⊢ (F \in Field \land F \in Field) \to (F /_{FldExt} F \leftrightarrow (F = F ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (F)))$
10	9	anidms	$⊢ F \in Field \to (F /_{FldExt} F \leftrightarrow (F = F ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (F)))$
11	3 8 10	mpbir2and	$⊢ F \in Field \to F /_{FldExt} F$

Metamath Proof Explorer