Metamath Proof Explorer

Theorem fldextrspundgdvds

Description: Given two finite extensions I / K and J / K of the same field K , the degree of the extension I / K divides the degree of the extension E / K , E being the composite field I J . (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 ) ) )
fldextrspundgledvds.1 
|- ( ph -> ( I [:] K ) e. NN )
Assertion fldextrspundgdvds 
|- ( ph -> ( I [:] K ) || ( E [:] 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 fldextrspundgledvds.1 
 |-  ( ph -> ( I [:] K ) e. NN )
12 1 2 3 4 5 6 7 8 9 10 11 fldextrspundgdvdslem 
 |-  ( ph -> ( E [:] I ) e. NN0 )
13 12 nn0zd 
 |-  ( ph -> ( E [:] I ) e. ZZ )
14 11 nnzd 
 |-  ( ph -> ( I [:] K ) e. ZZ )
15 eqid 
 |-  ( Base ` L ) = ( Base ` L )
16 4 flddrngd 
 |-  ( ph -> L e. DivRing )
17 15 sdrgss 
 |-  ( G e. ( SubDRing ` L ) -> G C_ ( Base ` L ) )
18 7 17 syl 
 |-  ( ph -> G C_ ( Base ` L ) )
19 15 sdrgss 
 |-  ( H e. ( SubDRing ` L ) -> H C_ ( Base ` L ) )
20 8 19 syl 
 |-  ( ph -> H C_ ( Base ` L ) )
21 18 20 unssd 
 |-  ( ph -> ( G u. H ) C_ ( Base ` L ) )
22 15 16 21 fldgensdrg 
 |-  ( ph -> ( L fldGen ( G u. H ) ) e. ( SubDRing ` L ) )
23 eqid 
 |-  ( RingSpan ` L ) = ( RingSpan ` L )
24 eqid 
 |-  ( ( RingSpan ` L ) ` ( G u. H ) ) = ( ( RingSpan ` L ) ` ( G u. H ) )
25 eqid 
 |-  ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) = ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) )
26 1 2 3 4 5 6 7 8 9 23 24 25 fldextrspunlem2 
 |-  ( ph -> ( ( RingSpan ` L ) ` ( G u. H ) ) = ( L fldGen ( G u. H ) ) )
27 26 oveq2d 
 |-  ( ph -> ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) = ( L |`s ( L fldGen ( G u. H ) ) ) )
28 10 27 eqtr4id 
 |-  ( ph -> E = ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) )
29 1 2 3 4 5 6 7 8 9 23 24 25 fldextrspunfld 
 |-  ( ph -> ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) e. Field )
30 28 29 eqeltrd 
 |-  ( ph -> E e. Field )
31 30 flddrngd 
 |-  ( ph -> E e. DivRing )
32 31 drngringd 
 |-  ( ph -> E e. Ring )
33 10 oveq1i 
 |-  ( E |`s F ) = ( ( L |`s ( L fldGen ( G u. H ) ) ) |`s F )
34 ovexd 
 |-  ( ph -> ( L fldGen ( G u. H ) ) e. _V )
35 eqid 
 |-  ( Base ` I ) = ( Base ` I )
36 35 sdrgss 
 |-  ( F e. ( SubDRing ` I ) -> F C_ ( Base ` I ) )
37 5 36 syl 
 |-  ( ph -> F C_ ( Base ` I ) )
38 2 15 ressbas2 
 |-  ( G C_ ( Base ` L ) -> G = ( Base ` I ) )
39 18 38 syl 
 |-  ( ph -> G = ( Base ` I ) )
40 37 39 sseqtrrd 
 |-  ( ph -> F C_ G )
41 ssun1 
 |-  G C_ ( G u. H )
42 41 a1i 
 |-  ( ph -> G C_ ( G u. H ) )
43 40 42 sstrd 
 |-  ( ph -> F C_ ( G u. H ) )
44 15 16 21 fldgenssid 
 |-  ( ph -> ( G u. H ) C_ ( L fldGen ( G u. H ) ) )
45 43 44 sstrd 
 |-  ( ph -> F C_ ( L fldGen ( G u. H ) ) )
46 ressabs 
 |-  ( ( ( L fldGen ( G u. H ) ) e. _V /\ F C_ ( L fldGen ( G u. H ) ) ) -> ( ( L |`s ( L fldGen ( G u. H ) ) ) |`s F ) = ( L |`s F ) )
47 34 45 46 syl2anc 
 |-  ( ph -> ( ( L |`s ( L fldGen ( G u. H ) ) ) |`s F ) = ( L |`s F ) )
48 33 47 eqtrid 
 |-  ( ph -> ( E |`s F ) = ( L |`s F ) )
49 2 oveq1i 
 |-  ( I |`s F ) = ( ( L |`s G ) |`s F )
50 ressabs 
 |-  ( ( G e. ( SubDRing ` L ) /\ F C_ G ) -> ( ( L |`s G ) |`s F ) = ( L |`s F ) )
51 7 40 50 syl2anc 
 |-  ( ph -> ( ( L |`s G ) |`s F ) = ( L |`s F ) )
52 49 51 eqtrid 
 |-  ( ph -> ( I |`s F ) = ( L |`s F ) )
53 48 52 eqtr4d 
 |-  ( ph -> ( E |`s F ) = ( I |`s F ) )
54 eqid 
 |-  ( I |`s F ) = ( I |`s F )
55 54 sdrgdrng 
 |-  ( F e. ( SubDRing ` I ) -> ( I |`s F ) e. DivRing )
56 5 55 syl 
 |-  ( ph -> ( I |`s F ) e. DivRing )
57 53 56 eqeltrd 
 |-  ( ph -> ( E |`s F ) e. DivRing )
58 57 drngringd 
 |-  ( ph -> ( E |`s F ) e. Ring )
59 15 16 21 fldgenssv 
 |-  ( ph -> ( L fldGen ( G u. H ) ) C_ ( Base ` L ) )
60 10 15 ressbas2 
 |-  ( ( L fldGen ( G u. H ) ) C_ ( Base ` L ) -> ( L fldGen ( G u. H ) ) = ( Base ` E ) )
61 59 60 syl 
 |-  ( ph -> ( L fldGen ( G u. H ) ) = ( Base ` E ) )
62 45 61 sseqtrd 
 |-  ( ph -> F C_ ( Base ` E ) )
63 16 drngringd 
 |-  ( ph -> L e. Ring )
64 42 44 sstrd 
 |-  ( ph -> G C_ ( L fldGen ( G u. H ) ) )
65 sdrgsubrg 
 |-  ( G e. ( SubDRing ` L ) -> G e. ( SubRing ` L ) )
66 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
67 66 subrg1cl 
 |-  ( G e. ( SubRing ` L ) -> ( 1r ` L ) e. G )
68 7 65 67 3syl 
 |-  ( ph -> ( 1r ` L ) e. G )
69 64 68 sseldd 
 |-  ( ph -> ( 1r ` L ) e. ( L fldGen ( G u. H ) ) )
70 10 15 66 ress1r 
 |-  ( ( L e. Ring /\ ( 1r ` L ) e. ( L fldGen ( G u. H ) ) /\ ( L fldGen ( G u. H ) ) C_ ( Base ` L ) ) -> ( 1r ` L ) = ( 1r ` E ) )
71 63 69 59 70 syl3anc 
 |-  ( ph -> ( 1r ` L ) = ( 1r ` E ) )
72 2 15 66 ress1r 
 |-  ( ( L e. Ring /\ ( 1r ` L ) e. G /\ G C_ ( Base ` L ) ) -> ( 1r ` L ) = ( 1r ` I ) )
73 63 68 18 72 syl3anc 
 |-  ( ph -> ( 1r ` L ) = ( 1r ` I ) )
74 71 73 eqtr3d 
 |-  ( ph -> ( 1r ` E ) = ( 1r ` I ) )
75 sdrgsubrg 
 |-  ( F e. ( SubDRing ` I ) -> F e. ( SubRing ` I ) )
76 eqid 
 |-  ( 1r ` I ) = ( 1r ` I )
77 76 subrg1cl 
 |-  ( F e. ( SubRing ` I ) -> ( 1r ` I ) e. F )
78 5 75 77 3syl 
 |-  ( ph -> ( 1r ` I ) e. F )
79 74 78 eqeltrd 
 |-  ( ph -> ( 1r ` E ) e. F )
80 eqid 
 |-  ( Base ` E ) = ( Base ` E )
81 eqid 
 |-  ( 1r ` E ) = ( 1r ` E )
82 80 81 issubrg 
 |-  ( F e. ( SubRing ` E ) <-> ( ( E e. Ring /\ ( E |`s F ) e. Ring ) /\ ( F C_ ( Base ` E ) /\ ( 1r ` E ) e. F ) ) )
83 32 58 62 79 82 syl22anbrc 
 |-  ( ph -> F e. ( SubRing ` E ) )
84 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
85 31 83 57 84 syl3anbrc 
 |-  ( ph -> F e. ( SubDRing ` E ) )
86 10 4 22 85 1 fldsdrgfldext2 
 |-  ( ph -> E /FldExt K )
87 extdgcl 
 |-  ( E /FldExt K -> ( E [:] K ) e. NN0* )
88 86 87 syl 
 |-  ( ph -> ( E [:] K ) e. NN0* )
89 11 nnnn0d 
 |-  ( ph -> ( I [:] K ) e. NN0 )
90 89 9 nn0mulcld 
 |-  ( ph -> ( ( I [:] K ) x. ( J [:] K ) ) e. NN0 )
91 1 2 3 4 5 6 7 8 9 10 fldextrspundglemul 
 |-  ( ph -> ( E [:] K ) <_ ( ( I [:] K ) *e ( J [:] K ) ) )
92 11 nnred 
 |-  ( ph -> ( I [:] K ) e. RR )
93 9 nn0red 
 |-  ( ph -> ( J [:] K ) e. RR )
94 rexmul 
 |-  ( ( ( I [:] K ) e. RR /\ ( J [:] K ) e. RR ) -> ( ( I [:] K ) *e ( J [:] K ) ) = ( ( I [:] K ) x. ( J [:] K ) ) )
95 92 93 94 syl2anc 
 |-  ( ph -> ( ( I [:] K ) *e ( J [:] K ) ) = ( ( I [:] K ) x. ( J [:] K ) ) )
96 91 95 breqtrd 
 |-  ( ph -> ( E [:] K ) <_ ( ( I [:] K ) x. ( J [:] K ) ) )
97 xnn0lenn0nn0 
 |-  ( ( ( E [:] K ) e. NN0* /\ ( ( I [:] K ) x. ( J [:] K ) ) e. NN0 /\ ( E [:] K ) <_ ( ( I [:] K ) x. ( J [:] K ) ) ) -> ( E [:] K ) e. NN0 )
98 88 90 96 97 syl3anc 
 |-  ( ph -> ( E [:] K ) e. NN0 )
99 98 nn0zd 
 |-  ( ph -> ( E [:] K ) e. ZZ )
100 15 2 10 4 7 20 fldgenfldext 
 |-  ( ph -> E /FldExt I )
101 2 4 7 5 1 fldsdrgfldext2 
 |-  ( ph -> I /FldExt K )
102 extdgmul 
 |-  ( ( E /FldExt I /\ I /FldExt K ) -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
103 100 101 102 syl2anc 
 |-  ( ph -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
104 12 nn0red 
 |-  ( ph -> ( E [:] I ) e. RR )
105 rexmul 
 |-  ( ( ( E [:] I ) e. RR /\ ( I [:] K ) e. RR ) -> ( ( E [:] I ) *e ( I [:] K ) ) = ( ( E [:] I ) x. ( I [:] K ) ) )
106 104 92 105 syl2anc 
 |-  ( ph -> ( ( E [:] I ) *e ( I [:] K ) ) = ( ( E [:] I ) x. ( I [:] K ) ) )
107 103 106 eqtr2d 
 |-  ( ph -> ( ( E [:] I ) x. ( I [:] K ) ) = ( E [:] K ) )
108 dvds0lem 
 |-  ( ( ( ( E [:] I ) e. ZZ /\ ( I [:] K ) e. ZZ /\ ( E [:] K ) e. ZZ ) /\ ( ( E [:] I ) x. ( I [:] K ) ) = ( E [:] K ) ) -> ( I [:] K ) || ( E [:] K ) )
109 13 14 99 107 108 syl31anc 
 |-  ( ph -> ( I [:] K ) || ( E [:] K ) )