Metamath Proof Explorer

Theorem fldextrspundgdvdslem

Description: Lemma for fldextrspundgdvds . (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 fldextrspundgdvdslem ( 𝜑 → ( 𝐸 [:] 𝐼 ) ∈ ℕ0 )

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