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 ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
fldextrspun.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
fldextrspun.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
fldextrspun.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
fldextrspun.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
fldextrspun.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
fldextrspun.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspun.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
fldext2rspun.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
fldext2rspun.1 ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) = 2 )
fldext2rspun.2 ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) = ( 2 ↑ 𝑁 ) )
fldext2rspun.e ⊢ 𝐸 = ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
Assertion fldext2rspun ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( 𝐸 [:] 𝐾 ) = ( 2 ↑ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 fldextrspun.k ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
2 fldextrspun.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
3 fldextrspun.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
4 fldextrspun.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
5 fldextrspun.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
6 fldextrspun.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
7 fldextrspun.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
8 fldextrspun.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
9 fldext2rspun.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
10 fldext2rspun.1 ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) = 2 )
11 fldext2rspun.2 ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) = ( 2 ↑ 𝑁 ) )
12 fldext2rspun.e ⊢ 𝐸 = ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
13 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
14 13 sdrgss ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
15 8 14 syl ⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
16 13 2 12 4 7 15 fldgenfldext ⊢ ( 𝜑 → 𝐸 /FldExt 𝐼 )
17 2 4 7 5 1 fldsdrgfldext2 ⊢ ( 𝜑 → 𝐼 /FldExt 𝐾 )
18 extdgmul ⊢ ( ( 𝐸 /FldExt 𝐼 ∧ 𝐼 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) )
19 16 17 18 syl2anc ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) )
20 2nn ⊢ 2 ∈ ℕ
21 20 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
22 21 9 nnexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ )
23 11 22 eqeltrd ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ )
24 23 nnnn0d ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ0 )
25 10 20 eqeltrdi ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℕ )
26 1 2 3 4 5 6 7 8 24 12 25 fldextrspundgdvdslem ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℕ0 )
27 elnn0 ⊢ ( ( 𝐸 [:] 𝐼 ) ∈ ℕ0 ↔ ( ( 𝐸 [:] 𝐼 ) ∈ ℕ ∨ ( 𝐸 [:] 𝐼 ) = 0 ) )
28 26 27 sylib ⊢ ( 𝜑 → ( ( 𝐸 [:] 𝐼 ) ∈ ℕ ∨ ( 𝐸 [:] 𝐼 ) = 0 ) )
29 extdggt0 ⊢ ( 𝐸 /FldExt 𝐼 → 0 < ( 𝐸 [:] 𝐼 ) )
30 16 29 syl ⊢ ( 𝜑 → 0 < ( 𝐸 [:] 𝐼 ) )
31 30 gt0ne0d ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ≠ 0 )
32 31 neneqd ⊢ ( 𝜑 → ¬ ( 𝐸 [:] 𝐼 ) = 0 )
33 28 32 olcnd ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℕ )
34 33 nnred ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℝ )
35 25 nnred ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℝ )
36 rexmul ⊢ ( ( ( 𝐸 [:] 𝐼 ) ∈ ℝ ∧ ( 𝐼 [:] 𝐾 ) ∈ ℝ ) → ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) = ( ( 𝐸 [:] 𝐼 ) · ( 𝐼 [:] 𝐾 ) ) )
37 34 35 36 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) = ( ( 𝐸 [:] 𝐼 ) · ( 𝐼 [:] 𝐾 ) ) )
38 19 37 eqtrd ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐼 ) · ( 𝐼 [:] 𝐾 ) ) )
39 33 25 nnmulcld ⊢ ( 𝜑 → ( ( 𝐸 [:] 𝐼 ) · ( 𝐼 [:] 𝐾 ) ) ∈ ℕ )
40 38 39 eqeltrd ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ∈ ℕ )
41 2nn0 ⊢ 2 ∈ ℕ0
42 10 41 eqeltrdi ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℕ0 )
43 uncom ⊢ ( 𝐺 ∪ 𝐻 ) = ( 𝐻 ∪ 𝐺 )
44 43 oveq2i ⊢ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) = ( 𝐿 fldGen ( 𝐻 ∪ 𝐺 ) )
45 44 oveq2i ⊢ ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ) = ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐻 ∪ 𝐺 ) ) )
46 12 45 eqtri ⊢ 𝐸 = ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐻 ∪ 𝐺 ) ) )
47 1 3 2 4 6 5 8 7 42 46 23 fldextrspundgdvds ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∥ ( 𝐸 [:] 𝐾 ) )
48 11 47 eqbrtrrd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ ( 𝐸 [:] 𝐾 ) )
49 1 2 3 4 5 6 7 8 24 12 fldextrspundglemul ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ≤ ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) )
50 23 nnred ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℝ )
51 rexmul ⊢ ( ( ( 𝐼 [:] 𝐾 ) ∈ ℝ ∧ ( 𝐽 [:] 𝐾 ) ∈ ℝ ) → ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) = ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) )
52 35 50 51 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) = ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) )
53 10 11 oveq12d ⊢ ( 𝜑 → ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) = ( 2 · ( 2 ↑ 𝑁 ) ) )
54 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
55 54 9 expcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℂ )
56 54 55 mulcomd ⊢ ( 𝜑 → ( 2 · ( 2 ↑ 𝑁 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
57 54 9 expp1d ⊢ ( 𝜑 → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
58 56 57 eqtr4d ⊢ ( 𝜑 → ( 2 · ( 2 ↑ 𝑁 ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
59 52 53 58 3eqtrd ⊢ ( 𝜑 → ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
60 49 59 breqtrd ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ≤ ( 2 ↑ ( 𝑁 + 1 ) ) )
61 40 9 48 60 2exple2exp ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( 𝐸 [:] 𝐾 ) = ( 2 ↑ 𝑛 ) )