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

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		fldextrspundglemul.7	⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ0 )
10		fldextrspundglemul.1	⊢ 𝐸 = ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
11		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
12	11	sdrgss	⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
13	8 12	syl	⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
14	11 2 10 4 7 13	fldgenfldext	⊢ ( 𝜑 → 𝐸 /FldExt 𝐼 )
15		extdgcl	⊢ ( 𝐸 /FldExt 𝐼 → ( 𝐸 [:] 𝐼 ) ∈ ℕ0* )
16		xnn0xr	⊢ ( ( 𝐸 [:] 𝐼 ) ∈ ℕ0* → ( 𝐸 [:] 𝐼 ) ∈ ℝ* )
17	14 15 16	3syl	⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℝ* )
18	3 4 8 6 1	fldsdrgfldext2	⊢ ( 𝜑 → 𝐽 /FldExt 𝐾 )
19		extdgcl	⊢ ( 𝐽 /FldExt 𝐾 → ( 𝐽 [:] 𝐾 ) ∈ ℕ0* )
20		xnn0xr	⊢ ( ( 𝐽 [:] 𝐾 ) ∈ ℕ0* → ( 𝐽 [:] 𝐾 ) ∈ ℝ* )
21	18 19 20	3syl	⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℝ* )
22	2 4 7 5 1	fldsdrgfldext2	⊢ ( 𝜑 → 𝐼 /FldExt 𝐾 )
23		extdgcl	⊢ ( 𝐼 /FldExt 𝐾 → ( 𝐼 [:] 𝐾 ) ∈ ℕ0* )
24		xnn0xrge0	⊢ ( ( 𝐼 [:] 𝐾 ) ∈ ℕ0* → ( 𝐼 [:] 𝐾 ) ∈ ( 0 [,] +∞ ) )
25	22 23 24	3syl	⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ( 0 [,] +∞ ) )
26		elxrge0	⊢ ( ( 𝐼 [:] 𝐾 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐼 [:] 𝐾 ) ∈ ℝ* ∧ 0 ≤ ( 𝐼 [:] 𝐾 ) ) )
27	25 26	sylib	⊢ ( 𝜑 → ( ( 𝐼 [:] 𝐾 ) ∈ ℝ* ∧ 0 ≤ ( 𝐼 [:] 𝐾 ) ) )
28	1 2 3 4 5 6 7 8 9 10	fldextrspundgle	⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ≤ ( 𝐽 [:] 𝐾 ) )
29		xlemul1a	⊢ ( ( ( ( 𝐸 [:] 𝐼 ) ∈ ℝ* ∧ ( 𝐽 [:] 𝐾 ) ∈ ℝ* ∧ ( ( 𝐼 [:] 𝐾 ) ∈ ℝ* ∧ 0 ≤ ( 𝐼 [:] 𝐾 ) ) ) ∧ ( 𝐸 [:] 𝐼 ) ≤ ( 𝐽 [:] 𝐾 ) ) → ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) ≤ ( ( 𝐽 [:] 𝐾 ) ·e ( 𝐼 [:] 𝐾 ) ) )
30	17 21 27 28 29	syl31anc	⊢ ( 𝜑 → ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) ≤ ( ( 𝐽 [:] 𝐾 ) ·e ( 𝐼 [:] 𝐾 ) ) )
31		extdgmul	⊢ ( ( 𝐸 /FldExt 𝐼 ∧ 𝐼 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) )
32	14 22 31	syl2anc	⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) )
33		xnn0xr	⊢ ( ( 𝐼 [:] 𝐾 ) ∈ ℕ0* → ( 𝐼 [:] 𝐾 ) ∈ ℝ* )
34	22 23 33	3syl	⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℝ* )
35		xmulcom	⊢ ( ( ( 𝐼 [:] 𝐾 ) ∈ ℝ* ∧ ( 𝐽 [:] 𝐾 ) ∈ ℝ* ) → ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) = ( ( 𝐽 [:] 𝐾 ) ·e ( 𝐼 [:] 𝐾 ) ) )
36	34 21 35	syl2anc	⊢ ( 𝜑 → ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) = ( ( 𝐽 [:] 𝐾 ) ·e ( 𝐼 [:] 𝐾 ) ) )
37	30 32 36	3brtr4d	⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ≤ ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) )