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	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	fldext2rspun.1	⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) = 2 )
	fldext2rspun.2	⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) = ( 2 ↑ 𝑁 ) )
	fldext2rspun.e	⊢ 𝐸 = ( 𝐿 ↾_s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
Assertion	fldext2rspun	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ₀ ( 𝐸 [:] 𝐾 ) = ( 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	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
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	⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ₀ )
25	10 20	eqeltrdi	⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℕ )
26	1 2 3 4 5 6 7 8 24 12 25	fldextrspundgdvdslem	⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℕ₀ )
27		elnn0	⊢ ( ( 𝐸 [:] 𝐼 ) ∈ ℕ₀ ↔ ( ( 𝐸 [:] 𝐼 ) ∈ ℕ ∨ ( 𝐸 [:] 𝐼 ) = 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 ∈ ℕ₀
42	10 41	eqeltrdi	⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℕ₀ )
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	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ₀ ( 𝐸 [:] 𝐾 ) = ( 2 ↑ 𝑛 ) )

Metamath Proof Explorer

Theorem fldext2rspun

Proof