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 
|- ( ph -> E /FinExt F )
Assertion finextalg 
|- ( ph -> E /AlgExt F )

Proof

Step Hyp Ref Expression
1 finextalg.1 
 |-  ( ph -> E /FinExt F )
2 1 finextfldext 
 |-  ( ph -> 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 e. Field )
6 2 5 syl 
 |-  ( ph -> E e. Field )
7 eqid 
 |-  ( Base ` F ) = ( Base ` F )
8 7 2 fldextsdrg 
 |-  ( ph -> ( Base ` F ) e. ( SubDRing ` E ) )
9 extdgval 
 |-  ( E /FldExt F -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
10 2 9 syl 
 |-  ( ph -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
11 brfinext 
 |-  ( E /FldExt F -> ( E /FinExt F <-> ( E [:] F ) e. NN0 ) )
12 2 11 syl 
 |-  ( ph -> ( E /FinExt F <-> ( E [:] F ) e. NN0 ) )
13 1 12 mpbid 
 |-  ( ph -> ( E [:] F ) e. NN0 )
14 10 13 eqeltrrd 
 |-  ( ph -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) e. NN0 )
15 3 4 6 8 14 extdgfialg 
 |-  ( ph -> ( E IntgRing ( Base ` F ) ) = ( Base ` E ) )
16 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
17 2 16 syl 
 |-  ( ph -> F e. Field )
18 3 7 6 17 bralgext 
 |-  ( ph -> ( E /AlgExt F <-> ( E /FldExt F /\ ( E IntgRing ( Base ` F ) ) = ( Base ` E ) ) ) )
19 2 15 18 mpbir2and 
 |-  ( ph -> E /AlgExt F )