Proof of Theorem gsummoncoe1fzo
Step | Hyp | Ref
| Expression |
1 | | gsummoncoe1fzo.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
2 | | eqid 2727 |
. . . . . . 7
⊢
(0g‘𝑃) = (0g‘𝑃) |
3 | | gsummoncoe1fzo.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | gsummoncoe1fzo.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
5 | 4 | ply1ring 22153 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
6 | 3, 5 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ Ring) |
7 | 6 | ringcmnd 20209 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ CMnd) |
8 | | nn0ex 12500 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℕ0 ∈
V) |
10 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → 𝑘 ∈ (ℕ0
∖ (0..^𝑁))) |
11 | 10 | eldifbd 3957 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → ¬
𝑘 ∈ (0..^𝑁)) |
12 | 11 | iffalsed 4535 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) = 0 ) |
13 | 12 | oveq1d 7429 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)) = ( 0 ∗ (𝑘 ↑ 𝑋))) |
14 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → 𝑅 ∈ Ring) |
15 | 10 | eldifad 3956 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → 𝑘 ∈
ℕ0) |
16 | | eqid 2727 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
17 | 16, 1 | mgpbas 20071 |
. . . . . . . . . . 11
⊢ 𝐵 =
(Base‘(mulGrp‘𝑃)) |
18 | | gsummoncoe1fzo.e |
. . . . . . . . . . 11
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
19 | 16 | ringmgp 20170 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
20 | 6, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd) |
21 | 20 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(mulGrp‘𝑃) ∈
Mnd) |
22 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
23 | | gsummoncoe1fzo.x |
. . . . . . . . . . . . . 14
⊢ 𝑋 = (var1‘𝑅) |
24 | 23, 4, 1 | vr1cl 22123 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
25 | 3, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
26 | 25 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
27 | 17, 18, 21, 22, 26 | mulgnn0cld 19041 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
28 | 15, 27 | syldan 590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
29 | | gsummoncoe1fzo.m |
. . . . . . . . . 10
⊢ ∗ = (
·𝑠 ‘𝑃) |
30 | | gsummoncoe1fzo.1 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑅) |
31 | 4, 1, 29, 30 | ply10s0 22162 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ( 0 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
32 | 14, 28, 31 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → ( 0 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
33 | 13, 32 | eqtrd 2767 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖
(0..^𝑁))) → (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
34 | | fzofi 13963 |
. . . . . . . 8
⊢
(0..^𝑁) ∈
Fin |
35 | 34 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0..^𝑁) ∈ Fin) |
36 | 4 | ply1lmod 22157 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
37 | 3, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ LMod) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod) |
39 | | gsummoncoe1fzo.a |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)𝐴 ∈ 𝐾) |
40 | 39 | r19.21bi 3243 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐴 ∈ 𝐾) |
41 | 40 | adantlr 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ∈ (0..^𝑁)) → 𝐴 ∈ 𝐾) |
42 | | gsummoncoe1fzo.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = (Base‘𝑅) |
43 | 42, 30 | ring0cl 20192 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐾) |
44 | 3, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ 𝐾) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (0..^𝑁)) → 0 ∈ 𝐾) |
46 | 41, 45 | ifclda 4559 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∈ 𝐾) |
47 | 4 | ply1sca 22158 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
48 | 3, 47 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
49 | 48 | fveq2d 6895 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
50 | 42, 49 | eqtrid 2779 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑃))) |
51 | 50 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐾 =
(Base‘(Scalar‘𝑃))) |
52 | 46, 51 | eleqtrd 2830 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∈
(Base‘(Scalar‘𝑃))) |
53 | | eqid 2727 |
. . . . . . . . 9
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
54 | | eqid 2727 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
55 | 1, 53, 29, 54 | lmodvscl 20750 |
. . . . . . . 8
⊢ ((𝑃 ∈ LMod ∧ if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∈
(Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
56 | 38, 52, 27, 55 | syl3anc 1369 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
57 | | fzo0ssnn0 13737 |
. . . . . . . 8
⊢
(0..^𝑁) ⊆
ℕ0 |
58 | 57 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0..^𝑁) ⊆
ℕ0) |
59 | 1, 2, 7, 9, 33, 35, 56, 58 | gsummptres2 32745 |
. . . . . 6
⊢ (𝜑 → (𝑃 Σg (𝑘 ∈ ℕ0
↦ (if(𝑘 ∈
(0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ (0..^𝑁) ↦ (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋))))) |
60 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ (0..^𝑁)) |
61 | 60 | iftrued 4532 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) = 𝐴) |
62 | 61 | oveq1d 7429 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)) = (𝐴 ∗ (𝑘 ↑ 𝑋))) |
63 | 62 | mpteq2dva 5242 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (0..^𝑁) ↦ (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋))) = (𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))) |
64 | 63 | oveq2d 7430 |
. . . . . 6
⊢ (𝜑 → (𝑃 Σg (𝑘 ∈ (0..^𝑁) ↦ (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋))))) |
65 | 59, 64 | eqtrd 2767 |
. . . . 5
⊢ (𝜑 → (𝑃 Σg (𝑘 ∈ ℕ0
↦ (if(𝑘 ∈
(0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋))))) |
66 | 65 | fveq2d 6895 |
. . . 4
⊢ (𝜑 →
(coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋))))) = (coe1‘(𝑃 Σg
(𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))) |
67 | 66 | fveq1d 6893 |
. . 3
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ((coe1‘(𝑃 Σg
(𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿)) |
68 | 46 | ralrimiva 3141 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∈ 𝐾) |
69 | | eqid 2727 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 ∈
(0..^𝑁), 𝐴, 0 )) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0..^𝑁), 𝐴, 0 )) |
70 | 69, 9, 35, 40, 44 | mptiffisupp 32457 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0..^𝑁), 𝐴, 0 )) finSupp 0
) |
71 | | gsummoncoe1fzo.l |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ (0..^𝑁)) |
72 | 57, 71 | sselid 3976 |
. . . 4
⊢ (𝜑 → 𝐿 ∈
ℕ0) |
73 | 4, 1, 23, 18, 3, 42, 29, 30, 68, 70, 72 | gsummoncoe1 22214 |
. . 3
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌if(𝑘 ∈ (0..^𝑁), 𝐴, 0 )) |
74 | 67, 73 | eqtr3d 2769 |
. 2
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌if(𝑘 ∈ (0..^𝑁), 𝐴, 0 )) |
75 | | eleq1 2816 |
. . . . 5
⊢ (𝑘 = 𝐿 → (𝑘 ∈ (0..^𝑁) ↔ 𝐿 ∈ (0..^𝑁))) |
76 | | gsummoncoe1fzo.2 |
. . . . 5
⊢ (𝑘 = 𝐿 → 𝐴 = 𝐶) |
77 | 75, 76 | ifbieq1d 4548 |
. . . 4
⊢ (𝑘 = 𝐿 → if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) = if(𝐿 ∈ (0..^𝑁), 𝐶, 0 )) |
78 | 77 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑘 = 𝐿) → if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) = if(𝐿 ∈ (0..^𝑁), 𝐶, 0 )) |
79 | 71, 78 | csbied 3927 |
. 2
⊢ (𝜑 → ⦋𝐿 / 𝑘⦌if(𝑘 ∈ (0..^𝑁), 𝐴, 0 ) = if(𝐿 ∈ (0..^𝑁), 𝐶, 0 )) |
80 | 71 | iftrued 4532 |
. 2
⊢ (𝜑 → if(𝐿 ∈ (0..^𝑁), 𝐶, 0 ) = 𝐶) |
81 | 74, 79, 80 | 3eqtrd 2771 |
1
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = 𝐶) |