This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 isfld 
 |-  ( E e. Field <-> ( E e. DivRing /\ E e. CRing ) )
5 4 simplbi 
 |-  ( E e. Field -> E e. DivRing )
6 rlmval 
 |-  ( ringLMod ` E ) = ( ( subringAlg ` E ) ` ( Base ` E ) )
7 6 eqcomi 
 |-  ( ( subringAlg ` E ) ` ( Base ` E ) ) = ( ringLMod ` E )
8 7 rlmdim 
 |-  ( E e. DivRing -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` E ) ) ) = 1 )
9 5 8 syl 
 |-  ( E e. Field -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` E ) ) ) = 1 )
10 3 9 eqtrd 
 |-  ( E e. Field -> ( E [:] E ) = 1 )