Metamath Proof Explorer

Theorem fldextrspundgdvdslem

Description: Lemma for fldextrspundgdvds . (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 fldextrspundgdvdslem 
|- ( ph -> ( E [:] I ) e. NN0 )

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 eqid 
 |-  ( Base ` L ) = ( Base ` L )
13 12 sdrgss 
 |-  ( H e. ( SubDRing ` L ) -> H C_ ( Base ` L ) )
14 8 13 syl 
 |-  ( ph -> H C_ ( Base ` L ) )
15 12 2 10 4 7 14 fldgenfldext 
 |-  ( ph -> E /FldExt I )
16 extdgcl 
 |-  ( E /FldExt I -> ( E [:] I ) e. NN0* )
17 15 16 syl 
 |-  ( ph -> ( E [:] I ) e. NN0* )
18 elxnn0 
 |-  ( ( E [:] I ) e. NN0* <-> ( ( E [:] I ) e. NN0 \/ ( E [:] I ) = +oo ) )
19 17 18 sylib 
 |-  ( ph -> ( ( E [:] I ) e. NN0 \/ ( E [:] I ) = +oo ) )
20 2 4 7 5 1 fldsdrgfldext2 
 |-  ( ph -> I /FldExt K )
21 extdgmul 
 |-  ( ( E /FldExt I /\ I /FldExt K ) -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
22 15 20 21 syl2anc 
 |-  ( ph -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
23 22 adantr 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
24 simpr 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> ( E [:] I ) = +oo )
25 24 oveq1d 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> ( ( E [:] I ) *e ( I [:] K ) ) = ( +oo *e ( I [:] K ) ) )
26 11 nnred 
 |-  ( ph -> ( I [:] K ) e. RR )
27 26 rexrd 
 |-  ( ph -> ( I [:] K ) e. RR* )
28 27 adantr 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> ( I [:] K ) e. RR* )
29 11 nngt0d 
 |-  ( ph -> 0 < ( I [:] K ) )
30 29 adantr 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> 0 < ( I [:] K ) )
31 xmulpnf2 
 |-  ( ( ( I [:] K ) e. RR* /\ 0 < ( I [:] K ) ) -> ( +oo *e ( I [:] K ) ) = +oo )
32 28 30 31 syl2anc 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> ( +oo *e ( I [:] K ) ) = +oo )
33 23 25 32 3eqtrd 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> ( E [:] K ) = +oo )
34 4 flddrngd 
 |-  ( ph -> L e. DivRing )
35 12 sdrgss 
 |-  ( G e. ( SubDRing ` L ) -> G C_ ( Base ` L ) )
36 7 35 syl 
 |-  ( ph -> G C_ ( Base ` L ) )
37 36 14 unssd 
 |-  ( ph -> ( G u. H ) C_ ( Base ` L ) )
38 12 34 37 fldgensdrg 
 |-  ( ph -> ( L fldGen ( G u. H ) ) e. ( SubDRing ` L ) )
39 eqid 
 |-  ( RingSpan ` L ) = ( RingSpan ` L )
40 eqid 
 |-  ( ( RingSpan ` L ) ` ( G u. H ) ) = ( ( RingSpan ` L ) ` ( G u. H ) )
41 eqid 
 |-  ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) = ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) )
42 1 2 3 4 5 6 7 8 9 39 40 41 fldextrspunlem2 
 |-  ( ph -> ( ( RingSpan ` L ) ` ( G u. H ) ) = ( L fldGen ( G u. H ) ) )
43 42 oveq2d 
 |-  ( ph -> ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) = ( L |`s ( L fldGen ( G u. H ) ) ) )
44 10 43 eqtr4id 
 |-  ( ph -> E = ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) )
45 1 2 3 4 5 6 7 8 9 39 40 41 fldextrspunfld 
 |-  ( ph -> ( L |`s ( ( RingSpan ` L ) ` ( G u. H ) ) ) e. Field )
46 44 45 eqeltrd 
 |-  ( ph -> E e. Field )
47 46 flddrngd 
 |-  ( ph -> E e. DivRing )
48 47 drngringd 
 |-  ( ph -> E e. Ring )
49 10 oveq1i 
 |-  ( E |`s F ) = ( ( L |`s ( L fldGen ( G u. H ) ) ) |`s F )
50 ovexd 
 |-  ( ph -> ( L fldGen ( G u. H ) ) e. _V )
51 eqid 
 |-  ( Base ` I ) = ( Base ` I )
52 51 sdrgss 
 |-  ( F e. ( SubDRing ` I ) -> F C_ ( Base ` I ) )
53 5 52 syl 
 |-  ( ph -> F C_ ( Base ` I ) )
54 2 12 ressbas2 
 |-  ( G C_ ( Base ` L ) -> G = ( Base ` I ) )
55 36 54 syl 
 |-  ( ph -> G = ( Base ` I ) )
56 53 55 sseqtrrd 
 |-  ( ph -> F C_ G )
57 ssun1 
 |-  G C_ ( G u. H )
58 57 a1i 
 |-  ( ph -> G C_ ( G u. H ) )
59 56 58 sstrd 
 |-  ( ph -> F C_ ( G u. H ) )
60 12 34 37 fldgenssid 
 |-  ( ph -> ( G u. H ) C_ ( L fldGen ( G u. H ) ) )
61 59 60 sstrd 
 |-  ( ph -> F C_ ( L fldGen ( G u. H ) ) )
62 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 ) )
63 50 61 62 syl2anc 
 |-  ( ph -> ( ( L |`s ( L fldGen ( G u. H ) ) ) |`s F ) = ( L |`s F ) )
64 49 63 eqtrid 
 |-  ( ph -> ( E |`s F ) = ( L |`s F ) )
65 2 oveq1i 
 |-  ( I |`s F ) = ( ( L |`s G ) |`s F )
66 ressabs 
 |-  ( ( G e. ( SubDRing ` L ) /\ F C_ G ) -> ( ( L |`s G ) |`s F ) = ( L |`s F ) )
67 7 56 66 syl2anc 
 |-  ( ph -> ( ( L |`s G ) |`s F ) = ( L |`s F ) )
68 65 67 eqtrid 
 |-  ( ph -> ( I |`s F ) = ( L |`s F ) )
69 64 68 eqtr4d 
 |-  ( ph -> ( E |`s F ) = ( I |`s F ) )
70 eqid 
 |-  ( I |`s F ) = ( I |`s F )
71 70 sdrgdrng 
 |-  ( F e. ( SubDRing ` I ) -> ( I |`s F ) e. DivRing )
72 5 71 syl 
 |-  ( ph -> ( I |`s F ) e. DivRing )
73 69 72 eqeltrd 
 |-  ( ph -> ( E |`s F ) e. DivRing )
74 73 drngringd 
 |-  ( ph -> ( E |`s F ) e. Ring )
75 12 34 37 fldgenssv 
 |-  ( ph -> ( L fldGen ( G u. H ) ) C_ ( Base ` L ) )
76 10 12 ressbas2 
 |-  ( ( L fldGen ( G u. H ) ) C_ ( Base ` L ) -> ( L fldGen ( G u. H ) ) = ( Base ` E ) )
77 75 76 syl 
 |-  ( ph -> ( L fldGen ( G u. H ) ) = ( Base ` E ) )
78 61 77 sseqtrd 
 |-  ( ph -> F C_ ( Base ` E ) )
79 34 drngringd 
 |-  ( ph -> L e. Ring )
80 58 60 sstrd 
 |-  ( ph -> G C_ ( L fldGen ( G u. H ) ) )
81 sdrgsubrg 
 |-  ( G e. ( SubDRing ` L ) -> G e. ( SubRing ` L ) )
82 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
83 82 subrg1cl 
 |-  ( G e. ( SubRing ` L ) -> ( 1r ` L ) e. G )
84 7 81 83 3syl 
 |-  ( ph -> ( 1r ` L ) e. G )
85 80 84 sseldd 
 |-  ( ph -> ( 1r ` L ) e. ( L fldGen ( G u. H ) ) )
86 10 12 82 ress1r 
 |-  ( ( L e. Ring /\ ( 1r ` L ) e. ( L fldGen ( G u. H ) ) /\ ( L fldGen ( G u. H ) ) C_ ( Base ` L ) ) -> ( 1r ` L ) = ( 1r ` E ) )
87 79 85 75 86 syl3anc 
 |-  ( ph -> ( 1r ` L ) = ( 1r ` E ) )
88 2 12 82 ress1r 
 |-  ( ( L e. Ring /\ ( 1r ` L ) e. G /\ G C_ ( Base ` L ) ) -> ( 1r ` L ) = ( 1r ` I ) )
89 79 84 36 88 syl3anc 
 |-  ( ph -> ( 1r ` L ) = ( 1r ` I ) )
90 87 89 eqtr3d 
 |-  ( ph -> ( 1r ` E ) = ( 1r ` I ) )
91 sdrgsubrg 
 |-  ( F e. ( SubDRing ` I ) -> F e. ( SubRing ` I ) )
92 eqid 
 |-  ( 1r ` I ) = ( 1r ` I )
93 92 subrg1cl 
 |-  ( F e. ( SubRing ` I ) -> ( 1r ` I ) e. F )
94 5 91 93 3syl 
 |-  ( ph -> ( 1r ` I ) e. F )
95 90 94 eqeltrd 
 |-  ( ph -> ( 1r ` E ) e. F )
96 eqid 
 |-  ( Base ` E ) = ( Base ` E )
97 eqid 
 |-  ( 1r ` E ) = ( 1r ` E )
98 96 97 issubrg 
 |-  ( F e. ( SubRing ` E ) <-> ( ( E e. Ring /\ ( E |`s F ) e. Ring ) /\ ( F C_ ( Base ` E ) /\ ( 1r ` E ) e. F ) ) )
99 48 74 78 95 98 syl22anbrc 
 |-  ( ph -> F e. ( SubRing ` E ) )
100 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
101 47 99 73 100 syl3anbrc 
 |-  ( ph -> F e. ( SubDRing ` E ) )
102 10 4 38 101 1 fldsdrgfldext2 
 |-  ( ph -> E /FldExt K )
103 extdgcl 
 |-  ( E /FldExt K -> ( E [:] K ) e. NN0* )
104 102 103 syl 
 |-  ( ph -> ( E [:] K ) e. NN0* )
105 11 nnnn0d 
 |-  ( ph -> ( I [:] K ) e. NN0 )
106 105 9 nn0mulcld 
 |-  ( ph -> ( ( I [:] K ) x. ( J [:] K ) ) e. NN0 )
107 1 2 3 4 5 6 7 8 9 10 fldextrspundglemul 
 |-  ( ph -> ( E [:] K ) <_ ( ( I [:] K ) *e ( J [:] K ) ) )
108 9 nn0red 
 |-  ( ph -> ( J [:] K ) e. RR )
109 rexmul 
 |-  ( ( ( I [:] K ) e. RR /\ ( J [:] K ) e. RR ) -> ( ( I [:] K ) *e ( J [:] K ) ) = ( ( I [:] K ) x. ( J [:] K ) ) )
110 26 108 109 syl2anc 
 |-  ( ph -> ( ( I [:] K ) *e ( J [:] K ) ) = ( ( I [:] K ) x. ( J [:] K ) ) )
111 107 110 breqtrd 
 |-  ( ph -> ( E [:] K ) <_ ( ( I [:] K ) x. ( J [:] K ) ) )
112 xnn0lenn0nn0 
 |-  ( ( ( E [:] K ) e. NN0* /\ ( ( I [:] K ) x. ( J [:] K ) ) e. NN0 /\ ( E [:] K ) <_ ( ( I [:] K ) x. ( J [:] K ) ) ) -> ( E [:] K ) e. NN0 )
113 104 106 111 112 syl3anc 
 |-  ( ph -> ( E [:] K ) e. NN0 )
114 113 nn0red 
 |-  ( ph -> ( E [:] K ) e. RR )
115 114 adantr 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> ( E [:] K ) e. RR )
116 115 renepnfd 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> ( E [:] K ) =/= +oo )
117 116 neneqd 
 |-  ( ( ph /\ ( E [:] I ) = +oo ) -> -. ( E [:] K ) = +oo )
118 33 117 pm2.65da 
 |-  ( ph -> -. ( E [:] I ) = +oo )
119 19 118 olcnd 
 |-  ( ph -> ( E [:] I ) e. NN0 )