Metamath Proof Explorer

Theorem fldextrspundgle

Description: Inequality involving the degree of two different field extensions I and J of a same field F . Part of the proof of Proposition 5, Chapter 5, of BourbakiAlg2 p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses fldextrspunfld.k ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
fldextrspunfld.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
fldextrspunfld.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
fldextrspunfld.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
fldextrspunfld.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
fldextrspunfld.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
fldextrspunfld.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspunfld.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspunfld.7 ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ0 )
fldextrspundgle.1 ⊢ 𝐸 = ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
Assertion fldextrspundgle ( 𝜑 → ( 𝐸 [:] 𝐼 ) ≤ ( 𝐽 [:] 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fldextrspunfld.k ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
2 fldextrspunfld.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
3 fldextrspunfld.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
4 fldextrspunfld.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
5 fldextrspunfld.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
6 fldextrspunfld.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
7 fldextrspunfld.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
8 fldextrspunfld.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
9 fldextrspunfld.7 ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ0 )
10 fldextrspundgle.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 extdgval ⊢ ( 𝐸 /FldExt 𝐼 → ( 𝐸 [:] 𝐼 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) ) )
16 14 15 syl ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) ) )
17 eqid ⊢ ( RingSpan ‘ 𝐿 ) = ( RingSpan ‘ 𝐿 )
18 eqid ⊢ ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) = ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) )
19 eqid ⊢ ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) = ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) )
20 1 2 3 4 5 6 7 8 9 17 18 19 fldextrspunlem2 ⊢ ( 𝜑 → ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) = ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
21 20 oveq2d ⊢ ( 𝜑 → ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) = ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ) )
22 21 10 eqtr4di ⊢ ( 𝜑 → ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) = 𝐸 )
23 22 fveq2d ⊢ ( 𝜑 → ( subringAlg ‘ ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ) = ( subringAlg ‘ 𝐸 ) )
24 11 sdrgss ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
25 2 11 ressbas2 ⊢ ( 𝐺 ⊆ ( Base ‘ 𝐿 ) → 𝐺 = ( Base ‘ 𝐼 ) )
26 7 24 25 3syl ⊢ ( 𝜑 → 𝐺 = ( Base ‘ 𝐼 ) )
27 23 26 fveq12d ⊢ ( 𝜑 → ( ( subringAlg ‘ ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ) ‘ 𝐺 ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) )
28 27 fveq2d ⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ) ‘ 𝐺 ) ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) ) )
29 1 2 3 4 5 6 7 8 9 17 18 19 fldextrspunlem1 ⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ) ‘ 𝐺 ) ) ≤ ( 𝐽 [:] 𝐾 ) )
30 28 29 eqbrtrrd ⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) ) ≤ ( 𝐽 [:] 𝐾 ) )
31 16 30 eqbrtrd ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ≤ ( 𝐽 [:] 𝐾 ) )