Metamath Proof Explorer

Theorem extdgid

Description: A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023)

Ref Expression
Assertion extdgid 
|- ( E e. Field -> ( E [:] E ) = 1 )

Proof

Step Hyp Ref Expression
1 fldextid 
 |-  ( E e. Field -> E /FldExt E )
2 extdgval 
 |-  ( E /FldExt E -> ( E [:] E ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` E ) ) ) )
3 1 2 syl 
 |-  ( E e. Field -> ( E [:] E ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` E ) ) ) )
4 rlmval 
 |-  ( ringLMod ` E ) = ( ( subringAlg ` E ) ` ( Base ` E ) )
5 4 eqcomi 
 |-  ( ( subringAlg ` E ) ` ( Base ` E ) ) = ( ringLMod ` E )
6 5 rgmoddim 
 |-  ( E e. Field -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` E ) ) ) = 1 )
7 3 6 eqtrd 
 |-  ( E e. Field -> ( E [:] E ) = 1 )