Metamath Proof Explorer

Theorem fldextrspundglemul

Description: Given two field extensions I / K and J / K of the same field K , J / K being finite, and the composiste field E = I J , the degree of the extension of the composite field E / K is at most the product of the field extension degrees of I / K and J / K . (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses fldextrspun.k 
|- K = ( L |`s F )
fldextrspun.i 
|- I = ( L |`s G )
fldextrspun.j 
|- J = ( L |`s H )
fldextrspun.2 
|- ( ph -> L e. Field )
fldextrspun.3 
|- ( ph -> F e. ( SubDRing ` I ) )
fldextrspun.4 
|- ( ph -> F e. ( SubDRing ` J ) )
fldextrspun.5 
|- ( ph -> G e. ( SubDRing ` L ) )
fldextrspun.6 
|- ( ph -> H e. ( SubDRing ` L ) )
fldextrspundglemul.7 
|- ( ph -> ( J [:] K ) e. NN0 )
fldextrspundglemul.1 
|- E = ( L |`s ( L fldGen ( G u. H ) ) )
Assertion fldextrspundglemul 
|- ( ph -> ( E [:] K ) <_ ( ( I [:] K ) *e ( J [:] K ) ) )

Proof

Step Hyp Ref Expression
1 fldextrspun.k 
 |-  K = ( L |`s F )
2 fldextrspun.i 
 |-  I = ( L |`s G )
3 fldextrspun.j 
 |-  J = ( L |`s H )
4 fldextrspun.2 
 |-  ( ph -> L e. Field )
5 fldextrspun.3 
 |-  ( ph -> F e. ( SubDRing ` I ) )
6 fldextrspun.4 
 |-  ( ph -> F e. ( SubDRing ` J ) )
7 fldextrspun.5 
 |-  ( ph -> G e. ( SubDRing ` L ) )
8 fldextrspun.6 
 |-  ( ph -> H e. ( SubDRing ` L ) )
9 fldextrspundglemul.7 
 |-  ( ph -> ( J [:] K ) e. NN0 )
10 fldextrspundglemul.1 
 |-  E = ( L |`s ( L fldGen ( G u. H ) ) )
11 eqid 
 |-  ( Base ` L ) = ( Base ` L )
12 11 sdrgss 
 |-  ( H e. ( SubDRing ` L ) -> H C_ ( Base ` L ) )
13 8 12 syl 
 |-  ( ph -> H C_ ( Base ` L ) )
14 11 2 10 4 7 13 fldgenfldext 
 |-  ( ph -> E /FldExt I )
15 extdgcl 
 |-  ( E /FldExt I -> ( E [:] I ) e. NN0* )
16 xnn0xr 
 |-  ( ( E [:] I ) e. NN0* -> ( E [:] I ) e. RR* )
17 14 15 16 3syl 
 |-  ( ph -> ( E [:] I ) e. RR* )
18 3 4 8 6 1 fldsdrgfldext2 
 |-  ( ph -> J /FldExt K )
19 extdgcl 
 |-  ( J /FldExt K -> ( J [:] K ) e. NN0* )
20 xnn0xr 
 |-  ( ( J [:] K ) e. NN0* -> ( J [:] K ) e. RR* )
21 18 19 20 3syl 
 |-  ( ph -> ( J [:] K ) e. RR* )
22 2 4 7 5 1 fldsdrgfldext2 
 |-  ( ph -> I /FldExt K )
23 extdgcl 
 |-  ( I /FldExt K -> ( I [:] K ) e. NN0* )
24 xnn0xrge0 
 |-  ( ( I [:] K ) e. NN0* -> ( I [:] K ) e. ( 0 [,] +oo ) )
25 22 23 24 3syl 
 |-  ( ph -> ( I [:] K ) e. ( 0 [,] +oo ) )
26 elxrge0 
 |-  ( ( I [:] K ) e. ( 0 [,] +oo ) <-> ( ( I [:] K ) e. RR* /\ 0 <_ ( I [:] K ) ) )
27 25 26 sylib 
 |-  ( ph -> ( ( I [:] K ) e. RR* /\ 0 <_ ( I [:] K ) ) )
28 1 2 3 4 5 6 7 8 9 10 fldextrspundgle 
 |-  ( ph -> ( E [:] I ) <_ ( J [:] K ) )
29 xlemul1a 
 |-  ( ( ( ( E [:] I ) e. RR* /\ ( J [:] K ) e. RR* /\ ( ( I [:] K ) e. RR* /\ 0 <_ ( I [:] K ) ) ) /\ ( E [:] I ) <_ ( J [:] K ) ) -> ( ( E [:] I ) *e ( I [:] K ) ) <_ ( ( J [:] K ) *e ( I [:] K ) ) )
30 17 21 27 28 29 syl31anc 
 |-  ( ph -> ( ( E [:] I ) *e ( I [:] K ) ) <_ ( ( J [:] K ) *e ( I [:] K ) ) )
31 extdgmul 
 |-  ( ( E /FldExt I /\ I /FldExt K ) -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
32 14 22 31 syl2anc 
 |-  ( ph -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
33 xnn0xr 
 |-  ( ( I [:] K ) e. NN0* -> ( I [:] K ) e. RR* )
34 22 23 33 3syl 
 |-  ( ph -> ( I [:] K ) e. RR* )
35 xmulcom 
 |-  ( ( ( I [:] K ) e. RR* /\ ( J [:] K ) e. RR* ) -> ( ( I [:] K ) *e ( J [:] K ) ) = ( ( J [:] K ) *e ( I [:] K ) ) )
36 34 21 35 syl2anc 
 |-  ( ph -> ( ( I [:] K ) *e ( J [:] K ) ) = ( ( J [:] K ) *e ( I [:] K ) ) )
37 30 32 36 3brtr4d 
 |-  ( ph -> ( E [:] K ) <_ ( ( I [:] K ) *e ( J [:] K ) ) )