Metamath Proof Explorer

Theorem extdggt0

Description: Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion extdggt0 
|- ( E /FldExt F -> 0 < ( E [:] F ) )

Proof

Step Hyp Ref Expression
1 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
2 isfld 
 |-  ( E e. Field <-> ( E e. DivRing /\ E e. CRing ) )
3 2 simplbi 
 |-  ( E e. Field -> E e. DivRing )
4 1 3 syl 
 |-  ( E /FldExt F -> E e. DivRing )
5 fldextress 
 |-  ( E /FldExt F -> F = ( E |`s ( Base ` F ) ) )
6 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
7 isfld 
 |-  ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
8 7 simplbi 
 |-  ( F e. Field -> F e. DivRing )
9 6 8 syl 
 |-  ( E /FldExt F -> F e. DivRing )
10 5 9 eqeltrrd 
 |-  ( E /FldExt F -> ( E |`s ( Base ` F ) ) e. DivRing )
11 eqid 
 |-  ( Base ` F ) = ( Base ` F )
12 11 fldextsubrg 
 |-  ( E /FldExt F -> ( Base ` F ) e. ( SubRing ` E ) )
13 eqid 
 |-  ( ( subringAlg ` E ) ` ( Base ` F ) ) = ( ( subringAlg ` E ) ` ( Base ` F ) )
14 eqid 
 |-  ( E |`s ( Base ` F ) ) = ( E |`s ( Base ` F ) )
15 13 14 sralvec 
 |-  ( ( E e. DivRing /\ ( E |`s ( Base ` F ) ) e. DivRing /\ ( Base ` F ) e. ( SubRing ` E ) ) -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec )
16 4 10 12 15 syl3anc 
 |-  ( E /FldExt F -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec )
17 eqid 
 |-  ( Base ` E ) = ( Base ` E )
18 17 subrgss 
 |-  ( ( Base ` F ) e. ( SubRing ` E ) -> ( Base ` F ) C_ ( Base ` E ) )
19 12 18 syl 
 |-  ( E /FldExt F -> ( Base ` F ) C_ ( Base ` E ) )
20 13 17 sradrng 
 |-  ( ( E e. DivRing /\ ( Base ` F ) C_ ( Base ` E ) ) -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. DivRing )
21 4 19 20 syl2anc 
 |-  ( E /FldExt F -> ( ( subringAlg ` E ) ` ( Base ` F ) ) e. DivRing )
22 drngdimgt0 
 |-  ( ( ( ( subringAlg ` E ) ` ( Base ` F ) ) e. LVec /\ ( ( subringAlg ` E ) ` ( Base ` F ) ) e. DivRing ) -> 0 < ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
23 16 21 22 syl2anc 
 |-  ( E /FldExt F -> 0 < ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
24 extdgval 
 |-  ( E /FldExt F -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
25 23 24 breqtrrd 
 |-  ( E /FldExt F -> 0 < ( E [:] F ) )