Step | Hyp | Ref
| Expression |
1 | | oveq2 7421 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑘 ↑ 𝑥) = (𝑘 ↑ 𝑋)) |
2 | 1 | oveq2d 7429 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑘) · (𝑘 ↑ 𝑥)) = ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))) |
3 | 2 | mpteq2dv 5245 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑥))) = (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) |
4 | 3 | oveq2d 7429 |
. . 3
⊢ (𝑥 = 𝑋 → (𝑅 Σg (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑥)))) = (𝑅 Σg (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))))) |
5 | | evl1deg1.2 |
. . . 4
⊢ 𝑂 = (eval1‘𝑅) |
6 | | evl1deg1.1 |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
7 | | evl1deg1.3 |
. . . 4
⊢ 𝐾 = (Base‘𝑅) |
8 | | evl1deg1.4 |
. . . 4
⊢ 𝑈 = (Base‘𝑃) |
9 | | evl1deg2.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ CRing) |
10 | | evl1deg2.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ 𝑈) |
11 | | evl1deg1.5 |
. . . 4
⊢ · =
(.r‘𝑅) |
12 | | evl1deg2.p |
. . . 4
⊢ ↑ =
(.g‘(mulGrp‘𝑅)) |
13 | | evl1deg2.f |
. . . 4
⊢ 𝐹 = (coe1‘𝑀) |
14 | 5, 6, 7, 8, 9, 10,
11, 12, 13 | evl1fpws 33440 |
. . 3
⊢ (𝜑 → (𝑂‘𝑀) = (𝑥 ∈ 𝐾 ↦ (𝑅 Σg (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑥)))))) |
15 | | evl1deg2.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐾) |
16 | | ovexd 7448 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) ∈ V) |
17 | 4, 14, 15, 16 | fvmptd4 7022 |
. 2
⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = (𝑅 Σg (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))))) |
18 | | eqid 2726 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
19 | | evl1deg1.6 |
. . 3
⊢ + =
(+g‘𝑅) |
20 | 9 | crngringd 20222 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
21 | 20 | ringcmnd 20256 |
. . 3
⊢ (𝜑 → 𝑅 ∈ CMnd) |
22 | | nn0ex 12521 |
. . . 4
⊢
ℕ0 ∈ V |
23 | 22 | a1i 11 |
. . 3
⊢ (𝜑 → ℕ0 ∈
V) |
24 | 20 | adantr 479 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
25 | 13, 8, 6, 7 | coe1fvalcl 22195 |
. . . . 5
⊢ ((𝑀 ∈ 𝑈 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ 𝐾) |
26 | 10, 25 | sylan 578 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ 𝐾) |
27 | | eqid 2726 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
28 | 27, 7 | mgpbas 20116 |
. . . . 5
⊢ 𝐾 =
(Base‘(mulGrp‘𝑅)) |
29 | 27 | ringmgp 20215 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
30 | 20, 29 | syl 17 |
. . . . . 6
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
31 | 30 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(mulGrp‘𝑅) ∈
Mnd) |
32 | | simpr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
33 | 15 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ 𝐾) |
34 | 28, 12, 31, 32, 33 | mulgnn0cld 19082 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐾) |
35 | 7, 11, 24, 26, 34 | ringcld 20235 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐾) |
36 | | fvexd 6905 |
. . . 4
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
37 | | fveq2 6890 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) |
38 | | oveq1 7420 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝑘 ↑ 𝑋) = (𝑗 ↑ 𝑋)) |
39 | 37, 38 | oveq12d 7431 |
. . . 4
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)) = ((𝐹‘𝑗) · (𝑗 ↑ 𝑋))) |
40 | | breq1 5146 |
. . . . . . 7
⊢ (𝑖 = (𝐸‘𝑀) → (𝑖 < 𝑗 ↔ (𝐸‘𝑀) < 𝑗)) |
41 | 40 | imbi1d 340 |
. . . . . 6
⊢ (𝑖 = (𝐸‘𝑀) → ((𝑖 < 𝑗 → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = (0g‘𝑅)) ↔ ((𝐸‘𝑀) < 𝑗 → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = (0g‘𝑅)))) |
42 | 41 | ralbidv 3168 |
. . . . 5
⊢ (𝑖 = (𝐸‘𝑀) → (∀𝑗 ∈ ℕ0 (𝑖 < 𝑗 → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = (0g‘𝑅)) ↔ ∀𝑗 ∈ ℕ0 ((𝐸‘𝑀) < 𝑗 → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = (0g‘𝑅)))) |
43 | | evl1deg2.1 |
. . . . . 6
⊢ (𝜑 → (𝐸‘𝑀) = 2) |
44 | | 2nn0 12532 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℕ0) |
46 | 43, 45 | eqeltrd 2826 |
. . . . 5
⊢ (𝜑 → (𝐸‘𝑀) ∈
ℕ0) |
47 | 10 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → 𝑀 ∈ 𝑈) |
48 | | simplr 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → 𝑗 ∈ ℕ0) |
49 | | simpr 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → (𝐸‘𝑀) < 𝑗) |
50 | | evl1deg2.e |
. . . . . . . . . . 11
⊢ 𝐸 = (deg1‘𝑅) |
51 | 50, 6, 8, 18, 13 | deg1lt 26118 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ 𝑈 ∧ 𝑗 ∈ ℕ0 ∧ (𝐸‘𝑀) < 𝑗) → (𝐹‘𝑗) = (0g‘𝑅)) |
52 | 47, 48, 49, 51 | syl3anc 1368 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → (𝐹‘𝑗) = (0g‘𝑅)) |
53 | 52 | oveq1d 7428 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = ((0g‘𝑅) · (𝑗 ↑ 𝑋))) |
54 | 20 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → 𝑅 ∈ Ring) |
55 | 54, 29 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → (mulGrp‘𝑅) ∈ Mnd) |
56 | 15 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → 𝑋 ∈ 𝐾) |
57 | 28, 12, 55, 48, 56 | mulgnn0cld 19082 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → (𝑗 ↑ 𝑋) ∈ 𝐾) |
58 | 7, 11, 18, 54, 57 | ringlzd 20267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → ((0g‘𝑅) · (𝑗 ↑ 𝑋)) = (0g‘𝑅)) |
59 | 53, 58 | eqtrd 2766 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ (𝐸‘𝑀) < 𝑗) → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = (0g‘𝑅)) |
60 | 59 | ex 411 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐸‘𝑀) < 𝑗 → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = (0g‘𝑅))) |
61 | 60 | ralrimiva 3136 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ ℕ0 ((𝐸‘𝑀) < 𝑗 → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = (0g‘𝑅))) |
62 | 42, 46, 61 | rspcedvdw 3610 |
. . . 4
⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑗 ∈ ℕ0
(𝑖 < 𝑗 → ((𝐹‘𝑗) · (𝑗 ↑ 𝑋)) = (0g‘𝑅))) |
63 | 36, 35, 39, 62 | mptnn0fsuppd 14009 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑅)) |
64 | | fzouzdisj 13713 |
. . . 4
⊢ ((0..^3)
∩ (ℤ≥‘3)) = ∅ |
65 | 64 | a1i 11 |
. . 3
⊢ (𝜑 → ((0..^3) ∩
(ℤ≥‘3)) = ∅) |
66 | | nn0uz 12907 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
67 | | 3nn0 12533 |
. . . . . . 7
⊢ 3 ∈
ℕ0 |
68 | 67, 66 | eleqtri 2824 |
. . . . . 6
⊢ 3 ∈
(ℤ≥‘0) |
69 | | fzouzsplit 13712 |
. . . . . 6
⊢ (3 ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0..^3) ∪ (ℤ≥‘3))) |
70 | 68, 69 | ax-mp 5 |
. . . . 5
⊢
(ℤ≥‘0) = ((0..^3) ∪
(ℤ≥‘3)) |
71 | 66, 70 | eqtri 2754 |
. . . 4
⊢
ℕ0 = ((0..^3) ∪
(ℤ≥‘3)) |
72 | 71 | a1i 11 |
. . 3
⊢ (𝜑 → ℕ0 =
((0..^3) ∪ (ℤ≥‘3))) |
73 | 7, 18, 19, 21, 23, 35, 63, 65, 72 | gsumsplit2 19920 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ ℕ0
↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) = ((𝑅 Σg (𝑘 ∈ (0..^3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) + (𝑅 Σg (𝑘 ∈
(ℤ≥‘3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))))) |
74 | | fzo0to3tp 13763 |
. . . . . . 7
⊢ (0..^3) =
{0, 1, 2} |
75 | 74 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0..^3) = {0, 1,
2}) |
76 | 75 | mpteq1d 5238 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (0..^3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ {0, 1, 2} ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) |
77 | 76 | oveq2d 7429 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ (0..^3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) = (𝑅 Σg (𝑘 ∈ {0, 1, 2} ↦
((𝐹‘𝑘) · (𝑘 ↑ 𝑋))))) |
78 | 10 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ 𝑀 ∈ 𝑈) |
79 | | uzss 12888 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
(ℤ≥‘0) → (ℤ≥‘3)
⊆ (ℤ≥‘0)) |
80 | 68, 79 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘3) ⊆
(ℤ≥‘0) |
81 | 80, 66 | sseqtrri 4016 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘3) ⊆
ℕ0 |
82 | 81 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 →
(ℤ≥‘3) ⊆ ℕ0) |
83 | 82 | sselda 3978 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ 𝑘 ∈
ℕ0) |
84 | 43 | adantr 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ (𝐸‘𝑀) = 2) |
85 | | 2p1e3 12397 |
. . . . . . . . . . . . . . 15
⊢ (2 + 1) =
3 |
86 | 85 | fveq2i 6893 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘(2 + 1)) =
(ℤ≥‘3) |
87 | 86 | eleq2i 2818 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘(2 + 1)) ↔ 𝑘 ∈
(ℤ≥‘3)) |
88 | | 2z 12637 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
89 | | eluzp1l 12892 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ 𝑘
∈ (ℤ≥‘(2 + 1))) → 2 < 𝑘) |
90 | 88, 89 | mpan 688 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘(2 + 1)) → 2 < 𝑘) |
91 | 87, 90 | sylbir 234 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘3) → 2 < 𝑘) |
92 | 91 | adantl 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ 2 < 𝑘) |
93 | 84, 92 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ (𝐸‘𝑀) < 𝑘) |
94 | 50, 6, 8, 18, 13 | deg1lt 26118 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ 𝑈 ∧ 𝑘 ∈ ℕ0 ∧ (𝐸‘𝑀) < 𝑘) → (𝐹‘𝑘) = (0g‘𝑅)) |
95 | 78, 83, 93, 94 | syl3anc 1368 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ (𝐹‘𝑘) = (0g‘𝑅)) |
96 | 95 | oveq1d 7428 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)) = ((0g‘𝑅) · (𝑘 ↑ 𝑋))) |
97 | 20 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ 𝑅 ∈
Ring) |
98 | 97, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ (mulGrp‘𝑅)
∈ Mnd) |
99 | 15 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝐾) |
100 | 28, 12, 98, 83, 99 | mulgnn0cld 19082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ (𝑘 ↑ 𝑋) ∈ 𝐾) |
101 | 7, 11, 18, 97, 100 | ringlzd 20267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ ((0g‘𝑅) · (𝑘 ↑ 𝑋)) = (0g‘𝑅)) |
102 | 96, 101 | eqtrd 2766 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘3))
→ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)) = (0g‘𝑅)) |
103 | 102 | mpteq2dva 5243 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘3)
↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ (ℤ≥‘3)
↦ (0g‘𝑅))) |
104 | 103 | oveq2d 7429 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈
(ℤ≥‘3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) = (𝑅 Σg (𝑘 ∈
(ℤ≥‘3) ↦ (0g‘𝑅)))) |
105 | 9 | crnggrpd 20223 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Grp) |
106 | 105 | grpmndd 18933 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Mnd) |
107 | | fvexd 6905 |
. . . . . 6
⊢ (𝜑 →
(ℤ≥‘3) ∈ V) |
108 | 18 | gsumz 18818 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧
(ℤ≥‘3) ∈ V) → (𝑅 Σg (𝑘 ∈
(ℤ≥‘3) ↦ (0g‘𝑅))) = (0g‘𝑅)) |
109 | 106, 107,
108 | syl2anc 582 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈
(ℤ≥‘3) ↦ (0g‘𝑅))) = (0g‘𝑅)) |
110 | 104, 109 | eqtrd 2766 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈
(ℤ≥‘3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) = (0g‘𝑅)) |
111 | 77, 110 | oveq12d 7431 |
. . 3
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0..^3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) + (𝑅 Σg (𝑘 ∈
(ℤ≥‘3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))))) = ((𝑅 Σg (𝑘 ∈ {0, 1, 2} ↦
((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) + (0g‘𝑅))) |
112 | | tpex 7744 |
. . . . . 6
⊢ {0, 1, 2}
∈ V |
113 | 112 | a1i 11 |
. . . . 5
⊢ (𝜑 → {0, 1, 2} ∈
V) |
114 | 20 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {0, 1, 2}) → 𝑅 ∈ Ring) |
115 | 13, 8, 6, 7 | coe1f 22194 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝑈 → 𝐹:ℕ0⟶𝐾) |
116 | 10, 115 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ0⟶𝐾) |
117 | 116 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {0, 1, 2}) → 𝐹:ℕ0⟶𝐾) |
118 | | fzo0ssnn0 13758 |
. . . . . . . . . 10
⊢ (0..^3)
⊆ ℕ0 |
119 | 75, 118 | eqsstrrdi 4034 |
. . . . . . . . 9
⊢ (𝜑 → {0, 1, 2} ⊆
ℕ0) |
120 | 119 | sselda 3978 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {0, 1, 2}) → 𝑘 ∈ ℕ0) |
121 | 117, 120 | ffvelcdmd 7088 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {0, 1, 2}) → (𝐹‘𝑘) ∈ 𝐾) |
122 | 120, 34 | syldan 589 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {0, 1, 2}) → (𝑘 ↑ 𝑋) ∈ 𝐾) |
123 | 7, 11, 114, 121, 122 | ringcld 20235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {0, 1, 2}) → ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐾) |
124 | 123 | fmpttd 7118 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ {0, 1, 2} ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))):{0, 1, 2}⟶𝐾) |
125 | | fzofi 13985 |
. . . . . . 7
⊢ (0..^3)
∈ Fin |
126 | 75, 125 | eqeltrrdi 2835 |
. . . . . 6
⊢ (𝜑 → {0, 1, 2} ∈
Fin) |
127 | 124, 126,
36 | fidmfisupp 9406 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ {0, 1, 2} ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑅)) |
128 | 7, 18, 21, 113, 124, 127 | gsumcl 19906 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0, 1, 2} ↦
((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) ∈ 𝐾) |
129 | 7, 19, 18, 105, 128 | grpridd 18957 |
. . 3
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ {0, 1, 2} ↦
((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) + (0g‘𝑅)) = (𝑅 Σg (𝑘 ∈ {0, 1, 2} ↦
((𝐹‘𝑘) · (𝑘 ↑ 𝑋))))) |
130 | | fveq2 6890 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝐹‘𝑘) = (𝐹‘0)) |
131 | | evl1deg2.c |
. . . . . . 7
⊢ 𝐶 = (𝐹‘0) |
132 | 130, 131 | eqtr4di 2784 |
. . . . . 6
⊢ (𝑘 = 0 → (𝐹‘𝑘) = 𝐶) |
133 | | oveq1 7420 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑘 ↑ 𝑋) = (0 ↑ 𝑋)) |
134 | 132, 133 | oveq12d 7431 |
. . . . 5
⊢ (𝑘 = 0 → ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)) = (𝐶 · (0 ↑ 𝑋))) |
135 | | fveq2 6890 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
136 | | evl1deg2.b |
. . . . . . 7
⊢ 𝐵 = (𝐹‘1) |
137 | 135, 136 | eqtr4di 2784 |
. . . . . 6
⊢ (𝑘 = 1 → (𝐹‘𝑘) = 𝐵) |
138 | | oveq1 7420 |
. . . . . 6
⊢ (𝑘 = 1 → (𝑘 ↑ 𝑋) = (1 ↑ 𝑋)) |
139 | 137, 138 | oveq12d 7431 |
. . . . 5
⊢ (𝑘 = 1 → ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)) = (𝐵 · (1 ↑ 𝑋))) |
140 | | fveq2 6890 |
. . . . . . 7
⊢ (𝑘 = 2 → (𝐹‘𝑘) = (𝐹‘2)) |
141 | | evl1deg2.a |
. . . . . . 7
⊢ 𝐴 = (𝐹‘2) |
142 | 140, 141 | eqtr4di 2784 |
. . . . . 6
⊢ (𝑘 = 2 → (𝐹‘𝑘) = 𝐴) |
143 | | oveq1 7420 |
. . . . . 6
⊢ (𝑘 = 2 → (𝑘 ↑ 𝑋) = (2 ↑ 𝑋)) |
144 | 142, 143 | oveq12d 7431 |
. . . . 5
⊢ (𝑘 = 2 → ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)) = (𝐴 · (2 ↑ 𝑋))) |
145 | | 0nn0 12530 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
146 | 145 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℕ0) |
147 | | 1nn0 12531 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
148 | 147 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
149 | | 0ne1 12326 |
. . . . . 6
⊢ 0 ≠
1 |
150 | 149 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ≠ 1) |
151 | | 1ne2 12463 |
. . . . . 6
⊢ 1 ≠
2 |
152 | 151 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ≠ 2) |
153 | | 0ne2 12462 |
. . . . . 6
⊢ 0 ≠
2 |
154 | 153 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ≠ 2) |
155 | 13, 8, 6, 7 | coe1fvalcl 22195 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑈 ∧ 0 ∈ ℕ0) →
(𝐹‘0) ∈ 𝐾) |
156 | 10, 145, 155 | sylancl 584 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘0) ∈ 𝐾) |
157 | 131, 156 | eqeltrid 2830 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝐾) |
158 | 28, 12, 30, 146, 15 | mulgnn0cld 19082 |
. . . . . 6
⊢ (𝜑 → (0 ↑ 𝑋) ∈ 𝐾) |
159 | 7, 11, 20, 157, 158 | ringcld 20235 |
. . . . 5
⊢ (𝜑 → (𝐶 · (0 ↑ 𝑋)) ∈ 𝐾) |
160 | 13, 8, 6, 7 | coe1fvalcl 22195 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑈 ∧ 1 ∈ ℕ0) →
(𝐹‘1) ∈ 𝐾) |
161 | 10, 147, 160 | sylancl 584 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘1) ∈ 𝐾) |
162 | 136, 161 | eqeltrid 2830 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐾) |
163 | 28, 12, 30, 148, 15 | mulgnn0cld 19082 |
. . . . . 6
⊢ (𝜑 → (1 ↑ 𝑋) ∈ 𝐾) |
164 | 7, 11, 20, 162, 163 | ringcld 20235 |
. . . . 5
⊢ (𝜑 → (𝐵 · (1 ↑ 𝑋)) ∈ 𝐾) |
165 | 13, 8, 6, 7 | coe1fvalcl 22195 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑈 ∧ 2 ∈ ℕ0) →
(𝐹‘2) ∈ 𝐾) |
166 | 10, 44, 165 | sylancl 584 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘2) ∈ 𝐾) |
167 | 141, 166 | eqeltrid 2830 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝐾) |
168 | 28, 12, 30, 45, 15 | mulgnn0cld 19082 |
. . . . . 6
⊢ (𝜑 → (2 ↑ 𝑋) ∈ 𝐾) |
169 | 7, 11, 20, 167, 168 | ringcld 20235 |
. . . . 5
⊢ (𝜑 → (𝐴 · (2 ↑ 𝑋)) ∈ 𝐾) |
170 | 7, 19, 134, 139, 144, 21, 146, 148, 45, 150, 152, 154, 159, 164, 169 | gsumtp 32925 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0, 1, 2} ↦
((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) = (((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))) + (𝐴 · (2 ↑ 𝑋)))) |
171 | 7, 19, 105, 159, 164 | grpcld 18934 |
. . . . 5
⊢ (𝜑 → ((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))) ∈ 𝐾) |
172 | 7, 19 | cmncom 19789 |
. . . . 5
⊢ ((𝑅 ∈ CMnd ∧ ((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))) ∈ 𝐾 ∧ (𝐴 · (2 ↑ 𝑋)) ∈ 𝐾) → (((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))) + (𝐴 · (2 ↑ 𝑋))) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))))) |
173 | 21, 171, 169, 172 | syl3anc 1368 |
. . . 4
⊢ (𝜑 → (((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))) + (𝐴 · (2 ↑ 𝑋))) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))))) |
174 | 7, 19 | cmncom 19789 |
. . . . . . 7
⊢ ((𝑅 ∈ CMnd ∧ (𝐶 · (0 ↑ 𝑋)) ∈ 𝐾 ∧ (𝐵 · (1 ↑ 𝑋)) ∈ 𝐾) → ((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))) = ((𝐵 · (1 ↑ 𝑋)) + (𝐶 · (0 ↑ 𝑋)))) |
175 | 21, 159, 164, 174 | syl3anc 1368 |
. . . . . 6
⊢ (𝜑 → ((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))) = ((𝐵 · (1 ↑ 𝑋)) + (𝐶 · (0 ↑ 𝑋)))) |
176 | 28, 12 | mulg1 19068 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐾 → (1 ↑ 𝑋) = 𝑋) |
177 | 15, 176 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1 ↑ 𝑋) = 𝑋) |
178 | 177 | oveq2d 7429 |
. . . . . . 7
⊢ (𝜑 → (𝐵 · (1 ↑ 𝑋)) = (𝐵 · 𝑋)) |
179 | | eqid 2726 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
180 | 27, 179 | ringidval 20159 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (0g‘(mulGrp‘𝑅)) |
181 | 28, 180, 12 | mulg0 19061 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝐾 → (0 ↑ 𝑋) = (1r‘𝑅)) |
182 | 15, 181 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0 ↑ 𝑋) = (1r‘𝑅)) |
183 | 182 | oveq2d 7429 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 · (0 ↑ 𝑋)) = (𝐶 ·
(1r‘𝑅))) |
184 | 7, 11, 179, 20, 157 | ringridmd 20245 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ·
(1r‘𝑅)) =
𝐶) |
185 | 183, 184 | eqtrd 2766 |
. . . . . . 7
⊢ (𝜑 → (𝐶 · (0 ↑ 𝑋)) = 𝐶) |
186 | 178, 185 | oveq12d 7431 |
. . . . . 6
⊢ (𝜑 → ((𝐵 · (1 ↑ 𝑋)) + (𝐶 · (0 ↑ 𝑋))) = ((𝐵 · 𝑋) + 𝐶)) |
187 | 175, 186 | eqtrd 2766 |
. . . . 5
⊢ (𝜑 → ((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋))) = ((𝐵 · 𝑋) + 𝐶)) |
188 | 187 | oveq2d 7429 |
. . . 4
⊢ (𝜑 → ((𝐴 · (2 ↑ 𝑋)) + ((𝐶 · (0 ↑ 𝑋)) + (𝐵 · (1 ↑ 𝑋)))) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐵 · 𝑋) + 𝐶))) |
189 | 170, 173,
188 | 3eqtrd 2770 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ {0, 1, 2} ↦
((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐵 · 𝑋) + 𝐶))) |
190 | 111, 129,
189 | 3eqtrd 2770 |
. 2
⊢ (𝜑 → ((𝑅 Σg (𝑘 ∈ (0..^3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋)))) + (𝑅 Σg (𝑘 ∈
(ℤ≥‘3) ↦ ((𝐹‘𝑘) · (𝑘 ↑ 𝑋))))) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐵 · 𝑋) + 𝐶))) |
191 | 17, 73, 190 | 3eqtrd 2770 |
1
⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐵 · 𝑋) + 𝐶))) |