Theorem finextalg

Description: A finite field extension is algebraic. Proposition 1.1 of Lang, p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypothesis	finextalg.1	⊢ ( 𝜑 → 𝐸 /FinExt 𝐹 )
Assertion	finextalg	⊢ ( 𝜑 → 𝐸 /AlgExt 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		finextalg.1	⊢ ( 𝜑 → 𝐸 /FinExt 𝐹 )
2	1	finextfldext	⊢ ( 𝜑 → 𝐸 /FldExt 𝐹 )
3		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
4		eqid	⊢ ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
5		fldextfld1	⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )
6	2 5	syl	⊢ ( 𝜑 → 𝐸 ∈ Field )
7		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
8	7 2	fldextsdrg	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) ∈ ( SubDRing ‘ 𝐸 ) )
9		extdgval	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
10	2 9	syl	⊢ ( 𝜑 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
11		brfinext	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) )
12	2 11	syl	⊢ ( 𝜑 → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) )
13	1 12	mpbid	⊢ ( 𝜑 → ( 𝐸 [:] 𝐹 ) ∈ ℕ0 )
14	10 13	eqeltrrd	⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ ℕ0 )
15	3 4 6 8 14	extdgfialg	⊢ ( 𝜑 → ( 𝐸 IntgRing ( Base ‘ 𝐹 ) ) = ( Base ‘ 𝐸 ) )
16		fldextfld2	⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ Field )
17	2 16	syl	⊢ ( 𝜑 → 𝐹 ∈ Field )
18	3 7 6 17	bralgext	⊢ ( 𝜑 → ( 𝐸 /AlgExt 𝐹 ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 IntgRing ( Base ‘ 𝐹 ) ) = ( Base ‘ 𝐸 ) ) ) )
19	2 15 18	mpbir2and	⊢ ( 𝜑 → 𝐸 /AlgExt 𝐹 )