fldextrspundglemul

Description: Given two field extensions I / K and J / K of the same field K , J / K being finite, and the composiste field E = I J , the degree of the extension of the composite field E / K is at most the product of the field extension degrees of I / K and J / K . (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)$
	fldextrspundglemul.7	$⊢ φ \to J [. : .] K \in ℕ_{0}$
	fldextrspundglemul.1	$⊢ E = L ↾_{𝑠} (L fldGen (G \cup H))$
Assertion	fldextrspundglemul	$⊢ φ \to E [. : .] K \leq [I : K] \cdot_{𝑒} [J : K]$

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		fldextrspundglemul.7	$⊢ φ \to J [. : .] K \in ℕ_{0}$
10		fldextrspundglemul.1	$⊢ E = L ↾_{𝑠} (L fldGen (G \cup H))$
11		eqid	$⊢ {Base}_{L} = {Base}_{L}$
12	11	sdrgss	$⊢ H \in SubDRing (L) \to H \subseteq {Base}_{L}$
13	8 12	syl	$⊢ φ \to H \subseteq {Base}_{L}$
14	11 2 10 4 7 13	fldgenfldext	$⊢ φ \to E /_{FldExt} I$
15		extdgcl	$⊢ E /_{FldExt} I \to E [. : .] I \in ℕ_{0}^{*}$
16		xnn0xr	$⊢ E [. : .] I \in ℕ_{0}^{} \to E [. : .] I \in ℝ^{}$
17	14 15 16	3syl	$⊢ φ \to E [. : .] I \in ℝ^{*}$
18	3 4 8 6 1	fldsdrgfldext2	$⊢ φ \to J /_{FldExt} K$
19		extdgcl	$⊢ J /_{FldExt} K \to J [. : .] K \in ℕ_{0}^{*}$
20		xnn0xr	$⊢ J [. : .] K \in ℕ_{0}^{} \to J [. : .] K \in ℝ^{}$
21	18 19 20	3syl	$⊢ φ \to J [. : .] K \in ℝ^{*}$
22	2 4 7 5 1	fldsdrgfldext2	$⊢ φ \to I /_{FldExt} K$
23		extdgcl	$⊢ I /_{FldExt} K \to I [. : .] K \in ℕ_{0}^{*}$
24		xnn0xrge0	$⊢ I [. : .] K \in ℕ_{0}^{*} \to I [. : .] K \in [0, +∞]$
25	22 23 24	3syl	$⊢ φ \to I [. : .] K \in [0, +∞]$
26		elxrge0	$⊢ I [. : .] K \in [0, +∞] \leftrightarrow (I [. : .] K \in ℝ^{*} \land 0 \leq I [. : .] K)$
27	25 26	sylib	$⊢ φ \to (I [. : .] K \in ℝ^{*} \land 0 \leq I [. : .] K)$
28	1 2 3 4 5 6 7 8 9 10	fldextrspundgle	$⊢ φ \to E [. : .] I \leq J [. : .] K$
29		xlemul1a	$⊢ ((E [. : .] I \in ℝ^{} \land J [. : .] K \in ℝ^{} \land (I [. : .] K \in ℝ^{*} \land 0 \leq I [. : .] K)) \land E [. : .] I \leq J [. : .] K) \to [E : I] \cdot_{𝑒} [I : K] \leq [J : K] \cdot_{𝑒} [I : K]$
30	17 21 27 28 29	syl31anc	$⊢ φ \to [E : I] \cdot_{𝑒} [I : K] \leq [J : K] \cdot_{𝑒} [I : K]$
31		extdgmul	$⊢ (E /_{FldExt} I \land I /_{FldExt} K) \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
32	14 22 31	syl2anc	$⊢ φ \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
33		xnn0xr	$⊢ I [. : .] K \in ℕ_{0}^{} \to I [. : .] K \in ℝ^{}$
34	22 23 33	3syl	$⊢ φ \to I [. : .] K \in ℝ^{*}$
35		xmulcom	$⊢ (I [. : .] K \in ℝ^{} \land J [. : .] K \in ℝ^{}) \to [I : K] \cdot_{𝑒} [J : K] = [J : K] \cdot_{𝑒} [I : K]$
36	34 21 35	syl2anc	$⊢ φ \to [I : K] \cdot_{𝑒} [J : K] = [J : K] \cdot_{𝑒} [I : K]$
37	30 32 36	3brtr4d	$⊢ φ \to E [. : .] K \leq [I : K] \cdot_{𝑒} [J : K]$

Metamath Proof Explorer

Theorem fldextrspundglemul

Proof