Metamath Proof Explorer

Theorem fldext2rspun

Description: Given two field extensions I / K and J / K , I / K being a quadratic extension, and the degree of J / K being a power of 2 , the degree of the extension E / K is a power of 2 , 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 ) )
fldext2rspun.n 
|- ( ph -> N e. NN0 )
fldext2rspun.1 
|- ( ph -> ( I [:] K ) = 2 )
fldext2rspun.2 
|- ( ph -> ( J [:] K ) = ( 2 ^ N ) )
fldext2rspun.e 
|- E = ( L |`s ( L fldGen ( G u. H ) ) )
Assertion fldext2rspun 
|- ( ph -> E. n e. NN0 ( E [:] K ) = ( 2 ^ n ) )

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 fldext2rspun.n 
 |-  ( ph -> N e. NN0 )
10 fldext2rspun.1 
 |-  ( ph -> ( I [:] K ) = 2 )
11 fldext2rspun.2 
 |-  ( ph -> ( J [:] K ) = ( 2 ^ N ) )
12 fldext2rspun.e 
 |-  E = ( L |`s ( L fldGen ( G u. H ) ) )
13 eqid 
 |-  ( Base ` L ) = ( Base ` L )
14 13 sdrgss 
 |-  ( H e. ( SubDRing ` L ) -> H C_ ( Base ` L ) )
15 8 14 syl 
 |-  ( ph -> H C_ ( Base ` L ) )
16 13 2 12 4 7 15 fldgenfldext 
 |-  ( ph -> E /FldExt I )
17 2 4 7 5 1 fldsdrgfldext2 
 |-  ( ph -> I /FldExt K )
18 extdgmul 
 |-  ( ( E /FldExt I /\ I /FldExt K ) -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
19 16 17 18 syl2anc 
 |-  ( ph -> ( E [:] K ) = ( ( E [:] I ) *e ( I [:] K ) ) )
20 2nn 
 |-  2 e. NN
21 20 a1i 
 |-  ( ph -> 2 e. NN )
22 21 9 nnexpcld 
 |-  ( ph -> ( 2 ^ N ) e. NN )
23 11 22 eqeltrd 
 |-  ( ph -> ( J [:] K ) e. NN )
24 23 nnnn0d 
 |-  ( ph -> ( J [:] K ) e. NN0 )
25 10 20 eqeltrdi 
 |-  ( ph -> ( I [:] K ) e. NN )
26 1 2 3 4 5 6 7 8 24 12 25 fldextrspundgdvdslem 
 |-  ( ph -> ( E [:] I ) e. NN0 )
27 elnn0 
 |-  ( ( E [:] I ) e. NN0 <-> ( ( E [:] I ) e. NN \/ ( E [:] I ) = 0 ) )
28 26 27 sylib 
 |-  ( ph -> ( ( E [:] I ) e. NN \/ ( E [:] I ) = 0 ) )
29 extdggt0 
 |-  ( E /FldExt I -> 0 < ( E [:] I ) )
30 16 29 syl 
 |-  ( ph -> 0 < ( E [:] I ) )
31 30 gt0ne0d 
 |-  ( ph -> ( E [:] I ) =/= 0 )
32 31 neneqd 
 |-  ( ph -> -. ( E [:] I ) = 0 )
33 28 32 olcnd 
 |-  ( ph -> ( E [:] I ) e. NN )
34 33 nnred 
 |-  ( ph -> ( E [:] I ) e. RR )
35 25 nnred 
 |-  ( ph -> ( I [:] K ) e. RR )
36 rexmul 
 |-  ( ( ( E [:] I ) e. RR /\ ( I [:] K ) e. RR ) -> ( ( E [:] I ) *e ( I [:] K ) ) = ( ( E [:] I ) x. ( I [:] K ) ) )
37 34 35 36 syl2anc 
 |-  ( ph -> ( ( E [:] I ) *e ( I [:] K ) ) = ( ( E [:] I ) x. ( I [:] K ) ) )
38 19 37 eqtrd 
 |-  ( ph -> ( E [:] K ) = ( ( E [:] I ) x. ( I [:] K ) ) )
39 33 25 nnmulcld 
 |-  ( ph -> ( ( E [:] I ) x. ( I [:] K ) ) e. NN )
40 38 39 eqeltrd 
 |-  ( ph -> ( E [:] K ) e. NN )
41 2nn0 
 |-  2 e. NN0
42 10 41 eqeltrdi 
 |-  ( ph -> ( I [:] K ) e. NN0 )
43 uncom 
 |-  ( G u. H ) = ( H u. G )
44 43 oveq2i 
 |-  ( L fldGen ( G u. H ) ) = ( L fldGen ( H u. G ) )
45 44 oveq2i 
 |-  ( L |`s ( L fldGen ( G u. H ) ) ) = ( L |`s ( L fldGen ( H u. G ) ) )
46 12 45 eqtri 
 |-  E = ( L |`s ( L fldGen ( H u. G ) ) )
47 1 3 2 4 6 5 8 7 42 46 23 fldextrspundgdvds 
 |-  ( ph -> ( J [:] K ) || ( E [:] K ) )
48 11 47 eqbrtrrd 
 |-  ( ph -> ( 2 ^ N ) || ( E [:] K ) )
49 1 2 3 4 5 6 7 8 24 12 fldextrspundglemul 
 |-  ( ph -> ( E [:] K ) <_ ( ( I [:] K ) *e ( J [:] K ) ) )
50 23 nnred 
 |-  ( ph -> ( J [:] K ) e. RR )
51 rexmul 
 |-  ( ( ( I [:] K ) e. RR /\ ( J [:] K ) e. RR ) -> ( ( I [:] K ) *e ( J [:] K ) ) = ( ( I [:] K ) x. ( J [:] K ) ) )
52 35 50 51 syl2anc 
 |-  ( ph -> ( ( I [:] K ) *e ( J [:] K ) ) = ( ( I [:] K ) x. ( J [:] K ) ) )
53 10 11 oveq12d 
 |-  ( ph -> ( ( I [:] K ) x. ( J [:] K ) ) = ( 2 x. ( 2 ^ N ) ) )
54 2cnd 
 |-  ( ph -> 2 e. CC )
55 54 9 expcld 
 |-  ( ph -> ( 2 ^ N ) e. CC )
56 54 55 mulcomd 
 |-  ( ph -> ( 2 x. ( 2 ^ N ) ) = ( ( 2 ^ N ) x. 2 ) )
57 54 9 expp1d 
 |-  ( ph -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
58 56 57 eqtr4d 
 |-  ( ph -> ( 2 x. ( 2 ^ N ) ) = ( 2 ^ ( N + 1 ) ) )
59 52 53 58 3eqtrd 
 |-  ( ph -> ( ( I [:] K ) *e ( J [:] K ) ) = ( 2 ^ ( N + 1 ) ) )
60 49 59 breqtrd 
 |-  ( ph -> ( E [:] K ) <_ ( 2 ^ ( N + 1 ) ) )
61 40 9 48 60 2exple2exp 
 |-  ( ph -> E. n e. NN0 ( E [:] K ) = ( 2 ^ n ) )