Step | Hyp | Ref
| Expression |
1 | | gsummonply1.f |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴) finSupp 0 ) |
2 | | gsummonply1.a |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐴 ∈ 𝐾) |
3 | 2 | r19.21bi 2932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ 𝐾) |
4 | | eqid 2622 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ 𝐴) = (𝑘 ∈ ℕ0
↦ 𝐴) |
5 | 3, 4 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴):ℕ0⟶𝐾) |
6 | | gsummonply1.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝑅) |
7 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
8 | 6, 7 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐾 ∈ V |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ V) |
10 | | nn0ex 11298 |
. . . . . 6
⊢
ℕ0 ∈ V |
11 | | elmapg 7870 |
. . . . . 6
⊢ ((𝐾 ∈ V ∧
ℕ0 ∈ V) → ((𝑘 ∈ ℕ0 ↦ 𝐴) ∈ (𝐾 ↑𝑚
ℕ0) ↔ (𝑘 ∈ ℕ0 ↦ 𝐴):ℕ0⟶𝐾)) |
12 | 9, 10, 11 | sylancl 694 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ 𝐴) ∈ (𝐾 ↑𝑚
ℕ0) ↔ (𝑘 ∈ ℕ0 ↦ 𝐴):ℕ0⟶𝐾)) |
13 | 5, 12 | mpbird 247 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴) ∈ (𝐾 ↑𝑚
ℕ0)) |
14 | | gsummonply1.0 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
15 | | fvex 6201 |
. . . . 5
⊢
(0g‘𝑅) ∈ V |
16 | 14, 15 | eqeltri 2697 |
. . . 4
⊢ 0 ∈
V |
17 | | fsuppmapnn0ub 12795 |
. . . 4
⊢ (((𝑘 ∈ ℕ0
↦ 𝐴) ∈ (𝐾 ↑𝑚
ℕ0) ∧ 0 ∈ V) → ((𝑘 ∈ ℕ0
↦ 𝐴) finSupp 0 →
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 ))) |
18 | 13, 16, 17 | sylancl 694 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ 𝐴) finSupp 0 → ∃𝑠 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → ((𝑘 ∈ ℕ0
↦ 𝐴)‘𝑥) = 0 ))) |
19 | 1, 18 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 )) |
20 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ 𝑥 ∈
ℕ0) |
21 | 2 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ∀𝑘 ∈
ℕ0 𝐴
∈ 𝐾) |
22 | | rspcsbela 4006 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 𝐴
∈ 𝐾) →
⦋𝑥 / 𝑘⦌𝐴 ∈ 𝐾) |
23 | 20, 21, 22 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ⦋𝑥 /
𝑘⦌𝐴 ∈ 𝐾) |
24 | 4 | fvmpts 6285 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ0
∧ ⦋𝑥 /
𝑘⦌𝐴 ∈ 𝐾) → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = ⦋𝑥 / 𝑘⦌𝐴) |
25 | 20, 23, 24 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑘 ∈
ℕ0 ↦ 𝐴)‘𝑥) = ⦋𝑥 / 𝑘⦌𝐴) |
26 | 25 | eqeq1d 2624 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (((𝑘 ∈
ℕ0 ↦ 𝐴)‘𝑥) = 0 ↔
⦋𝑥 / 𝑘⦌𝐴 = 0 )) |
27 | 26 | imbi2d 330 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 ) ↔ (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ))) |
28 | 27 | biimpd 219 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 ) → (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ))) |
29 | 28 | ralimdva 2962 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → ((𝑘 ∈ ℕ0
↦ 𝐴)‘𝑥) = 0 ) → ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ))) |
30 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝜑 ∧ 𝑠 ∈ ℕ0) |
31 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘ℕ0 |
32 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘 𝑠 < 𝑥 |
33 | | nfcsb1v 3549 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐴 |
34 | 33 | nfeq1 2778 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐴 = 0 |
35 | 32, 34 | nfim 1825 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ) |
36 | 31, 35 | nfral 2945 |
. . . . . . . . . 10
⊢
Ⅎ𝑘∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ) |
37 | 30, 36 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) |
38 | | gsummonply1.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑃) |
39 | | eqid 2622 |
. . . . . . . . 9
⊢
(0g‘𝑃) = (0g‘𝑃) |
40 | | gsummonply1.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
41 | | gsummonply1.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Poly1‘𝑅) |
42 | 41 | ply1ring 19618 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
43 | | ringcmn 18581 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) |
44 | 40, 42, 43 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ CMnd) |
45 | 44 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → 𝑃 ∈ CMnd) |
46 | 40 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → 𝑅 ∈ Ring) |
47 | | simp3 1063 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → 𝐴 ∈ 𝐾) |
48 | | simp2 1062 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → 𝑘 ∈ ℕ0) |
49 | | gsummonply1.x |
. . . . . . . . . . . . . . 15
⊢ 𝑋 = (var1‘𝑅) |
50 | | gsummonply1.m |
. . . . . . . . . . . . . . 15
⊢ ∗ = (
·𝑠 ‘𝑃) |
51 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
52 | | gsummonply1.e |
. . . . . . . . . . . . . . 15
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
53 | 6, 41, 49, 50, 51, 52, 38 | ply1tmcl 19642 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0) → (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
54 | 46, 47, 48, 53 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
55 | 54 | 3expia 1267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 ∈ 𝐾 → (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵)) |
56 | 55 | ralimdva 2962 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑘 ∈ ℕ0
𝐴 ∈ 𝐾 → ∀𝑘 ∈ ℕ0 (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵)) |
57 | 2, 56 | mpd 15 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
58 | 57 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → ∀𝑘 ∈ ℕ0
(𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
59 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → 𝑠 ∈
ℕ0) |
60 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑠 < 𝑘 → ⦋𝑘 / 𝑘⦌𝐴 = 0 ) |
61 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (𝑠 < 𝑥 ↔ 𝑠 < 𝑘)) |
62 | | csbeq1 3536 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → ⦋𝑥 / 𝑘⦌𝐴 = ⦋𝑘 / 𝑘⦌𝐴) |
63 | 62 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (⦋𝑥 / 𝑘⦌𝐴 = 0 ↔
⦋𝑘 / 𝑘⦌𝐴 = 0 )) |
64 | 61, 63 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → ((𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ) ↔ (𝑠 < 𝑘 → ⦋𝑘 / 𝑘⦌𝐴 = 0 ))) |
65 | 35, 60, 64 | cbvral 3167 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) ↔ ∀𝑘 ∈ ℕ0
(𝑠 < 𝑘 → ⦋𝑘 / 𝑘⦌𝐴 = 0 )) |
66 | | csbid 3541 |
. . . . . . . . . . . . . . 15
⊢
⦋𝑘 /
𝑘⦌𝐴 = 𝐴 |
67 | 66 | eqeq1i 2627 |
. . . . . . . . . . . . . 14
⊢
(⦋𝑘 /
𝑘⦌𝐴 = 0 ↔ 𝐴 = 0 ) |
68 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = 0 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = ( 0 ∗ (𝑘 ↑ 𝑋))) |
69 | 41 | ply1sca 19623 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
70 | 40, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
71 | 70 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
72 | 14, 71 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 =
(0g‘(Scalar‘𝑃))) |
73 | 72 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 0
= (0g‘(Scalar‘𝑃))) |
74 | 73 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ( 0 ∗ (𝑘 ↑ 𝑋)) =
((0g‘(Scalar‘𝑃)) ∗ (𝑘 ↑ 𝑋))) |
75 | 41 | ply1lmod 19622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
76 | 40, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ LMod) |
77 | 76 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑃 ∈
LMod) |
78 | 51 | ringmgp 18553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
79 | 40, 42, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd) |
80 | 79 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (mulGrp‘𝑃)
∈ Mnd) |
81 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℕ0) |
82 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝑃) =
(Base‘𝑃) |
83 | 49, 41, 82 | vr1cl 19587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
84 | 40, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑃)) |
85 | 84 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑋 ∈
(Base‘𝑃)) |
86 | 51, 82 | mgpbas 18495 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
87 | 86, 52 | mulgnn0cl 17558 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((mulGrp‘𝑃)
∈ Mnd ∧ 𝑘 ∈
ℕ0 ∧ 𝑋
∈ (Base‘𝑃))
→ (𝑘 ↑ 𝑋) ∈ (Base‘𝑃)) |
88 | 80, 81, 85, 87 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ↑ 𝑋) ∈ (Base‘𝑃)) |
89 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
90 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
91 | 82, 89, 50, 90, 39 | lmod0vs 18896 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ LMod ∧ (𝑘 ↑ 𝑋) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃)) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
92 | 77, 88, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((0g‘(Scalar‘𝑃)) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
93 | 74, 92 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ( 0 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
94 | 68, 93 | sylan9eqr 2678 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝐴 = 0 ) →
(𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
95 | 94 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐴 = 0 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃))) |
96 | 67, 95 | syl5bi 232 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (⦋𝑘 /
𝑘⦌𝐴 = 0 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃))) |
97 | 96 | imim2d 57 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑠 < 𝑘 → ⦋𝑘 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝑘 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)))) |
98 | 97 | ralimdva 2962 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑘 ∈
ℕ0 (𝑠 <
𝑘 →
⦋𝑘 / 𝑘⦌𝐴 = 0 ) → ∀𝑘 ∈ ℕ0
(𝑠 < 𝑘 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)))) |
99 | 65, 98 | syl5bi 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) → ∀𝑘 ∈ ℕ0
(𝑠 < 𝑘 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)))) |
100 | 99 | imp 445 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → ∀𝑘 ∈ ℕ0
(𝑠 < 𝑘 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃))) |
101 | 37, 38, 39, 45, 58, 59, 100 | gsummptnn0fz 18382 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑃 Σg
(𝑘 ∈
ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋))))) |
102 | 101 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) →
(coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋))))) = (coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))) |
103 | 102 | fveq1d 6193 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ((coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿)) |
104 | 40 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → 𝑅 ∈ Ring) |
105 | | gsummonply1.l |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈
ℕ0) |
106 | 105 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → 𝐿 ∈
ℕ0) |
107 | | elfznn0 12433 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ0) |
108 | | simpll 790 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝜑) |
109 | 3 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈ 𝐾) |
110 | 108, 81, 109 | 3jca 1242 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝜑 ∧ 𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝐾)) |
111 | 107, 110 | sylan2 491 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → (𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾)) |
112 | 111, 54 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
113 | 112 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
∀𝑘 ∈ (0...𝑠)(𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
114 | 113 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → ∀𝑘 ∈ (0...𝑠)(𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
115 | | fzfid 12772 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (0...𝑠) ∈ Fin) |
116 | 41, 38, 104, 106, 114, 115 | coe1fzgsumd 19672 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) →
((coe1‘(𝑃
Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 ∗ (𝑘 ↑ 𝑋)))‘𝐿)))) |
117 | 40 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring) |
118 | 3 | expcom 451 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (𝜑 → 𝐴 ∈ 𝐾)) |
119 | 118, 107 | syl11 33 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ (0...𝑠) → 𝐴 ∈ 𝐾)) |
120 | 119 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑘 ∈ (0...𝑠) → 𝐴 ∈ 𝐾)) |
121 | 120 | imp 445 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝐴 ∈ 𝐾) |
122 | 107 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ0) |
123 | 14, 6, 41, 49, 50, 51, 52 | coe1tm 19643 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0) →
(coe1‘(𝐴
∗
(𝑘 ↑ 𝑋))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑘, 𝐴, 0 ))) |
124 | 117, 121,
122, 123 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → (coe1‘(𝐴 ∗ (𝑘 ↑ 𝑋))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑘, 𝐴, 0 ))) |
125 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝐿 → (𝑛 = 𝑘 ↔ 𝐿 = 𝑘)) |
126 | 125 | ifbid 4108 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝐿 → if(𝑛 = 𝑘, 𝐴, 0 ) = if(𝐿 = 𝑘, 𝐴, 0 )) |
127 | 126 | adantl 482 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑛 = 𝐿) → if(𝑛 = 𝑘, 𝐴, 0 ) = if(𝐿 = 𝑘, 𝐴, 0 )) |
128 | 105 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝐿 ∈
ℕ0) |
129 | 6, 14 | ring0cl 18569 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐾) |
130 | 40, 129 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ 𝐾) |
131 | 130 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 0 ∈ 𝐾) |
132 | 121, 131 | ifcld 4131 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐿 = 𝑘, 𝐴, 0 ) ∈ 𝐾) |
133 | 124, 127,
128, 132 | fvmptd 6288 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → ((coe1‘(𝐴 ∗ (𝑘 ↑ 𝑋)))‘𝐿) = if(𝐿 = 𝑘, 𝐴, 0 )) |
134 | 37, 133 | mpteq2da 4743 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 ∗ (𝑘 ↑ 𝑋)))‘𝐿)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) |
135 | 134 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
((coe1‘(𝐴
∗
(𝑘 ↑ 𝑋)))‘𝐿))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )))) |
136 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐿 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐿)) |
137 | | csbeq1 3536 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐿 → ⦋𝑥 / 𝑘⦌𝐴 = ⦋𝐿 / 𝑘⦌𝐴) |
138 | 137 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐿 → (⦋𝑥 / 𝑘⦌𝐴 = 0 ↔
⦋𝐿 / 𝑘⦌𝐴 = 0 )) |
139 | 136, 138 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐿 → ((𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ) ↔ (𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 ))) |
140 | 139 | rspcva 3307 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 )) |
141 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘(𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) |
142 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑘⦋𝐿 / 𝑘⦌𝐴 |
143 | 142 | nfeq1 2778 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘⦋𝐿 / 𝑘⦌𝐴 = 0 |
144 | 141, 143 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑘((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) |
145 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝑘 ≤ 𝑠)) |
146 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
147 | 146 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑘 ∈
ℝ) |
148 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑠 ∈ ℕ0
→ 𝑠 ∈
ℝ) |
149 | 148 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → 𝑠 ∈ ℝ) |
150 | 149 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑠 ∈
ℝ) |
151 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
152 | 151 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈
ℝ) |
153 | | lelttr 10128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿) → 𝑘 < 𝐿)) |
154 | 147, 150,
152, 153 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿) → 𝑘 < 𝐿)) |
155 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → 𝑘 < 𝐿) |
156 | 155 | olcd 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (𝐿 < 𝑘 ∨ 𝑘 < 𝐿)) |
157 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐿 ≠ 𝑘 ↔ ¬ 𝐿 = 𝑘) |
158 | 146 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → 𝑘 ∈ ℝ) |
159 | | lttri2 10120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐿 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐿 ≠ 𝑘 ↔ (𝐿 < 𝑘 ∨ 𝑘 < 𝐿))) |
160 | 151, 158,
159 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿 ≠ 𝑘 ↔ (𝐿 < 𝑘 ∨ 𝑘 < 𝐿))) |
161 | 160 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (𝐿 ≠ 𝑘 ↔ (𝐿 < 𝑘 ∨ 𝑘 < 𝐿))) |
162 | 157, 161 | syl5bbr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (¬ 𝐿 = 𝑘 ↔ (𝐿 < 𝑘 ∨ 𝑘 < 𝐿))) |
163 | 156, 162 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → ¬ 𝐿 = 𝑘) |
164 | 163 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑘 < 𝐿 → ¬ 𝐿 = 𝑘)) |
165 | 154, 164 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿) → ¬ 𝐿 = 𝑘)) |
166 | 165 | exp4b 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝐿 ∈ ℕ0 → (𝑘 ≤ 𝑠 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
167 | 166 | expimpd 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑘 ∈ ℕ0
→ ((𝑠 ∈
ℕ0 ∧ 𝐿
∈ ℕ0) → (𝑘 ≤ 𝑠 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
168 | 167 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑘 ∈ ℕ0
→ (𝑘 ≤ 𝑠 → ((𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
169 | 168 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑘 ∈ ℕ0
∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))) |
170 | 169 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0 ∧ 𝑘
≤ 𝑠) → ((𝑠 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))) |
171 | 145, 170 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))) |
172 | 171 | expd 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈ (0...𝑠) → (𝑠 ∈ ℕ0 → (𝐿 ∈ ℕ0
→ (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
173 | 105, 172 | syl7 74 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ (0...𝑠) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
174 | 173 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 ∈ ℕ0
→ (𝑘 ∈ (0...𝑠) → (𝜑 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
175 | 174 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 ∈ ℕ0
→ (𝑠 < 𝐿 → (𝜑 → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘)))) |
176 | 175 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 ∈ ℕ0
∧ 𝑠 < 𝐿) → (𝜑 → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘))) |
177 | 176 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘)) |
178 | 177 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘)) |
179 | 178 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐿 = 𝑘) |
180 | 179 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐿 = 𝑘, 𝐴, 0 ) = 0 ) |
181 | 144, 180 | mpteq2da 4743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )) = (𝑘 ∈ (0...𝑠) ↦ 0 )) |
182 | 181 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 ))) |
183 | | ringmnd 18556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
184 | 40, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ∈ Mnd) |
185 | 184 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) → 𝑅 ∈ Mnd) |
186 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(0...𝑠) ∈
V |
187 | 14 | gsumz 17374 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 ) |
188 | 185, 186,
187 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 ) |
189 | 188 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 ) |
190 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(⦋𝐿 /
𝑘⦌𝐴 = 0 →
⦋𝐿 / 𝑘⦌𝐴 = 0 ) |
191 | 190 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(⦋𝐿 /
𝑘⦌𝐴 = 0 → 0 = ⦋𝐿 / 𝑘⦌𝐴) |
192 | 191 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → 0 =
⦋𝐿 / 𝑘⦌𝐴) |
193 | 182, 189,
192 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴) |
194 | 193 | ex 450 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) → (⦋𝐿 / 𝑘⦌𝐴 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)) |
195 | 194 | expr 643 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (𝑠 < 𝐿 → (⦋𝐿 / 𝑘⦌𝐴 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴))) |
196 | 195 | a2d 29 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → ((𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴))) |
197 | 196 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑠 ∈ ℕ0 → ((𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)))) |
198 | 197 | com13 88 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑠 ∈ ℕ0
→ (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)))) |
199 | 140, 198 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑠 ∈ ℕ0
→ (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)))) |
200 | 199 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) → (𝑠 ∈ ℕ0
→ (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴))))) |
201 | 200 | com24 95 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ ℕ0
→ (𝜑 → (𝑠 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴))))) |
202 | 105, 201 | mpcom 38 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ ℕ0 →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)))) |
203 | 202 | imp31 448 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)) |
204 | 203 | com12 32 |
. . . . . . . 8
⊢ (𝑠 < 𝐿 → (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)) |
205 | | pm3.2 463 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (¬
𝑠 < 𝐿 → ((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿))) |
206 | 205 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (¬ 𝑠 < 𝐿 → ((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿))) |
207 | 184 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → 𝑅 ∈ Mnd) |
208 | 186 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → (0...𝑠) ∈ V) |
209 | 105 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ ℝ) |
210 | | lenlt 10116 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿)) |
211 | 209, 148,
210 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿)) |
212 | 105 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝐿 ≤ 𝑠) → 𝐿 ∈
ℕ0) |
213 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝐿 ≤ 𝑠) → 𝑠 ∈ ℕ0) |
214 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝐿 ≤ 𝑠) → 𝐿 ≤ 𝑠) |
215 | | elfz2nn0 12431 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ (0...𝑠) ↔ (𝐿 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝐿 ≤ 𝑠)) |
216 | 212, 213,
214, 215 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝐿 ≤ 𝑠) → 𝐿 ∈ (0...𝑠)) |
217 | 216 | ex 450 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (𝐿 ≤ 𝑠 → 𝐿 ∈ (0...𝑠))) |
218 | 211, 217 | sylbird 250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (¬
𝑠 < 𝐿 → 𝐿 ∈ (0...𝑠))) |
219 | 218 | imp 445 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → 𝐿 ∈ (0...𝑠)) |
220 | | eqcom 2629 |
. . . . . . . . . . . 12
⊢ (𝐿 = 𝑘 ↔ 𝑘 = 𝐿) |
221 | | ifbi 4107 |
. . . . . . . . . . . 12
⊢ ((𝐿 = 𝑘 ↔ 𝑘 = 𝐿) → if(𝐿 = 𝑘, 𝐴, 0 ) = if(𝑘 = 𝐿, 𝐴, 0 )) |
222 | 220, 221 | ax-mp 5 |
. . . . . . . . . . 11
⊢ if(𝐿 = 𝑘, 𝐴, 0 ) = if(𝑘 = 𝐿, 𝐴, 0 ) |
223 | 222 | mpteq2i 4741 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐿, 𝐴, 0 )) |
224 | 3, 6 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (Base‘𝑅)) |
225 | 224 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ ℕ0 → 𝐴 ∈ (Base‘𝑅))) |
226 | 225 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (𝑘 ∈ ℕ0
→ 𝐴 ∈
(Base‘𝑅))) |
227 | 107, 226 | syl5com 31 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑠) → ((𝜑 ∧ 𝑠 ∈ ℕ0) → 𝐴 ∈ (Base‘𝑅))) |
228 | 227 | impcom 446 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → 𝐴 ∈ (Base‘𝑅)) |
229 | 228 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
∀𝑘 ∈ (0...𝑠)𝐴 ∈ (Base‘𝑅)) |
230 | 229 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → ∀𝑘 ∈ (0...𝑠)𝐴 ∈ (Base‘𝑅)) |
231 | 14, 207, 208, 219, 223, 230 | gsummpt1n0 18364 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴) |
232 | 206, 231 | syl6com 37 |
. . . . . . . 8
⊢ (¬
𝑠 < 𝐿 → (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)) |
233 | 204, 232 | pm2.61i 176 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴) |
234 | 135, 233 | eqtrd 2656 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
((coe1‘(𝐴
∗
(𝑘 ↑ 𝑋)))‘𝐿))) = ⦋𝐿 / 𝑘⦌𝐴) |
235 | 103, 116,
234 | 3eqtrd 2660 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴) |
236 | 235 | ex 450 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴)) |
237 | 29, 236 | syld 47 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → ((𝑘 ∈ ℕ0
↦ 𝐴)‘𝑥) = 0 ) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴)) |
238 | 237 | rexlimdva 3031 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 ) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴)) |
239 | 19, 238 | mpd 15 |
1
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴) |