Metamath Proof Explorer

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 ⊢ φ → E /FinExt F
Assertion finextalg ⊢ φ → E /AlgExt F

Proof

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