Proof of Theorem aks6d1c6lem1
| Step | Hyp | Ref
| Expression |
| 1 | | aks6d1c6.10 |
. . . . 5
⊢ 𝐺 = (𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))) |
| 3 | 2 | fveq1d 6908 |
. . 3
⊢ (𝜑 → (𝐺‘𝑈) = ((𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘𝑈)) |
| 4 | 3 | fveq2d 6910 |
. 2
⊢ (𝜑 →
((deg1‘𝐾)‘(𝐺‘𝑈)) = ((deg1‘𝐾)‘((𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘𝑈))) |
| 5 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) = (𝑔
∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))) |
| 6 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 = 𝑈) ∧ 𝑖 ∈ (0...𝐴)) → 𝑔 = 𝑈) |
| 7 | 6 | fveq1d 6908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 = 𝑈) ∧ 𝑖 ∈ (0...𝐴)) → (𝑔‘𝑖) = (𝑈‘𝑖)) |
| 8 | 7 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 = 𝑈) ∧ 𝑖 ∈ (0...𝐴)) → ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))) |
| 9 | 8 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = 𝑈) → (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖
∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))) |
| 10 | 9 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝑈) →
((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))) = ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) |
| 11 | | aks6d1c6lem1.1 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ (ℕ0
↑m (0...𝐴))) |
| 12 | | ovexd 7466 |
. . . . 5
⊢ (𝜑 →
((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))) ∈ V) |
| 13 | 5, 10, 11, 12 | fvmptd 7023 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘𝑈) = ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) |
| 14 | 13 | fveq2d 6910 |
. . 3
⊢ (𝜑 →
((deg1‘𝐾)‘((𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘𝑈)) = ((deg1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))) |
| 15 | | aks6d1c6.3 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Field) |
| 16 | | fldidom 20771 |
. . . . . . 7
⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn) |
| 17 | 15, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ IDomn) |
| 18 | | fzfid 14014 |
. . . . . 6
⊢ (𝜑 → (0...𝐴) ∈ Fin) |
| 19 | | eqid 2737 |
. . . . . . . . . 10
⊢
(mulGrp‘(Poly1‘𝐾)) =
(mulGrp‘(Poly1‘𝐾)) |
| 20 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(Poly1‘𝐾)) =
(Base‘(Poly1‘𝐾)) |
| 21 | 19, 20 | mgpbas 20142 |
. . . . . . . . 9
⊢
(Base‘(Poly1‘𝐾)) =
(Base‘(mulGrp‘(Poly1‘𝐾))) |
| 22 | | eqid 2737 |
. . . . . . . . 9
⊢
(.g‘(mulGrp‘(Poly1‘𝐾))) =
(.g‘(mulGrp‘(Poly1‘𝐾))) |
| 23 | 15 | fldcrngd 20742 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ CRing) |
| 24 | | crngring 20242 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ Ring) |
| 26 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Poly1‘𝐾) = (Poly1‘𝐾) |
| 27 | 26 | ply1ring 22249 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ Ring →
(Poly1‘𝐾)
∈ Ring) |
| 28 | 25, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Poly1‘𝐾)
∈ Ring) |
| 29 | 19 | ringmgp 20236 |
. . . . . . . . . . 11
⊢
((Poly1‘𝐾) ∈ Ring →
(mulGrp‘(Poly1‘𝐾)) ∈ Mnd) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(mulGrp‘(Poly1‘𝐾)) ∈ Mnd) |
| 31 | 30 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) →
(mulGrp‘(Poly1‘𝐾)) ∈ Mnd) |
| 32 | | nn0ex 12532 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V |
| 33 | 32 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ0 ∈
V) |
| 34 | | ovexd 7466 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0...𝐴) ∈ V) |
| 35 | 33, 34 | elmapd 8880 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ∈ (ℕ0
↑m (0...𝐴))
↔ 𝑈:(0...𝐴)⟶ℕ0)) |
| 36 | 11, 35 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈:(0...𝐴)⟶ℕ0) |
| 37 | 36 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → 𝑈:(0...𝐴)⟶ℕ0) |
| 38 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → 𝑖 ∈ (0...𝐴)) |
| 39 | 37, 38 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝑈‘𝑖) ∈
ℕ0) |
| 40 | | 2fveq3 6911 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑖 →
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)) =
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) |
| 41 | 40 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑖 → ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) = ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) |
| 42 | 41 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑖 → (((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ∈ (Base‘(Poly1‘𝐾)) ↔ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ∈ (Base‘(Poly1‘𝐾)))) |
| 43 | | ringmnd 20240 |
. . . . . . . . . . . . . . 15
⊢
((Poly1‘𝐾) ∈ Ring →
(Poly1‘𝐾)
∈ Mnd) |
| 44 | 28, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Poly1‘𝐾)
∈ Mnd) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → (Poly1‘𝐾) ∈ Mnd) |
| 46 | 25 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 𝐾 ∈ Ring) |
| 47 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(var1‘𝐾) = (var1‘𝐾) |
| 48 | 47, 26, 20 | vr1cl 22219 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ Ring →
(var1‘𝐾)
∈ (Base‘(Poly1‘𝐾))) |
| 49 | 46, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → (var1‘𝐾) ∈
(Base‘(Poly1‘𝐾))) |
| 50 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℤRHom‘𝐾) = (ℤRHom‘𝐾) |
| 51 | 50 | zrhrhm 21522 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ Ring →
(ℤRHom‘𝐾)
∈ (ℤring RingHom 𝐾)) |
| 52 | 25, 51 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤring
RingHom 𝐾)) |
| 53 | | zringbas 21464 |
. . . . . . . . . . . . . . . . . 18
⊢ ℤ =
(Base‘ℤring) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 55 | 53, 54 | rhmf 20485 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤRHom‘𝐾) ∈ (ℤring RingHom
𝐾) →
(ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) |
| 56 | 52, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) |
| 58 | | elfzelz 13564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ (0...𝐴) → 𝑡 ∈ ℤ) |
| 59 | 58 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 𝑡 ∈ ℤ) |
| 60 | 57, 59 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((ℤRHom‘𝐾)‘𝑡) ∈ (Base‘𝐾)) |
| 61 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(algSc‘(Poly1‘𝐾)) =
(algSc‘(Poly1‘𝐾)) |
| 62 | 26, 61, 54, 20 | ply1sclcl 22289 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Ring ∧
((ℤRHom‘𝐾)‘𝑡) ∈ (Base‘𝐾)) →
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)) ∈
(Base‘(Poly1‘𝐾))) |
| 63 | 46, 60, 62 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) →
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)) ∈
(Base‘(Poly1‘𝐾))) |
| 64 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘(Poly1‘𝐾)) =
(+g‘(Poly1‘𝐾)) |
| 65 | 20, 64 | mndcl 18755 |
. . . . . . . . . . . . 13
⊢
(((Poly1‘𝐾) ∈ Mnd ∧
(var1‘𝐾)
∈ (Base‘(Poly1‘𝐾)) ∧
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)) ∈
(Base‘(Poly1‘𝐾))) → ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ∈ (Base‘(Poly1‘𝐾))) |
| 66 | 45, 49, 63, 65 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ∈ (Base‘(Poly1‘𝐾))) |
| 67 | 66 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑡 ∈ (0...𝐴)((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ∈ (Base‘(Poly1‘𝐾))) |
| 68 | 67 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ∀𝑡 ∈ (0...𝐴)((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ∈ (Base‘(Poly1‘𝐾))) |
| 69 | 42, 68, 38 | rspcdva 3623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ∈ (Base‘(Poly1‘𝐾))) |
| 70 | 21, 22, 31, 39, 69 | mulgnn0cld 19113 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈ (Base‘(Poly1‘𝐾))) |
| 71 | 26 | ply1idom 26164 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ IDomn →
(Poly1‘𝐾)
∈ IDomn) |
| 72 | 17, 71 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(Poly1‘𝐾)
∈ IDomn) |
| 73 | 72 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (Poly1‘𝐾) ∈ IDomn) |
| 74 | 41 | neeq1d 3000 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑖 → (((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ≠
(0g‘(Poly1‘𝐾)) ↔ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ≠
(0g‘(Poly1‘𝐾)))) |
| 75 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(deg1‘𝐾) = (deg1‘𝐾) |
| 76 | 75, 26, 20 | deg1xrcl 26121 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)) ∈
(Base‘(Poly1‘𝐾)) → ((deg1‘𝐾)‘((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ∈ ℝ*) |
| 77 | 63, 76 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ∈ ℝ*) |
| 78 | | 0xr 11308 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ* |
| 79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 0 ∈
ℝ*) |
| 80 | | 1xr 11320 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ* |
| 81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 1 ∈
ℝ*) |
| 82 | 75, 26, 54, 61 | deg1sclle 26151 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ Ring ∧
((ℤRHom‘𝐾)‘𝑡) ∈ (Base‘𝐾)) → ((deg1‘𝐾)‘((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ≤ 0) |
| 83 | 46, 60, 82 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ≤ 0) |
| 84 | | 0lt1 11785 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 <
1 |
| 85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 0 < 1) |
| 86 | 77, 79, 81, 83, 85 | xrlelttrd 13202 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) < 1) |
| 87 | 21, 22 | mulg1 19099 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((var1‘𝐾) ∈
(Base‘(Poly1‘𝐾)) →
(1(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)) = (var1‘𝐾)) |
| 88 | 49, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) →
(1(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)) = (var1‘𝐾)) |
| 89 | 88 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → (var1‘𝐾) =
(1(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘(var1‘𝐾)) =
((deg1‘𝐾)‘(1(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) |
| 91 | | isfld 20740 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐾 ∈ Field ↔ (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing)) |
| 92 | | drngnzr 20748 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing) |
| 93 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing) → 𝐾 ∈ NzRing) |
| 94 | 91, 93 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐾 ∈ Field → 𝐾 ∈ NzRing) |
| 95 | 15, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ NzRing) |
| 96 | 95 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 𝐾 ∈ NzRing) |
| 97 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℕ0 |
| 98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 1 ∈
ℕ0) |
| 99 | 75, 26, 47, 19, 22 | deg1pw 26160 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ NzRing ∧ 1 ∈
ℕ0) → ((deg1‘𝐾)‘(1(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = 1) |
| 100 | 96, 98, 99 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘(1(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = 1) |
| 101 | 90, 100 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 1 = ((deg1‘𝐾)‘(var1‘𝐾))) |
| 102 | 86, 101 | breqtrd 5169 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) < ((deg1‘𝐾)‘(var1‘𝐾))) |
| 103 | 26, 75, 46, 20, 64, 49, 63, 102 | deg1add 26142 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))) = ((deg1‘𝐾)‘(var1‘𝐾))) |
| 104 | 90, 100 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘(var1‘𝐾)) = 1) |
| 105 | 103, 104 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))) = 1) |
| 106 | 105, 98 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))) ∈ ℕ0) |
| 107 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(Poly1‘𝐾)) =
(0g‘(Poly1‘𝐾)) |
| 108 | 75, 26, 107, 20 | deg1nn0clb 26129 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Ring ∧
((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ∈ (Base‘(Poly1‘𝐾))) →
(((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ≠
(0g‘(Poly1‘𝐾)) ↔ ((deg1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))) ∈ ℕ0)) |
| 109 | 46, 66, 108 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → (((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ≠
(0g‘(Poly1‘𝐾)) ↔ ((deg1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))) ∈ ℕ0)) |
| 110 | 106, 109 | mpbird 257 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ≠
(0g‘(Poly1‘𝐾))) |
| 111 | 110 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑡 ∈ (0...𝐴)((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ≠
(0g‘(Poly1‘𝐾))) |
| 112 | 111 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ∀𝑡 ∈ (0...𝐴)((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) ≠
(0g‘(Poly1‘𝐾))) |
| 113 | 74, 112, 38 | rspcdva 3623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ≠
(0g‘(Poly1‘𝐾))) |
| 114 | 73, 69, 113, 39, 22 | idomnnzpownz 42133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ≠ (0g‘(Poly1‘𝐾))) |
| 115 | 70, 114 | jca 511 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈ (Base‘(Poly1‘𝐾)) ∧ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ≠ (0g‘(Poly1‘𝐾)))) |
| 116 | 115 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑖 ∈ (0...𝐴)(((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈ (Base‘(Poly1‘𝐾)) ∧ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ≠ (0g‘(Poly1‘𝐾)))) |
| 117 | 17, 18, 116 | deg1gprod 42141 |
. . . . 5
⊢ (𝜑 →
(((deg1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) = Σ𝑡 ∈ (0...𝐴)((deg1‘𝐾)‘((𝑖
∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘𝑡)) ∧ 0 ≤ ((deg1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))) |
| 118 | 117 | simpld 494 |
. . . 4
⊢ (𝜑 →
((deg1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) = Σ𝑡 ∈ (0...𝐴)((deg1‘𝐾)‘((𝑖
∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘𝑡))) |
| 119 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖
∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))) |
| 120 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝐴)) ∧ 𝑖 = 𝑡) → 𝑖 = 𝑡) |
| 121 | 120 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝐴)) ∧ 𝑖 = 𝑡) → (𝑈‘𝑖) = (𝑈‘𝑡)) |
| 122 | 120 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝐴)) ∧ 𝑖 = 𝑡) → ((ℤRHom‘𝐾)‘𝑖) = ((ℤRHom‘𝐾)‘𝑡)) |
| 123 | 122 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝐴)) ∧ 𝑖 = 𝑡) →
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)) =
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))) |
| 124 | 123 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝐴)) ∧ 𝑖 = 𝑡) → ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) = ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))) |
| 125 | 121, 124 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (0...𝐴)) ∧ 𝑖 = 𝑡) → ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝑈‘𝑡)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))))) |
| 126 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 𝑡 ∈ (0...𝐴)) |
| 127 | | ovexd 7466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((𝑈‘𝑡)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))) ∈ V) |
| 128 | 119, 125,
126, 127 | fvmptd 7023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘𝑡) = ((𝑈‘𝑡)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))))) |
| 129 | 128 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘𝑡)) = ((deg1‘𝐾)‘((𝑈‘𝑡)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))))) |
| 130 | 17 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → 𝐾 ∈ IDomn) |
| 131 | 36 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → (𝑈‘𝑡) ∈
ℕ0) |
| 132 | 130, 66, 110, 131, 22, 75 | deg1pow 42142 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((𝑈‘𝑡)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))))) = ((𝑈‘𝑡)
· ((deg1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡)))))) |
| 133 | 105 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((𝑈‘𝑡) · ((deg1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))))) = ((𝑈‘𝑡) · 1)) |
| 134 | 131 | nn0cnd 12589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → (𝑈‘𝑡) ∈ ℂ) |
| 135 | 134 | mulridd 11278 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((𝑈‘𝑡) · 1) = (𝑈‘𝑡)) |
| 136 | 133, 135 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((𝑈‘𝑡) · ((deg1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))))) = (𝑈‘𝑡)) |
| 137 | 132, 136 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((𝑈‘𝑡)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑡))))) = (𝑈‘𝑡)) |
| 138 | 129, 137 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (0...𝐴)) → ((deg1‘𝐾)‘((𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘𝑡)) = (𝑈‘𝑡)) |
| 139 | 138 | sumeq2dv 15738 |
. . . 4
⊢ (𝜑 → Σ𝑡 ∈ (0...𝐴)((deg1‘𝐾)‘((𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘𝑡)) = Σ𝑡
∈ (0...𝐴)(𝑈‘𝑡)) |
| 140 | 118, 139 | eqtrd 2777 |
. . 3
⊢ (𝜑 →
((deg1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑈‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) = Σ𝑡 ∈ (0...𝐴)(𝑈‘𝑡)) |
| 141 | 14, 140 | eqtrd 2777 |
. 2
⊢ (𝜑 →
((deg1‘𝐾)‘((𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘𝑈)) = Σ𝑡 ∈ (0...𝐴)(𝑈‘𝑡)) |
| 142 | 4, 141 | eqtrd 2777 |
1
⊢ (𝜑 →
((deg1‘𝐾)‘(𝐺‘𝑈)) = Σ𝑡 ∈ (0...𝐴)(𝑈‘𝑡)) |