Metamath Proof Explorer

Theorem fldextrspundgle

Description: Inequality involving the degree of two different field extensions I and J of a same field F . Part of the proof of Proposition 5, Chapter 5, of BourbakiAlg2 p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 fldextrspunfld.k 
 |-  K = ( L |`s F )
2 fldextrspunfld.i 
 |-  I = ( L |`s G )
3 fldextrspunfld.j 
 |-  J = ( L |`s H )
4 fldextrspunfld.2 
 |-  ( ph -> L e. Field )
5 fldextrspunfld.3 
 |-  ( ph -> F e. ( SubDRing ` I ) )
6 fldextrspunfld.4 
 |-  ( ph -> F e. ( SubDRing ` J ) )
7 fldextrspunfld.5 
 |-  ( ph -> G e. ( SubDRing ` L ) )
8 fldextrspunfld.6 
 |-  ( ph -> H e. ( SubDRing ` L ) )
9 fldextrspunfld.7 
 |-  ( ph -> ( J [:] K ) e. NN0 )
10 fldextrspundgle.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 extdgval 
 |-  ( E /FldExt I -> ( E [:] I ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` I ) ) ) )
16 14 15 syl 
 |-  ( ph -> ( E [:] I ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` I ) ) ) )
17 eqid 
 |-  ( RingSpan ` L ) = ( RingSpan ` L )
18 eqid 
 |-  ( ( RingSpan ` L ) ` ( G u. H ) ) = ( ( RingSpan ` L ) ` ( G u. H ) )
19 eqid 
 |-  ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) = ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) )
20 1 2 3 4 5 6 7 8 9 17 18 19 fldextrspunlem2 
 |-  ( ph -> ( ( RingSpan ` L ) ` ( G u. H ) ) = ( L fldGen ( G u. H ) ) )
21 20 oveq2d 
 |-  ( ph -> ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) = ( L |`s ( L fldGen ( G u. H ) ) ) )
22 21 10 eqtr4di 
 |-  ( ph -> ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) = E )
23 22 fveq2d 
 |-  ( ph -> ( subringAlg ` ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) ) = ( subringAlg ` E ) )
24 11 sdrgss 
 |-  ( G e. ( SubDRing ` L ) -> G C_ ( Base ` L ) )
25 2 11 ressbas2 
 |-  ( G C_ ( Base ` L ) -> G = ( Base ` I ) )
26 7 24 25 3syl 
 |-  ( ph -> G = ( Base ` I ) )
27 23 26 fveq12d 
 |-  ( ph -> ( ( subringAlg ` ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) ) ` G ) = ( ( subringAlg ` E ) ` ( Base ` I ) ) )
28 27 fveq2d 
 |-  ( ph -> ( dim ` ( ( subringAlg ` ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) ) ` G ) ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` I ) ) ) )
29 1 2 3 4 5 6 7 8 9 17 18 19 fldextrspunlem1 
 |-  ( ph -> ( dim ` ( ( subringAlg ` ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) ) ` G ) ) <_ ( J [:] K ) )
30 28 29 eqbrtrrd 
 |-  ( ph -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` I ) ) ) <_ ( J [:] K ) )
31 16 30 eqbrtrd 
 |-  ( ph -> ( E [:] I ) <_ ( J [:] K ) )