Metamath Proof Explorer

Theorem extdgmul

Description: The multiplicativity formula for degrees of field extensions. Given E a field extension of F , itself a field extension of K , the degree of the extension E /FldExt K is the product of the degrees of the extensions E /FldExt F and F /FldExt K . Proposition 1.2 of Lang, p. 224. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion extdgmul 
|- ( ( E /FldExt F /\ F /FldExt K ) -> ( E [:] K ) = ( ( E [:] F ) *e ( F [:] K ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ( subringAlg ` E ) ` ( Base ` K ) ) = ( ( subringAlg ` E ) ` ( Base ` K ) )
2 eqid 
 |-  ( ( subringAlg ` E ) ` ( Base ` F ) ) = ( ( subringAlg ` E ) ` ( Base ` F ) )
3 eqid 
 |-  ( ( subringAlg ` ( E |`s ( Base ` F ) ) ) ` ( Base ` K ) ) = ( ( subringAlg ` ( E |`s ( Base ` F ) ) ) ` ( Base ` K ) )
4 eqid 
 |-  ( E |`s ( Base ` F ) ) = ( E |`s ( Base ` F ) )
5 eqid 
 |-  ( E |`s ( Base ` K ) ) = ( E |`s ( Base ` K ) )
6 simpl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> E /FldExt F )
7 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
8 6 7 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> E e. Field )
9 isfld 
 |-  ( E e. Field <-> ( E e. DivRing /\ E e. CRing ) )
10 9 simplbi 
 |-  ( E e. Field -> E e. DivRing )
11 8 10 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> E e. DivRing )
12 fldextfld1 
 |-  ( F /FldExt K -> F e. Field )
13 12 adantl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> F e. Field )
14 brfldext 
 |-  ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
15 8 13 14 syl2anc 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
16 6 15 mpbid 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) )
17 16 simpld 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> F = ( E |`s ( Base ` F ) ) )
18 isfld 
 |-  ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
19 18 simplbi 
 |-  ( F e. Field -> F e. DivRing )
20 13 19 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> F e. DivRing )
21 17 20 eqeltrrd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E |`s ( Base ` F ) ) e. DivRing )
22 fldexttr 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> E /FldExt K )
23 fldextfld2 
 |-  ( F /FldExt K -> K e. Field )
24 23 adantl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> K e. Field )
25 brfldext 
 |-  ( ( E e. Field /\ K e. Field ) -> ( E /FldExt K <-> ( K = ( E |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` E ) ) ) )
26 8 24 25 syl2anc 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E /FldExt K <-> ( K = ( E |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` E ) ) ) )
27 22 26 mpbid 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( K = ( E |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` E ) ) )
28 27 simpld 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> K = ( E |`s ( Base ` K ) ) )
29 isfld 
 |-  ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) )
30 29 simplbi 
 |-  ( K e. Field -> K e. DivRing )
31 24 30 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> K e. DivRing )
32 28 31 eqeltrrd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E |`s ( Base ` K ) ) e. DivRing )
33 16 simprd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( Base ` F ) e. ( SubRing ` E ) )
34 eqid 
 |-  ( Base ` K ) = ( Base ` K )
35 34 fldextsubrg 
 |-  ( F /FldExt K -> ( Base ` K ) e. ( SubRing ` F ) )
36 35 adantl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( Base ` K ) e. ( SubRing ` F ) )
37 17 fveq2d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( SubRing ` F ) = ( SubRing ` ( E |`s ( Base ` F ) ) ) )
38 36 37 eleqtrd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( Base ` K ) e. ( SubRing ` ( E |`s ( Base ` F ) ) ) )
39 1 2 3 4 5 11 21 32 33 38 fedgmul 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` K ) ) ) = ( ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) *e ( dim ` ( ( subringAlg ` ( E |`s ( Base ` F ) ) ) ` ( Base ` K ) ) ) ) )
40 extdgval 
 |-  ( E /FldExt K -> ( E [:] K ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` K ) ) ) )
41 22 40 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E [:] K ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` K ) ) ) )
42 extdgval 
 |-  ( E /FldExt F -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
43 6 42 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
44 extdgval 
 |-  ( F /FldExt K -> ( F [:] K ) = ( dim ` ( ( subringAlg ` F ) ` ( Base ` K ) ) ) )
45 44 adantl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F [:] K ) = ( dim ` ( ( subringAlg ` F ) ` ( Base ` K ) ) ) )
46 17 fveq2d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( subringAlg ` F ) = ( subringAlg ` ( E |`s ( Base ` F ) ) ) )
47 46 fveq1d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( ( subringAlg ` F ) ` ( Base ` K ) ) = ( ( subringAlg ` ( E |`s ( Base ` F ) ) ) ` ( Base ` K ) ) )
48 47 fveq2d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( dim ` ( ( subringAlg ` F ) ` ( Base ` K ) ) ) = ( dim ` ( ( subringAlg ` ( E |`s ( Base ` F ) ) ) ` ( Base ` K ) ) ) )
49 45 48 eqtrd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F [:] K ) = ( dim ` ( ( subringAlg ` ( E |`s ( Base ` F ) ) ) ` ( Base ` K ) ) ) )
50 43 49 oveq12d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( ( E [:] F ) *e ( F [:] K ) ) = ( ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) *e ( dim ` ( ( subringAlg ` ( E |`s ( Base ` F ) ) ) ` ( Base ` K ) ) ) ) )
51 39 41 50 3eqtr4d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E [:] K ) = ( ( E [:] F ) *e ( F [:] K ) ) )