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 ↾_{𝑠} F$
	fldextrspun.i	$⊢ I = L ↾_{𝑠} G$
	fldextrspun.j	$⊢ J = L ↾_{𝑠} H$
	fldextrspun.2	$⊢ φ \to L \in Field$
	fldextrspun.3	$⊢ φ \to F \in SubDRing (I)$
	fldextrspun.4	$⊢ φ \to F \in SubDRing (J)$
	fldextrspun.5	$⊢ φ \to G \in SubDRing (L)$
	fldextrspun.6	$⊢ φ \to H \in SubDRing (L)$
	fldext2rspun.n	$⊢ φ \to N \in ℕ_{0}$
	fldext2rspun.1	$⊢ φ \to I [. : .] K = 2$
	fldext2rspun.2	$⊢ φ \to J [. : .] K = 2^{N}$
	fldext2rspun.e	$⊢ E = L ↾_{𝑠} (L fldGen (G \cup H))$
Assertion	fldext2rspun	$⊢ φ \to \exists n \in ℕ_{0} E [. : .] K = 2^{n}$

Proof

Step	Hyp	Ref	Expression
1		fldextrspun.k	$⊢ K = L ↾_{𝑠} F$
2		fldextrspun.i	$⊢ I = L ↾_{𝑠} G$
3		fldextrspun.j	$⊢ J = L ↾_{𝑠} H$
4		fldextrspun.2	$⊢ φ \to L \in Field$
5		fldextrspun.3	$⊢ φ \to F \in SubDRing (I)$
6		fldextrspun.4	$⊢ φ \to F \in SubDRing (J)$
7		fldextrspun.5	$⊢ φ \to G \in SubDRing (L)$
8		fldextrspun.6	$⊢ φ \to H \in SubDRing (L)$
9		fldext2rspun.n	$⊢ φ \to N \in ℕ_{0}$
10		fldext2rspun.1	$⊢ φ \to I [. : .] K = 2$
11		fldext2rspun.2	$⊢ φ \to J [. : .] K = 2^{N}$
12		fldext2rspun.e	$⊢ E = L ↾_{𝑠} (L fldGen (G \cup H))$
13		eqid	$⊢ {Base}_{L} = {Base}_{L}$
14	13	sdrgss	$⊢ H \in SubDRing (L) \to H \subseteq {Base}_{L}$
15	8 14	syl	$⊢ φ \to H \subseteq {Base}_{L}$
16	13 2 12 4 7 15	fldgenfldext	$⊢ φ \to E /_{FldExt} I$
17	2 4 7 5 1	fldsdrgfldext2	$⊢ φ \to I /_{FldExt} K$
18		extdgmul	$⊢ (E /_{FldExt} I \land I /_{FldExt} K) \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
19	16 17 18	syl2anc	$⊢ φ \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
20		2nn	$⊢ 2 \in ℕ$
21	20	a1i	$⊢ φ \to 2 \in ℕ$
22	21 9	nnexpcld	$⊢ φ \to 2^{N} \in ℕ$
23	11 22	eqeltrd	$⊢ φ \to J [. : .] K \in ℕ$
24	23	nnnn0d	$⊢ φ \to J [. : .] K \in ℕ_{0}$
25	10 20	eqeltrdi	$⊢ φ \to I [. : .] K \in ℕ$
26	1 2 3 4 5 6 7 8 24 12 25	fldextrspundgdvdslem	$⊢ φ \to E [. : .] I \in ℕ_{0}$
27		elnn0	$⊢ E [. : .] I \in ℕ_{0} \leftrightarrow (E [. : .] I \in ℕ \lor E [. : .] I = 0)$
28	26 27	sylib	$⊢ φ \to (E [. : .] I \in ℕ \lor E [. : .] I = 0)$
29		extdggt0	$⊢ E /_{FldExt} I \to 0 < E [. : .] I$
30	16 29	syl	$⊢ φ \to 0 < E [. : .] I$
31	30	gt0ne0d	$⊢ φ \to E [. : .] I \neq 0$
32	31	neneqd	$⊢ φ \to \neg E [. : .] I = 0$
33	28 32	olcnd	$⊢ φ \to E [. : .] I \in ℕ$
34	33	nnred	$⊢ φ \to E [. : .] I \in ℝ$
35	25	nnred	$⊢ φ \to I [. : .] K \in ℝ$
36		rexmul	$⊢ (E [. : .] I \in ℝ \land I [. : .] K \in ℝ) \to [E : I] \cdot_{𝑒} [I : K] = [E : I] [I : K]$
37	34 35 36	syl2anc	$⊢ φ \to [E : I] \cdot_{𝑒} [I : K] = [E : I] [I : K]$
38	19 37	eqtrd	$⊢ φ \to E [. : .] K = [E : I] [I : K]$
39	33 25	nnmulcld	$⊢ φ \to [E : I] [I : K] \in ℕ$
40	38 39	eqeltrd	$⊢ φ \to E [. : .] K \in ℕ$
41		2nn0	$⊢ 2 \in ℕ_{0}$
42	10 41	eqeltrdi	$⊢ φ \to I [. : .] K \in ℕ_{0}$
43		uncom	$⊢ G \cup H = H \cup G$
44	43	oveq2i	$⊢ L fldGen (G \cup H) = L fldGen (H \cup G)$
45	44	oveq2i	$⊢ L ↾_{𝑠} (L fldGen (G \cup H)) = L ↾_{𝑠} (L fldGen (H \cup G))$
46	12 45	eqtri	$⊢ E = L ↾_{𝑠} (L fldGen (H \cup G))$
47	1 3 2 4 6 5 8 7 42 46 23	fldextrspundgdvds	$⊢ φ \to [J : K] ∥ [E : K]$
48	11 47	eqbrtrrd	$⊢ φ \to 2^{N} ∥ [E : K]$
49	1 2 3 4 5 6 7 8 24 12	fldextrspundglemul	$⊢ φ \to E [. : .] K \leq [I : K] \cdot_{𝑒} [J : K]$
50	23	nnred	$⊢ φ \to J [. : .] K \in ℝ$
51		rexmul	$⊢ (I [. : .] K \in ℝ \land J [. : .] K \in ℝ) \to [I : K] \cdot_{𝑒} [J : K] = [I : K] [J : K]$
52	35 50 51	syl2anc	$⊢ φ \to [I : K] \cdot_{𝑒} [J : K] = [I : K] [J : K]$
53	10 11	oveq12d	$⊢ φ \to [I : K] [J : K] = 2 2^{N}$
54		2cnd	$⊢ φ \to 2 \in ℂ$
55	54 9	expcld	$⊢ φ \to 2^{N} \in ℂ$
56	54 55	mulcomd	$⊢ φ \to 2 2^{N} = 2^{N} \cdot 2$
57	54 9	expp1d	$⊢ φ \to 2^{N + 1} = 2^{N} \cdot 2$
58	56 57	eqtr4d	$⊢ φ \to 2 2^{N} = 2^{N + 1}$
59	52 53 58	3eqtrd	$⊢ φ \to [I : K] \cdot_{𝑒} [J : K] = 2^{N + 1}$
60	49 59	breqtrd	$⊢ φ \to E [. : .] K \leq 2^{N + 1}$
61	40 9 48 60	2exple2exp	$⊢ φ \to \exists n \in ℕ_{0} E [. : .] K = 2^{n}$

Metamath Proof Explorer

Theorem fldext2rspun

Proof