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 ⊢ K = L ↾ 𝑠 F
fldextrspunfld.i ⊢ I = L ↾ 𝑠 G
fldextrspunfld.j ⊢ J = L ↾ 𝑠 H
fldextrspunfld.2 ⊢ φ → L ∈ Field
fldextrspunfld.3 ⊢ φ → F ∈ SubDRing ⁡ I
fldextrspunfld.4 ⊢ φ → F ∈ SubDRing ⁡ J
fldextrspunfld.5 ⊢ φ → G ∈ SubDRing ⁡ L
fldextrspunfld.6 ⊢ φ → H ∈ SubDRing ⁡ L
fldextrspunfld.7 ⊢ φ → J .:. K ∈ ℕ 0
fldextrspundgle.1 ⊢ E = L ↾ 𝑠 L fldGen G ∪ H
Assertion fldextrspundgle ⊢ φ → E .:. I ≤ J .:. K

Proof

Step Hyp Ref Expression
1 fldextrspunfld.k ⊢ K = L ↾ 𝑠 F
2 fldextrspunfld.i ⊢ I = L ↾ 𝑠 G
3 fldextrspunfld.j ⊢ J = L ↾ 𝑠 H
4 fldextrspunfld.2 ⊢ φ → L ∈ Field
5 fldextrspunfld.3 ⊢ φ → F ∈ SubDRing ⁡ I
6 fldextrspunfld.4 ⊢ φ → F ∈ SubDRing ⁡ J
7 fldextrspunfld.5 ⊢ φ → G ∈ SubDRing ⁡ L
8 fldextrspunfld.6 ⊢ φ → H ∈ SubDRing ⁡ L
9 fldextrspunfld.7 ⊢ φ → J .:. K ∈ ℕ 0
10 fldextrspundgle.1 ⊢ E = L ↾ 𝑠 L fldGen G ∪ H
11 eqid ⊢ Base L = Base L
12 11 sdrgss ⊢ H ∈ SubDRing ⁡ L → H ⊆ Base L
13 8 12 syl ⊢ φ → H ⊆ Base L
14 11 2 10 4 7 13 fldgenfldext ⊢ φ → E /FldExt I
15 extdgval ⊢ E /FldExt I → E .:. I = dim ⁡ subringAlg ⁡ E ⁡ Base I
16 14 15 syl ⊢ φ → E .:. I = dim ⁡ subringAlg ⁡ E ⁡ Base I
17 eqid ⊢ RingSpan ⁡ L = RingSpan ⁡ L
18 eqid ⊢ RingSpan ⁡ L ⁡ G ∪ H = RingSpan ⁡ L ⁡ G ∪ H
19 eqid ⊢ L ↾ 𝑠 RingSpan ⁡ L ⁡ G ∪ H = L ↾ 𝑠 RingSpan ⁡ L ⁡ G ∪ H
20 1 2 3 4 5 6 7 8 9 17 18 19 fldextrspunlem2 ⊢ φ → RingSpan ⁡ L ⁡ G ∪ H = L fldGen G ∪ H
21 20 oveq2d ⊢ φ → L ↾ 𝑠 RingSpan ⁡ L ⁡ G ∪ H = L ↾ 𝑠 L fldGen G ∪ H
22 21 10 eqtr4di ⊢ φ → L ↾ 𝑠 RingSpan ⁡ L ⁡ G ∪ H = E
23 22 fveq2d ⊢ φ → subringAlg ⁡ L ↾ 𝑠 RingSpan ⁡ L ⁡ G ∪ H = subringAlg ⁡ E
24 11 sdrgss ⊢ G ∈ SubDRing ⁡ L → G ⊆ Base L
25 2 11 ressbas2 ⊢ G ⊆ Base L → G = Base I
26 7 24 25 3syl ⊢ φ → G = Base I
27 23 26 fveq12d ⊢ φ → subringAlg ⁡ L ↾ 𝑠 RingSpan ⁡ L ⁡ G ∪ H ⁡ G = subringAlg ⁡ E ⁡ Base I
28 27 fveq2d ⊢ φ → dim ⁡ subringAlg ⁡ L ↾ 𝑠 RingSpan ⁡ L ⁡ G ∪ H ⁡ G = dim ⁡ subringAlg ⁡ E ⁡ Base I
29 1 2 3 4 5 6 7 8 9 17 18 19 fldextrspunlem1 ⊢ φ → dim ⁡ subringAlg ⁡ L ↾ 𝑠 RingSpan ⁡ L ⁡ G ∪ H ⁡ G ≤ J .:. K
30 28 29 eqbrtrrd ⊢ φ → dim ⁡ subringAlg ⁡ E ⁡ Base I ≤ J .:. K
31 16 30 eqbrtrd ⊢ φ → E .:. I ≤ J .:. K