Metamath Proof Explorer

Theorem extdgcl

Description: Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion extdgcl 
|- ( E /FldExt F -> ( E [:] F ) e. NN0* )

Proof

Step Hyp Ref Expression
1 extdgval 
 |-  ( E /FldExt F -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
2 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
3 isfld 
 |-  ( E e. Field <-> ( E e. DivRing /\ E e. CRing ) )
4 2 3 sylib 
 |-  ( E /FldExt F -> ( E e. DivRing /\ E e. CRing ) )
5 4 simpld 
 |-  ( E /FldExt F -> E e. DivRing )
6 fldextress 
 |-  ( E /FldExt F -> F = ( E |`s ( Base ` F ) ) )
7 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
8 isfld 
 |-  ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
9 7 8 sylib 
 |-  ( E /FldExt F -> ( F e. DivRing /\ F e. CRing ) )
10 9 simpld 
 |-  ( E /FldExt F -> F e. DivRing )
11 6 10 eqeltrrd 
 |-  ( E /FldExt F -> ( E |`s ( Base ` F ) ) e. DivRing )
12 eqid 
 |-  ( Base ` F ) = ( Base ` F )
13 12 fldextsubrg 
 |-  ( E /FldExt F -> ( Base ` F ) e. ( SubRing ` E ) )
14 eqid 
 |-  ( ( subringAlg ` E ) ` ( Base ` F ) ) = ( ( subringAlg ` E ) ` ( Base ` F ) )
15 eqid 
 |-  ( E |`s ( Base ` F ) ) = ( E |`s ( Base ` F ) )
16 14 15 sralvec 
 |-  ( ( E e. DivRing /\ ( E |`s ( Base ` F ) ) e. DivRing /\ ( Base ` F ) e. ( SubRing ` E ) ) -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec )
17 5 11 13 16 syl3anc 
 |-  ( E /FldExt F -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec )
18 dimcl 
 |-  ( ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) e. NN0* )
19 17 18 syl 
 |-  ( E /FldExt F -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) e. NN0* )
20 1 19 eqeltrd 
 |-  ( E /FldExt F -> ( E [:] F ) e. NN0* )