This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐽 [:] 𝐾 ) ) )