Metamath Proof Explorer

Theorem fldextrspundgdvds

Description: Given two finite extensions I / K and J / K of the same field K , the degree of the extension I / K divides the degree of the extension E / K , E being the composite field I J . (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 ( 𝐺 ∪ 𝐻 ) ) )
fldextrspundgledvds.1 ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℕ )
Assertion fldextrspundgdvds ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∥ ( 𝐸 [:] 𝐾 ) )

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 fldextrspundgledvds.1 ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℕ )
12 1 2 3 4 5 6 7 8 9 10 11 fldextrspundgdvdslem ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℕ0 )
13 12 nn0zd ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℤ )
14 11 nnzd ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℤ )
15 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
16 4 flddrngd ⊢ ( 𝜑 → 𝐿 ∈ DivRing )
17 15 sdrgss ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
18 7 17 syl ⊢ ( 𝜑 → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
19 15 sdrgss ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
20 8 19 syl ⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
21 18 20 unssd ⊢ ( 𝜑 → ( 𝐺 ∪ 𝐻 ) ⊆ ( Base ‘ 𝐿 ) )
22 15 16 21 fldgensdrg ⊢ ( 𝜑 → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ∈ ( SubDRing ‘ 𝐿 ) )
23 eqid ⊢ ( RingSpan ‘ 𝐿 ) = ( RingSpan ‘ 𝐿 )
24 eqid ⊢ ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) = ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) )
25 eqid ⊢ ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) = ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) )
26 1 2 3 4 5 6 7 8 9 23 24 25 fldextrspunlem2 ⊢ ( 𝜑 → ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) = ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
27 26 oveq2d ⊢ ( 𝜑 → ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) = ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ) )
28 10 27 eqtr4id ⊢ ( 𝜑 → 𝐸 = ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) )
29 1 2 3 4 5 6 7 8 9 23 24 25 fldextrspunfld ⊢ ( 𝜑 → ( 𝐿 ↾s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ∈ Field )
30 28 29 eqeltrd ⊢ ( 𝜑 → 𝐸 ∈ Field )
31 30 flddrngd ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
32 31 drngringd ⊢ ( 𝜑 → 𝐸 ∈ Ring )
33 10 oveq1i ⊢ ( 𝐸 ↾s 𝐹 ) = ( ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ) ↾s 𝐹 )
34 ovexd ⊢ ( 𝜑 → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ∈ V )
35 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
36 35 sdrgss ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐼 ) → 𝐹 ⊆ ( Base ‘ 𝐼 ) )
37 5 36 syl ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐼 ) )
38 2 15 ressbas2 ⊢ ( 𝐺 ⊆ ( Base ‘ 𝐿 ) → 𝐺 = ( Base ‘ 𝐼 ) )
39 18 38 syl ⊢ ( 𝜑 → 𝐺 = ( Base ‘ 𝐼 ) )
40 37 39 sseqtrrd ⊢ ( 𝜑 → 𝐹 ⊆ 𝐺 )
41 ssun1 ⊢ 𝐺 ⊆ ( 𝐺 ∪ 𝐻 )
42 41 a1i ⊢ ( 𝜑 → 𝐺 ⊆ ( 𝐺 ∪ 𝐻 ) )
43 40 42 sstrd ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝐺 ∪ 𝐻 ) )
44 15 16 21 fldgenssid ⊢ ( 𝜑 → ( 𝐺 ∪ 𝐻 ) ⊆ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
45 43 44 sstrd ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
46 ressabs ⊢ ( ( ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ∈ V ∧ 𝐹 ⊆ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ) → ( ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ) ↾s 𝐹 ) = ( 𝐿 ↾s 𝐹 ) )
47 34 45 46 syl2anc ⊢ ( 𝜑 → ( ( 𝐿 ↾s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ) ↾s 𝐹 ) = ( 𝐿 ↾s 𝐹 ) )
48 33 47 eqtrid ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) = ( 𝐿 ↾s 𝐹 ) )
49 2 oveq1i ⊢ ( 𝐼 ↾s 𝐹 ) = ( ( 𝐿 ↾s 𝐺 ) ↾s 𝐹 )
50 ressabs ⊢ ( ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) ∧ 𝐹 ⊆ 𝐺 ) → ( ( 𝐿 ↾s 𝐺 ) ↾s 𝐹 ) = ( 𝐿 ↾s 𝐹 ) )
51 7 40 50 syl2anc ⊢ ( 𝜑 → ( ( 𝐿 ↾s 𝐺 ) ↾s 𝐹 ) = ( 𝐿 ↾s 𝐹 ) )
52 49 51 eqtrid ⊢ ( 𝜑 → ( 𝐼 ↾s 𝐹 ) = ( 𝐿 ↾s 𝐹 ) )
53 48 52 eqtr4d ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) = ( 𝐼 ↾s 𝐹 ) )
54 eqid ⊢ ( 𝐼 ↾s 𝐹 ) = ( 𝐼 ↾s 𝐹 )
55 54 sdrgdrng ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐼 ) → ( 𝐼 ↾s 𝐹 ) ∈ DivRing )
56 5 55 syl ⊢ ( 𝜑 → ( 𝐼 ↾s 𝐹 ) ∈ DivRing )
57 53 56 eqeltrd ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
58 57 drngringd ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Ring )
59 15 16 21 fldgenssv ⊢ ( 𝜑 → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ⊆ ( Base ‘ 𝐿 ) )
60 10 15 ressbas2 ⊢ ( ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ⊆ ( Base ‘ 𝐿 ) → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) = ( Base ‘ 𝐸 ) )
61 59 60 syl ⊢ ( 𝜑 → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) = ( Base ‘ 𝐸 ) )
62 45 61 sseqtrd ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
63 16 drngringd ⊢ ( 𝜑 → 𝐿 ∈ Ring )
64 42 44 sstrd ⊢ ( 𝜑 → 𝐺 ⊆ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
65 sdrgsubrg ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ∈ ( SubRing ‘ 𝐿 ) )
66 eqid ⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 )
67 66 subrg1cl ⊢ ( 𝐺 ∈ ( SubRing ‘ 𝐿 ) → ( 1r ‘ 𝐿 ) ∈ 𝐺 )
68 7 65 67 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝐿 ) ∈ 𝐺 )
69 64 68 sseldd ⊢ ( 𝜑 → ( 1r ‘ 𝐿 ) ∈ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
70 10 15 66 ress1r ⊢ ( ( 𝐿 ∈ Ring ∧ ( 1r ‘ 𝐿 ) ∈ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ⊆ ( Base ‘ 𝐿 ) ) → ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐸 ) )
71 63 69 59 70 syl3anc ⊢ ( 𝜑 → ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐸 ) )
72 2 15 66 ress1r ⊢ ( ( 𝐿 ∈ Ring ∧ ( 1r ‘ 𝐿 ) ∈ 𝐺 ∧ 𝐺 ⊆ ( Base ‘ 𝐿 ) ) → ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐼 ) )
73 63 68 18 72 syl3anc ⊢ ( 𝜑 → ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐼 ) )
74 71 73 eqtr3d ⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐼 ) )
75 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐼 ) → 𝐹 ∈ ( SubRing ‘ 𝐼 ) )
76 eqid ⊢ ( 1r ‘ 𝐼 ) = ( 1r ‘ 𝐼 )
77 76 subrg1cl ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐼 ) → ( 1r ‘ 𝐼 ) ∈ 𝐹 )
78 5 75 77 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝐼 ) ∈ 𝐹 )
79 74 78 eqeltrd ⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) ∈ 𝐹 )
80 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
81 eqid ⊢ ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐸 )
82 80 81 issubrg ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) ↔ ( ( 𝐸 ∈ Ring ∧ ( 𝐸 ↾s 𝐹 ) ∈ Ring ) ∧ ( 𝐹 ⊆ ( Base ‘ 𝐸 ) ∧ ( 1r ‘ 𝐸 ) ∈ 𝐹 ) ) )
83 32 58 62 79 82 syl22anbrc ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
84 issdrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
85 31 83 57 84 syl3anbrc ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
86 10 4 22 85 1 fldsdrgfldext2 ⊢ ( 𝜑 → 𝐸 /FldExt 𝐾 )
87 extdgcl ⊢ ( 𝐸 /FldExt 𝐾 → ( 𝐸 [:] 𝐾 ) ∈ ℕ0* )
88 86 87 syl ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ∈ ℕ0* )
89 11 nnnn0d ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℕ0 )
90 89 9 nn0mulcld ⊢ ( 𝜑 → ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) ∈ ℕ0 )
91 1 2 3 4 5 6 7 8 9 10 fldextrspundglemul ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ≤ ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) )
92 11 nnred ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∈ ℝ )
93 9 nn0red ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℝ )
94 rexmul ⊢ ( ( ( 𝐼 [:] 𝐾 ) ∈ ℝ ∧ ( 𝐽 [:] 𝐾 ) ∈ ℝ ) → ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) = ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) )
95 92 93 94 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 [:] 𝐾 ) ·e ( 𝐽 [:] 𝐾 ) ) = ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) )
96 91 95 breqtrd ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ≤ ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) )
97 xnn0lenn0nn0 ⊢ ( ( ( 𝐸 [:] 𝐾 ) ∈ ℕ0* ∧ ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) ∈ ℕ0 ∧ ( 𝐸 [:] 𝐾 ) ≤ ( ( 𝐼 [:] 𝐾 ) · ( 𝐽 [:] 𝐾 ) ) ) → ( 𝐸 [:] 𝐾 ) ∈ ℕ0 )
98 88 90 96 97 syl3anc ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ∈ ℕ0 )
99 98 nn0zd ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) ∈ ℤ )
100 15 2 10 4 7 20 fldgenfldext ⊢ ( 𝜑 → 𝐸 /FldExt 𝐼 )
101 2 4 7 5 1 fldsdrgfldext2 ⊢ ( 𝜑 → 𝐼 /FldExt 𝐾 )
102 extdgmul ⊢ ( ( 𝐸 /FldExt 𝐼 ∧ 𝐼 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) )
103 100 101 102 syl2anc ⊢ ( 𝜑 → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) )
104 12 nn0red ⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℝ )
105 rexmul ⊢ ( ( ( 𝐸 [:] 𝐼 ) ∈ ℝ ∧ ( 𝐼 [:] 𝐾 ) ∈ ℝ ) → ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) = ( ( 𝐸 [:] 𝐼 ) · ( 𝐼 [:] 𝐾 ) ) )
106 104 92 105 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 [:] 𝐼 ) ·e ( 𝐼 [:] 𝐾 ) ) = ( ( 𝐸 [:] 𝐼 ) · ( 𝐼 [:] 𝐾 ) ) )
107 103 106 eqtr2d ⊢ ( 𝜑 → ( ( 𝐸 [:] 𝐼 ) · ( 𝐼 [:] 𝐾 ) ) = ( 𝐸 [:] 𝐾 ) )
108 dvds0lem ⊢ ( ( ( ( 𝐸 [:] 𝐼 ) ∈ ℤ ∧ ( 𝐼 [:] 𝐾 ) ∈ ℤ ∧ ( 𝐸 [:] 𝐾 ) ∈ ℤ ) ∧ ( ( 𝐸 [:] 𝐼 ) · ( 𝐼 [:] 𝐾 ) ) = ( 𝐸 [:] 𝐾 ) ) → ( 𝐼 [:] 𝐾 ) ∥ ( 𝐸 [:] 𝐾 ) )
109 13 14 99 107 108 syl31anc ⊢ ( 𝜑 → ( 𝐼 [:] 𝐾 ) ∥ ( 𝐸 [:] 𝐾 ) )