Proof of Theorem aks6d1c5lem2
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(eval1‘𝐾) = (eval1‘𝐾) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(Poly1‘𝐾) = (Poly1‘𝐾) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 4 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Poly1‘𝐾)) =
(Base‘(Poly1‘𝐾)) |
| 5 | | aks6d1p5.1 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Field) |
| 6 | | isfld 20740 |
. . . . . . . 8
⊢ (𝐾 ∈ Field ↔ (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing)) |
| 7 | 6 | simprbi 496 |
. . . . . . 7
⊢ (𝐾 ∈ Field → 𝐾 ∈ CRing) |
| 8 | 5, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ CRing) |
| 9 | 8 | crngringd 20243 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ Ring) |
| 10 | | eqid 2737 |
. . . . . . . . . 10
⊢
(ℤRHom‘𝐾) = (ℤRHom‘𝐾) |
| 11 | 10 | zrhrhm 21522 |
. . . . . . . . 9
⊢ (𝐾 ∈ Ring →
(ℤRHom‘𝐾)
∈ (ℤring RingHom 𝐾)) |
| 12 | 9, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤring
RingHom 𝐾)) |
| 13 | | zringbas 21464 |
. . . . . . . . 9
⊢ ℤ =
(Base‘ℤring) |
| 14 | 13, 3 | rhmf 20485 |
. . . . . . . 8
⊢
((ℤRHom‘𝐾) ∈ (ℤring RingHom
𝐾) →
(ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) |
| 15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) |
| 16 | | 0zd 12625 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℤ) |
| 17 | | aks6d1c5p2.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ (0...𝐴)) |
| 18 | 17 | elfzelzd 13565 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ ℤ) |
| 19 | 16, 18 | zsubcld 12727 |
. . . . . . 7
⊢ (𝜑 → (0 − 𝑊) ∈
ℤ) |
| 20 | 15, 19 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → ((ℤRHom‘𝐾)‘(0 − 𝑊)) ∈ (Base‘𝐾)) |
| 21 | | eqid 2737 |
. . . . . . . . 9
⊢
(mulGrp‘(Poly1‘𝐾)) =
(mulGrp‘(Poly1‘𝐾)) |
| 22 | 21, 4 | mgpbas 20142 |
. . . . . . . 8
⊢
(Base‘(Poly1‘𝐾)) =
(Base‘(mulGrp‘(Poly1‘𝐾))) |
| 23 | | aks6d1c5.7 |
. . . . . . . 8
⊢ ↑ =
(.g‘(mulGrp‘(Poly1‘𝐾))) |
| 24 | 2 | ply1crng 22200 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ CRing →
(Poly1‘𝐾)
∈ CRing) |
| 25 | 8, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(Poly1‘𝐾)
∈ CRing) |
| 26 | 21 | crngmgp 20238 |
. . . . . . . . . 10
⊢
((Poly1‘𝐾) ∈ CRing →
(mulGrp‘(Poly1‘𝐾)) ∈ CMnd) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(mulGrp‘(Poly1‘𝐾)) ∈ CMnd) |
| 28 | 27 | cmnmndd 19822 |
. . . . . . . 8
⊢ (𝜑 →
(mulGrp‘(Poly1‘𝐾)) ∈ Mnd) |
| 29 | | aks6d1c5p2.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ (ℕ0
↑m (0...𝐴))) |
| 30 | | nn0ex 12532 |
. . . . . . . . . . . . . . . 16
⊢
ℕ0 ∈ V |
| 31 | 30 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℕ0 ∈
V) |
| 32 | | ovexd 7466 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0...𝐴) ∈ V) |
| 33 | | elmapg 8879 |
. . . . . . . . . . . . . . 15
⊢
((ℕ0 ∈ V ∧ (0...𝐴) ∈ V) → (𝑌 ∈ (ℕ0
↑m (0...𝐴))
↔ 𝑌:(0...𝐴)⟶ℕ0)) |
| 34 | 31, 32, 33 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 ∈ (ℕ0
↑m (0...𝐴))
↔ 𝑌:(0...𝐴)⟶ℕ0)) |
| 35 | 29, 34 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌:(0...𝐴)⟶ℕ0) |
| 36 | 35, 17 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌‘𝑊) ∈
ℕ0) |
| 37 | 36 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌‘𝑊) ∈ ℤ) |
| 38 | 37, 37 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌‘𝑊) − (𝑌‘𝑊)) ∈ ℤ) |
| 39 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) |
| 40 | 39 | leidd 11829 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 0) |
| 41 | 36 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌‘𝑊) ∈ ℝ) |
| 42 | 41 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌‘𝑊) ∈ ℂ) |
| 43 | 42 | subidd 11608 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌‘𝑊) − (𝑌‘𝑊)) = 0) |
| 44 | 43 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 = ((𝑌‘𝑊) − (𝑌‘𝑊))) |
| 45 | 40, 44 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ ((𝑌‘𝑊) − (𝑌‘𝑊))) |
| 46 | 38, 45 | jca 511 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌‘𝑊) − (𝑌‘𝑊)) ∈ ℤ ∧ 0 ≤ ((𝑌‘𝑊) − (𝑌‘𝑊)))) |
| 47 | | elnn0z 12626 |
. . . . . . . . 9
⊢ (((𝑌‘𝑊) − (𝑌‘𝑊)) ∈ ℕ0 ↔
(((𝑌‘𝑊) − (𝑌‘𝑊)) ∈ ℤ ∧ 0 ≤ ((𝑌‘𝑊) − (𝑌‘𝑊)))) |
| 48 | 46, 47 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → ((𝑌‘𝑊) − (𝑌‘𝑊)) ∈
ℕ0) |
| 49 | | aks6d1c5.6 |
. . . . . . . . . . 11
⊢ 𝑋 = (var1‘𝐾) |
| 50 | 1, 49, 3, 2, 4, 8, 20 | evl1vard 22341 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘𝑋)‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 51 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(algSc‘(Poly1‘𝐾)) =
(algSc‘(Poly1‘𝐾)) |
| 52 | 15, 18 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝑊) ∈ (Base‘𝐾)) |
| 53 | 1, 2, 3, 51, 4, 8,
52, 20 | evl1scad 22339 |
. . . . . . . . . 10
⊢ (𝜑 →
(((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((ℤRHom‘𝐾)‘𝑊))) |
| 54 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘(Poly1‘𝐾)) =
(+g‘(Poly1‘𝐾)) |
| 55 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝐾) = (+g‘𝐾) |
| 56 | 1, 2, 3, 4, 8, 20,
50, 53, 54, 55 | evl1addd 22345 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((ℤRHom‘𝐾)‘(0 − 𝑊))(+g‘𝐾)((ℤRHom‘𝐾)‘𝑊)))) |
| 57 | 56 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))) ∈
(Base‘(Poly1‘𝐾))) |
| 58 | 22, 23, 28, 48, 57 | mulgnn0cld 19113 |
. . . . . . 7
⊢ (𝜑 → (((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) ∈
(Base‘(Poly1‘𝐾))) |
| 59 | 43 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) = (0 ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))) |
| 60 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(0g‘(mulGrp‘(Poly1‘𝐾))) =
(0g‘(mulGrp‘(Poly1‘𝐾))) |
| 61 | 22, 60, 23 | mulg0 19092 |
. . . . . . . . . . . 12
⊢ ((𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))) ∈
(Base‘(Poly1‘𝐾)) → (0 ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) =
(0g‘(mulGrp‘(Poly1‘𝐾)))) |
| 62 | 57, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) =
(0g‘(mulGrp‘(Poly1‘𝐾)))) |
| 63 | 59, 62 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) =
(0g‘(mulGrp‘(Poly1‘𝐾)))) |
| 64 | 63 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝜑 →
((eval1‘𝐾)‘(((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))) = ((eval1‘𝐾)‘(0g‘(mulGrp‘(Poly1‘𝐾))))) |
| 65 | 64 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝜑 →
(((eval1‘𝐾)‘(((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((eval1‘𝐾)‘(0g‘(mulGrp‘(Poly1‘𝐾))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 66 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(1r‘(Poly1‘𝐾)) =
(1r‘(Poly1‘𝐾)) |
| 67 | 21, 66 | ringidval 20180 |
. . . . . . . . . . . . 13
⊢
(1r‘(Poly1‘𝐾)) =
(0g‘(mulGrp‘(Poly1‘𝐾))) |
| 68 | 67 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢
(0g‘(mulGrp‘(Poly1‘𝐾))) =
(1r‘(Poly1‘𝐾)) |
| 69 | 68 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 →
(0g‘(mulGrp‘(Poly1‘𝐾))) =
(1r‘(Poly1‘𝐾))) |
| 70 | 69 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 →
((eval1‘𝐾)‘(0g‘(mulGrp‘(Poly1‘𝐾)))) = ((eval1‘𝐾)‘(1r‘(Poly1‘𝐾)))) |
| 71 | 70 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝜑 →
(((eval1‘𝐾)‘(0g‘(mulGrp‘(Poly1‘𝐾))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((eval1‘𝐾)‘(1r‘(Poly1‘𝐾)))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 72 | 2, 49, 21, 23 | ply1idvr1 22298 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ Ring → (0 ↑ 𝑋) =
(1r‘(Poly1‘𝐾))) |
| 73 | 72 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ Ring →
(1r‘(Poly1‘𝐾)) = (0 ↑ 𝑋)) |
| 74 | 9, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(1r‘(Poly1‘𝐾)) = (0 ↑ 𝑋)) |
| 75 | 74 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝜑 →
((eval1‘𝐾)‘(1r‘(Poly1‘𝐾))) = ((eval1‘𝐾)‘(0 ↑ 𝑋))) |
| 76 | 75 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝜑 →
(((eval1‘𝐾)‘(1r‘(Poly1‘𝐾)))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((eval1‘𝐾)‘(0 ↑ 𝑋))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 77 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.g‘(mulGrp‘𝐾)) =
(.g‘(mulGrp‘𝐾)) |
| 78 | 44, 48 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℕ0) |
| 79 | 1, 2, 3, 4, 8, 20,
50, 23, 77, 78 | evl1expd 22349 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((0 ↑ 𝑋) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘(0 ↑ 𝑋))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) =
(0(.g‘(mulGrp‘𝐾))((ℤRHom‘𝐾)‘(0 − 𝑊))))) |
| 80 | 79 | simprd 495 |
. . . . . . . . . . 11
⊢ (𝜑 →
(((eval1‘𝐾)‘(0 ↑ 𝑋))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) =
(0(.g‘(mulGrp‘𝐾))((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 81 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(mulGrp‘𝐾) =
(mulGrp‘𝐾) |
| 82 | 81, 3 | mgpbas 20142 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝐾) =
(Base‘(mulGrp‘𝐾)) |
| 83 | 82 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Base‘𝐾) =
(Base‘(mulGrp‘𝐾))) |
| 84 | 20, 83 | eleqtrd 2843 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℤRHom‘𝐾)‘(0 − 𝑊)) ∈
(Base‘(mulGrp‘𝐾))) |
| 85 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘(mulGrp‘𝐾)) = (Base‘(mulGrp‘𝐾)) |
| 86 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(0g‘(mulGrp‘𝐾)) =
(0g‘(mulGrp‘𝐾)) |
| 87 | 85, 86, 77 | mulg0 19092 |
. . . . . . . . . . . . 13
⊢
(((ℤRHom‘𝐾)‘(0 − 𝑊)) ∈ (Base‘(mulGrp‘𝐾)) →
(0(.g‘(mulGrp‘𝐾))((ℤRHom‘𝐾)‘(0 − 𝑊))) =
(0g‘(mulGrp‘𝐾))) |
| 88 | 84, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(0(.g‘(mulGrp‘𝐾))((ℤRHom‘𝐾)‘(0 − 𝑊))) =
(0g‘(mulGrp‘𝐾))) |
| 89 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝐾) = (1r‘𝐾) |
| 90 | 81, 89 | ringidval 20180 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝐾) = (0g‘(mulGrp‘𝐾)) |
| 91 | 90 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢
(0g‘(mulGrp‘𝐾)) = (1r‘𝐾) |
| 92 | 91 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(0g‘(mulGrp‘𝐾)) = (1r‘𝐾)) |
| 93 | 88, 92 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 →
(0(.g‘(mulGrp‘𝐾))((ℤRHom‘𝐾)‘(0 − 𝑊))) = (1r‘𝐾)) |
| 94 | 80, 93 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 →
(((eval1‘𝐾)‘(0 ↑ 𝑋))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (1r‘𝐾)) |
| 95 | 76, 94 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 →
(((eval1‘𝐾)‘(1r‘(Poly1‘𝐾)))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (1r‘𝐾)) |
| 96 | 71, 95 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 →
(((eval1‘𝐾)‘(0g‘(mulGrp‘(Poly1‘𝐾))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (1r‘𝐾)) |
| 97 | 65, 96 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 →
(((eval1‘𝐾)‘(((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (1r‘𝐾)) |
| 98 | 58, 97 | jca 511 |
. . . . . 6
⊢ (𝜑 → ((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘(((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (1r‘𝐾))) |
| 99 | | fzfid 14014 |
. . . . . . . . 9
⊢ (𝜑 → (0...𝐴) ∈ Fin) |
| 100 | | diffi 9215 |
. . . . . . . . 9
⊢
((0...𝐴) ∈ Fin
→ ((0...𝐴) ∖
{𝑊}) ∈
Fin) |
| 101 | 99, 100 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((0...𝐴) ∖ {𝑊}) ∈ Fin) |
| 102 | 28 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) →
(mulGrp‘(Poly1‘𝐾)) ∈ Mnd) |
| 103 | 35 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝑌:(0...𝐴)⟶ℕ0) |
| 104 | | eldifi 4131 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) → 𝑖 ∈ (0...𝐴)) |
| 105 | 104 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝑖 ∈ (0...𝐴)) |
| 106 | 103, 105 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (𝑌‘𝑖) ∈
ℕ0) |
| 107 | 25 | crngringd 20243 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Poly1‘𝐾)
∈ Ring) |
| 108 | | ringcmn 20279 |
. . . . . . . . . . . . . 14
⊢
((Poly1‘𝐾) ∈ Ring →
(Poly1‘𝐾)
∈ CMnd) |
| 109 | 107, 108 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Poly1‘𝐾)
∈ CMnd) |
| 110 | | cmnmnd 19815 |
. . . . . . . . . . . . 13
⊢
((Poly1‘𝐾) ∈ CMnd →
(Poly1‘𝐾)
∈ Mnd) |
| 111 | 109, 110 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Poly1‘𝐾)
∈ Mnd) |
| 112 | 111 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (Poly1‘𝐾) ∈ Mnd) |
| 113 | 50 | simpld 494 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈
(Base‘(Poly1‘𝐾))) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝑋 ∈
(Base‘(Poly1‘𝐾))) |
| 115 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝐾 ∈ Ring) |
| 116 | 115, 11, 14 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) |
| 117 | 105 | elfzelzd 13565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝑖 ∈ ℤ) |
| 118 | 116, 117 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → ((ℤRHom‘𝐾)‘𝑖) ∈ (Base‘𝐾)) |
| 119 | 2, 51, 3, 4 | ply1sclcl 22289 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Ring ∧
((ℤRHom‘𝐾)‘𝑖) ∈ (Base‘𝐾)) →
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)) ∈
(Base‘(Poly1‘𝐾))) |
| 120 | 115, 118,
119 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) →
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)) ∈
(Base‘(Poly1‘𝐾))) |
| 121 | 4, 54 | mndcl 18755 |
. . . . . . . . . . 11
⊢
(((Poly1‘𝐾) ∈ Mnd ∧ 𝑋 ∈
(Base‘(Poly1‘𝐾)) ∧
((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)) ∈
(Base‘(Poly1‘𝐾))) → (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ∈
(Base‘(Poly1‘𝐾))) |
| 122 | 112, 114,
120, 121 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ∈
(Base‘(Poly1‘𝐾))) |
| 123 | 22, 23, 102, 106, 122 | mulgnn0cld 19113 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈
(Base‘(Poly1‘𝐾))) |
| 124 | 123 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑖 ∈ ((0...𝐴) ∖ {𝑊})((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈
(Base‘(Poly1‘𝐾))) |
| 125 | 22, 27, 101, 124 | gsummptcl 19985 |
. . . . . . 7
⊢ (𝜑 →
((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))) ∈
(Base‘(Poly1‘𝐾))) |
| 126 | 124 | r19.21bi 3251 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈
(Base‘(Poly1‘𝐾))) |
| 127 | 126 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑖 ∈ ((0...𝐴) ∖ {𝑊})((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈
(Base‘(Poly1‘𝐾))) |
| 128 | 1, 2, 21, 3, 4, 81, 8, 20, 127, 101 | evl1gprodd 42118 |
. . . . . . 7
⊢ (𝜑 →
(((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))))) |
| 129 | 125, 128 | jca 511 |
. . . . . 6
⊢ (𝜑 →
(((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))))) |
| 130 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘(Poly1‘𝐾)) =
(.r‘(Poly1‘𝐾)) |
| 131 | 21, 130 | mgpplusg 20141 |
. . . . . . 7
⊢
(.r‘(Poly1‘𝐾)) =
(+g‘(mulGrp‘(Poly1‘𝐾))) |
| 132 | 131 | eqcomi 2746 |
. . . . . 6
⊢
(+g‘(mulGrp‘(Poly1‘𝐾))) =
(.r‘(Poly1‘𝐾)) |
| 133 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝐾) = (.r‘𝐾) |
| 134 | 1, 2, 3, 4, 8, 20,
98, 129, 132, 133 | evl1muld 22347 |
. . . . 5
⊢ (𝜑 → (((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
∈ (Base‘(Poly1‘𝐾))
∧ (((eval1‘𝐾)‘((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((1r‘𝐾)(.r‘𝐾)((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦
(((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))))))) |
| 135 | 134 | simprd 495 |
. . . 4
⊢ (𝜑 →
(((eval1‘𝐾)‘((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((1r‘𝐾)(.r‘𝐾)((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦
(((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))))) |
| 136 | | fldidom 20771 |
. . . . . . . 8
⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn) |
| 137 | 5, 136 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ IDomn) |
| 138 | | isidom 20725 |
. . . . . . 7
⊢ (𝐾 ∈ IDomn ↔ (𝐾 ∈ CRing ∧ 𝐾 ∈ Domn)) |
| 139 | 137, 138 | sylib 218 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∈ CRing ∧ 𝐾 ∈ Domn)) |
| 140 | 139 | simprd 495 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Domn) |
| 141 | 90 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝐾) =
(0g‘(mulGrp‘𝐾))) |
| 142 | 81 | ringmgp 20236 |
. . . . . . . . 9
⊢ (𝐾 ∈ Ring →
(mulGrp‘𝐾) ∈
Mnd) |
| 143 | 9, 142 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (mulGrp‘𝐾) ∈ Mnd) |
| 144 | 82, 86 | mndidcl 18762 |
. . . . . . . 8
⊢
((mulGrp‘𝐾)
∈ Mnd → (0g‘(mulGrp‘𝐾)) ∈ (Base‘𝐾)) |
| 145 | 143, 144 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(0g‘(mulGrp‘𝐾)) ∈ (Base‘𝐾)) |
| 146 | 141, 145 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → (1r‘𝐾) ∈ (Base‘𝐾)) |
| 147 | 5 | flddrngd 20741 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ DivRing) |
| 148 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝐾) = (0g‘𝐾) |
| 149 | 148, 89 | drngunz 20747 |
. . . . . . 7
⊢ (𝐾 ∈ DivRing →
(1r‘𝐾)
≠ (0g‘𝐾)) |
| 150 | 147, 149 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝐾) ≠
(0g‘𝐾)) |
| 151 | 146, 150 | jca 511 |
. . . . 5
⊢ (𝜑 →
((1r‘𝐾)
∈ (Base‘𝐾) ∧
(1r‘𝐾)
≠ (0g‘𝐾))) |
| 152 | 81 | crngmgp 20238 |
. . . . . . . 8
⊢ (𝐾 ∈ CRing →
(mulGrp‘𝐾) ∈
CMnd) |
| 153 | 8, 152 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd) |
| 154 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝐾 ∈ CRing) |
| 155 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → ((ℤRHom‘𝐾)‘(0 − 𝑊)) ∈ (Base‘𝐾)) |
| 156 | 1, 2, 3, 4, 154, 155, 123 | fveval1fvcl 22337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) ∈ (Base‘𝐾)) |
| 157 | 156 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ ((0...𝐴) ∖ {𝑊})(((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) ∈ (Base‘𝐾)) |
| 158 | 82, 153, 101, 157 | gsummptcl 19985 |
. . . . . 6
⊢ (𝜑 → ((mulGrp‘𝐾) Σg
(𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) ∈ (Base‘𝐾)) |
| 159 | 22 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) →
(Base‘(Poly1‘𝐾)) =
(Base‘(mulGrp‘(Poly1‘𝐾)))) |
| 160 | 122, 159 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ∈
(Base‘(mulGrp‘(Poly1‘𝐾)))) |
| 161 | 22 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢
(Base‘(mulGrp‘(Poly1‘𝐾))) =
(Base‘(Poly1‘𝐾)) |
| 162 | 161 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) →
(Base‘(mulGrp‘(Poly1‘𝐾))) =
(Base‘(Poly1‘𝐾))) |
| 163 | 160, 162 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ∈
(Base‘(Poly1‘𝐾))) |
| 164 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 165 | 163, 164 | jca 511 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → ((𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) |
| 166 | 1, 2, 3, 4, 154, 155, 165, 23, 77, 106 | evl1expd 22349 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((𝑌‘𝑖)(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))))) |
| 167 | 166 | simprd 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((𝑌‘𝑖)(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) |
| 168 | 137 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝐾 ∈ IDomn) |
| 169 | 1, 2, 3, 4, 154, 155, 163 | fveval1fvcl 22337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) ∈ (Base‘𝐾)) |
| 170 | | eldifsni 4790 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) → 𝑖 ≠ 𝑊) |
| 171 | 170 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝑖 ≠ 𝑊) |
| 172 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝐾 ∈ Field) |
| 173 | | aks6d1p5.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 174 | 173 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝑃 ∈ ℙ) |
| 175 | | aks6d1c5.3 |
. . . . . . . . . . . 12
⊢ 𝑃 = (chr‘𝐾) |
| 176 | | aks6d1c5.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈
ℕ0) |
| 177 | 176 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝐴 ∈
ℕ0) |
| 178 | | aks6d1c5.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 𝑃) |
| 179 | 178 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝐴 < 𝑃) |
| 180 | | aks6d1c5.8 |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) |
| 181 | 17 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝑊 ∈ (0...𝐴)) |
| 182 | 172, 174,
175, 177, 179, 49, 23, 180, 105, 181 | aks6d1c5lem1 42137 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (𝑖 = 𝑊 ↔ (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (0g‘𝐾))) |
| 183 | 182 | necon3bid 2985 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (𝑖 ≠ 𝑊 ↔ (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) ≠ (0g‘𝐾))) |
| 184 | 171, 183 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) ≠ (0g‘𝐾)) |
| 185 | 168, 169,
184, 106, 77 | idomnnzpownz 42133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → ((𝑌‘𝑖)(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) ≠ (0g‘𝐾)) |
| 186 | 167, 185 | eqnetrd 3008 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) ≠ (0g‘𝐾)) |
| 187 | 81, 137, 101, 156, 186 | idomnnzgmulnz 42134 |
. . . . . 6
⊢ (𝜑 → ((mulGrp‘𝐾) Σg
(𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) ≠ (0g‘𝐾)) |
| 188 | 158, 187 | jca 511 |
. . . . 5
⊢ (𝜑 → (((mulGrp‘𝐾) Σg
(𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) ∈ (Base‘𝐾) ∧ ((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) ≠ (0g‘𝐾))) |
| 189 | 3, 133, 148 | domnmuln0 20709 |
. . . . 5
⊢ ((𝐾 ∈ Domn ∧
((1r‘𝐾)
∈ (Base‘𝐾) ∧
(1r‘𝐾)
≠ (0g‘𝐾)) ∧ (((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) ∈ (Base‘𝐾) ∧ ((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) ≠ (0g‘𝐾))) → ((1r‘𝐾)(.r‘𝐾)((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))))) ≠ (0g‘𝐾)) |
| 190 | 140, 151,
188, 189 | syl3anc 1373 |
. . . 4
⊢ (𝜑 →
((1r‘𝐾)(.r‘𝐾)((mulGrp‘𝐾) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ (((eval1‘𝐾)‘((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))))) ≠ (0g‘𝐾)) |
| 191 | 135, 190 | eqnetrd 3008 |
. . 3
⊢ (𝜑 →
(((eval1‘𝐾)‘((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) ≠ (0g‘𝐾)) |
| 192 | 191 | necomd 2996 |
. 2
⊢ (𝜑 → (0g‘𝐾) ≠
(((eval1‘𝐾)‘((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 193 | 41 | leidd 11829 |
. . . . . . . 8
⊢ (𝜑 → (𝑌‘𝑊) ≤ (𝑌‘𝑊)) |
| 194 | | eqid 2737 |
. . . . . . . 8
⊢
(quot1p‘𝐾) = (quot1p‘𝐾) |
| 195 | 5, 173, 175, 176, 178, 49, 23, 180, 29, 17, 36, 193, 194, 51, 21 | aks6d1c5lem3 42138 |
. . . . . . 7
⊢ (𝜑 → ((𝐺‘𝑌)(quot1p‘𝐾)((𝑌‘𝑊) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))) = ((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))) |
| 196 | 195 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
= ((𝐺‘𝑌)(quot1p‘𝐾)((𝑌‘𝑊) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))) |
| 197 | | aks6d1c5p2.3 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝑌) = (𝐺‘𝑍)) |
| 198 | 197 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((𝐺‘𝑌)(quot1p‘𝐾)((𝑌‘𝑊) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))) = ((𝐺‘𝑍)(quot1p‘𝐾)((𝑌‘𝑊) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))) |
| 199 | | aks6d1c5p2.2 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (ℕ0
↑m (0...𝐴))) |
| 200 | | elmapg 8879 |
. . . . . . . . . . . 12
⊢
((ℕ0 ∈ V ∧ (0...𝐴) ∈ V) → (𝑍 ∈ (ℕ0
↑m (0...𝐴))
↔ 𝑍:(0...𝐴)⟶ℕ0)) |
| 201 | 31, 32, 200 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑍 ∈ (ℕ0
↑m (0...𝐴))
↔ 𝑍:(0...𝐴)⟶ℕ0)) |
| 202 | 199, 201 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍:(0...𝐴)⟶ℕ0) |
| 203 | 202, 17 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (𝜑 → (𝑍‘𝑊) ∈
ℕ0) |
| 204 | 203 | nn0red 12588 |
. . . . . . . 8
⊢ (𝜑 → (𝑍‘𝑊) ∈ ℝ) |
| 205 | | aks6d1c5p2.5 |
. . . . . . . 8
⊢ (𝜑 → (𝑌‘𝑊) < (𝑍‘𝑊)) |
| 206 | 41, 204, 205 | ltled 11409 |
. . . . . . 7
⊢ (𝜑 → (𝑌‘𝑊) ≤ (𝑍‘𝑊)) |
| 207 | 5, 173, 175, 176, 178, 49, 23, 180, 199, 17, 36, 206, 194, 51, 21 | aks6d1c5lem3 42138 |
. . . . . 6
⊢ (𝜑 → ((𝐺‘𝑍)(quot1p‘𝐾)((𝑌‘𝑊) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))) = ((((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))) |
| 208 | 196, 198,
207 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → ((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
= ((((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))) |
| 209 | 208 | fveq2d 6910 |
. . . 4
⊢ (𝜑 →
((eval1‘𝐾)‘((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))) = ((eval1‘𝐾)‘((((𝑍‘𝑊)
− (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))) |
| 210 | 209 | fveq1d 6908 |
. . 3
⊢ (𝜑 →
(((eval1‘𝐾)‘((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((eval1‘𝐾)‘((((𝑍‘𝑊)
− (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 211 | 203 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑍‘𝑊) ∈ ℤ) |
| 212 | 211, 37 | zsubcld 12727 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℤ) |
| 213 | 204, 41 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℝ) |
| 214 | 41, 204 | posdifd 11850 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌‘𝑊) < (𝑍‘𝑊) ↔ 0 < ((𝑍‘𝑊) − (𝑌‘𝑊)))) |
| 215 | 205, 214 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < ((𝑍‘𝑊) − (𝑌‘𝑊))) |
| 216 | 39, 213, 215 | ltled 11409 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ ((𝑍‘𝑊) − (𝑌‘𝑊))) |
| 217 | 212, 216 | jca 511 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℤ ∧ 0 ≤ ((𝑍‘𝑊) − (𝑌‘𝑊)))) |
| 218 | | elnn0z 12626 |
. . . . . . . . . 10
⊢ (((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℕ0 ↔
(((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℤ ∧ 0 ≤ ((𝑍‘𝑊) − (𝑌‘𝑊)))) |
| 219 | 217, 218 | sylibr 234 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑍‘𝑊) − (𝑌‘𝑊)) ∈
ℕ0) |
| 220 | 1, 2, 3, 4, 8, 20,
56, 23, 77, 219 | evl1expd 22349 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘(((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((𝑍‘𝑊) − (𝑌‘𝑊))(.g‘(mulGrp‘𝐾))(((ℤRHom‘𝐾)‘(0 − 𝑊))(+g‘𝐾)((ℤRHom‘𝐾)‘𝑊))))) |
| 221 | 220 | simpld 494 |
. . . . . . 7
⊢ (𝜑 → (((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) ∈
(Base‘(Poly1‘𝐾))) |
| 222 | 220 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 →
(((eval1‘𝐾)‘(((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((𝑍‘𝑊) − (𝑌‘𝑊))(.g‘(mulGrp‘𝐾))(((ℤRHom‘𝐾)‘(0 − 𝑊))(+g‘𝐾)((ℤRHom‘𝐾)‘𝑊)))) |
| 223 | | rhmghm 20484 |
. . . . . . . . . . . . 13
⊢
((ℤRHom‘𝐾) ∈ (ℤring RingHom
𝐾) →
(ℤRHom‘𝐾)
∈ (ℤring GrpHom 𝐾)) |
| 224 | 12, 223 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤring
GrpHom 𝐾)) |
| 225 | 19, 13 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 𝑊) ∈
(Base‘ℤring)) |
| 226 | 18, 13 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈
(Base‘ℤring)) |
| 227 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘ℤring) =
(Base‘ℤring) |
| 228 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘ℤring) =
(+g‘ℤring) |
| 229 | 227, 228,
55 | ghmlin 19239 |
. . . . . . . . . . . 12
⊢
(((ℤRHom‘𝐾) ∈ (ℤring GrpHom
𝐾) ∧ (0 − 𝑊) ∈
(Base‘ℤring) ∧ 𝑊 ∈ (Base‘ℤring))
→ ((ℤRHom‘𝐾)‘((0 − 𝑊)(+g‘ℤring)𝑊)) = (((ℤRHom‘𝐾)‘(0 − 𝑊))(+g‘𝐾)((ℤRHom‘𝐾)‘𝑊))) |
| 230 | 224, 225,
226, 229 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝑊)(+g‘ℤring)𝑊)) = (((ℤRHom‘𝐾)‘(0 − 𝑊))(+g‘𝐾)((ℤRHom‘𝐾)‘𝑊))) |
| 231 | | zringplusg 21465 |
. . . . . . . . . . . . . . . . 17
⊢ + =
(+g‘ℤring) |
| 232 | 231 | eqcomi 2746 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘ℤring) = + |
| 233 | 232 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(+g‘ℤring) = + ) |
| 234 | 233 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((0 − 𝑊)(+g‘ℤring)𝑊) = ((0 − 𝑊) + 𝑊)) |
| 235 | 234 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝑊)(+g‘ℤring)𝑊)) = ((ℤRHom‘𝐾)‘((0 − 𝑊) + 𝑊))) |
| 236 | | 0cnd 11254 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℂ) |
| 237 | 18 | zcnd 12723 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑊 ∈ ℂ) |
| 238 | 236, 237 | npcand 11624 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((0 − 𝑊) + 𝑊) = 0) |
| 239 | 238 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝑊) + 𝑊)) = ((ℤRHom‘𝐾)‘0)) |
| 240 | 235, 239 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝑊)(+g‘ℤring)𝑊)) = ((ℤRHom‘𝐾)‘0)) |
| 241 | 10, 148 | zrh0 21524 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ Ring →
((ℤRHom‘𝐾)‘0) = (0g‘𝐾)) |
| 242 | 9, 241 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) =
(0g‘𝐾)) |
| 243 | 240, 242 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝑊)(+g‘ℤring)𝑊)) = (0g‘𝐾)) |
| 244 | 230, 243 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (𝜑 → (((ℤRHom‘𝐾)‘(0 − 𝑊))(+g‘𝐾)((ℤRHom‘𝐾)‘𝑊)) = (0g‘𝐾)) |
| 245 | 244 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑍‘𝑊) − (𝑌‘𝑊))(.g‘(mulGrp‘𝐾))(((ℤRHom‘𝐾)‘(0 − 𝑊))(+g‘𝐾)((ℤRHom‘𝐾)‘𝑊))) = (((𝑍‘𝑊) − (𝑌‘𝑊))(.g‘(mulGrp‘𝐾))(0g‘𝐾))) |
| 246 | 219 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℤ) |
| 247 | 246, 215 | jca 511 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℤ ∧ 0 < ((𝑍‘𝑊) − (𝑌‘𝑊)))) |
| 248 | | elnnz 12623 |
. . . . . . . . . . 11
⊢ (((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℕ ↔ (((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℤ ∧ 0 < ((𝑍‘𝑊) − (𝑌‘𝑊)))) |
| 249 | 247, 248 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑍‘𝑊) − (𝑌‘𝑊)) ∈ ℕ) |
| 250 | 9, 249, 77 | ringexp0nn 42135 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑍‘𝑊) − (𝑌‘𝑊))(.g‘(mulGrp‘𝐾))(0g‘𝐾)) = (0g‘𝐾)) |
| 251 | 245, 250 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (((𝑍‘𝑊) − (𝑌‘𝑊))(.g‘(mulGrp‘𝐾))(((ℤRHom‘𝐾)‘(0 − 𝑊))(+g‘𝐾)((ℤRHom‘𝐾)‘𝑊))) = (0g‘𝐾)) |
| 252 | 222, 251 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 →
(((eval1‘𝐾)‘(((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (0g‘𝐾)) |
| 253 | 221, 252 | jca 511 |
. . . . . 6
⊢ (𝜑 → ((((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘(((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊)))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (0g‘𝐾))) |
| 254 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘(mulGrp‘(Poly1‘𝐾))) =
(Base‘(mulGrp‘(Poly1‘𝐾))) |
| 255 | 202 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → 𝑍:(0...𝐴)⟶ℕ0) |
| 256 | 255, 105 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → (𝑍‘𝑖) ∈
ℕ0) |
| 257 | 254, 23, 102, 256, 160 | mulgnn0cld 19113 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈
(Base‘(mulGrp‘(Poly1‘𝐾)))) |
| 258 | 257, 162 | eleqtrd 2843 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((0...𝐴) ∖ {𝑊})) → ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈
(Base‘(Poly1‘𝐾))) |
| 259 | 258 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑖 ∈ ((0...𝐴) ∖ {𝑊})((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))) ∈
(Base‘(Poly1‘𝐾))) |
| 260 | 22, 27, 101, 259 | gsummptcl 19985 |
. . . . . . 7
⊢ (𝜑 →
((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))) ∈
(Base‘(Poly1‘𝐾))) |
| 261 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 →
(((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) |
| 262 | 260, 261 | jca 511 |
. . . . . 6
⊢ (𝜑 →
(((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))) ∈
(Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) |
| 263 | 1, 2, 3, 4, 8, 20,
253, 262, 132, 133 | evl1muld 22347 |
. . . . 5
⊢ (𝜑 → (((((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
∈ (Base‘(Poly1‘𝐾))
∧ (((eval1‘𝐾)‘((((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((0g‘𝐾)(.r‘𝐾)(((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))))) |
| 264 | 263 | simprd 495 |
. . . 4
⊢ (𝜑 →
(((eval1‘𝐾)‘((((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = ((0g‘𝐾)(.r‘𝐾)(((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))))) |
| 265 | 1, 2, 3, 4, 8, 20,
260 | fveval1fvcl 22337 |
. . . . 5
⊢ (𝜑 →
(((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) ∈ (Base‘𝐾)) |
| 266 | 3, 133, 148, 9, 265 | ringlzd 20292 |
. . . 4
⊢ (𝜑 →
((0g‘𝐾)(.r‘𝐾)(((eval1‘𝐾)‘((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊)))) = (0g‘𝐾)) |
| 267 | 264, 266 | eqtrd 2777 |
. . 3
⊢ (𝜑 →
(((eval1‘𝐾)‘((((𝑍‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑍‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (0g‘𝐾)) |
| 268 | 210, 267 | eqtrd 2777 |
. 2
⊢ (𝜑 →
(((eval1‘𝐾)‘((((𝑌‘𝑊) − (𝑌‘𝑊)) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑊))))(+g‘(mulGrp‘(Poly1‘𝐾)))((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ ((0...𝐴)
∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))))‘((ℤRHom‘𝐾)‘(0 − 𝑊))) = (0g‘𝐾)) |
| 269 | 192, 268 | neeqtrd 3010 |
1
⊢ (𝜑 → (0g‘𝐾) ≠
(0g‘𝐾)) |