extdgcl

Description: Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023)

		Ref	Expression
	Assertion	extdgcl	$⊢ E /_{FldExt} F \to E [. : .] F \in ℕ_{0}^{*}$

Step	Hyp	Ref	Expression
1		extdgval	$⊢ E /_{FldExt} F \to E [. : .] F = \dim (subringAlg (E) ({Base}_{F}))$
2		fldextfld1	$⊢ E /_{FldExt} F \to E \in Field$
3		isfld	$⊢ E \in Field \leftrightarrow (E \in DivRing \land E \in CRing)$
4	2 3	sylib	$⊢ E /_{FldExt} F \to (E \in DivRing \land E \in CRing)$
5	4	simpld	$⊢ E /_{FldExt} F \to E \in DivRing$
6		fldextress	$⊢ E /_{FldExt} F \to F = E ↾_{𝑠} {Base}_{F}$
7		fldextfld2	$⊢ E /_{FldExt} F \to F \in Field$
8		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
9	7 8	sylib	$⊢ E /_{FldExt} F \to (F \in DivRing \land F \in CRing)$
10	9	simpld	$⊢ E /_{FldExt} F \to F \in DivRing$
11	6 10	eqeltrrd	$⊢ E /_{FldExt} F \to E ↾_{𝑠} {Base}_{F} \in DivRing$
12		eqid	$⊢ {Base}_{F} = {Base}_{F}$
13	12	fldextsubrg	$⊢ E /_{FldExt} F \to {Base}_{F} \in SubRing (E)$
14		eqid	$⊢ subringAlg (E) ({Base}_{F}) = subringAlg (E) ({Base}_{F})$
15		eqid	$⊢ E ↾_{𝑠} {Base}_{F} = E ↾_{𝑠} {Base}_{F}$
16	14 15	sralvec	$⊢ (E \in DivRing \land E ↾_{𝑠} {Base}_{F} \in DivRing \land {Base}_{F} \in SubRing (E)) \to subringAlg (E) ({Base}_{F}) \in LVec$
17	5 11 13 16	syl3anc	$⊢ E /_{FldExt} F \to subringAlg (E) ({Base}_{F}) \in LVec$
18		dimcl	$⊢ subringAlg (E) ({Base}_{F}) \in LVec \to \dim (subringAlg (E) ({Base}_{F})) \in ℕ_{0}^{*}$
19	17 18	syl	$⊢ E /_{FldExt} F \to \dim (subringAlg (E) ({Base}_{F})) \in ℕ_{0}^{*}$
20	1 19	eqeltrd	$⊢ E /_{FldExt} F \to E [. : .] F \in ℕ_{0}^{*}$

Metamath Proof Explorer