Step | Hyp | Ref
| Expression |
1 | | gsummonply1.f |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴) finSupp 0 ) |
2 | | gsummonply1.a |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐴 ∈ 𝐾) |
3 | 2 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ 𝐾) |
4 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ 𝐴) = (𝑘 ∈ ℕ0
↦ 𝐴) |
5 | 3, 4 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴):ℕ0⟶𝐾) |
6 | | gsummonply1.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝑅) |
7 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
8 | 6, 7 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐾 ∈ V |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ V) |
10 | | nn0ex 11175 |
. . . . . 6
⊢
ℕ0 ∈ V |
11 | | elmapg 7757 |
. . . . . 6
⊢ ((𝐾 ∈ V ∧
ℕ0 ∈ V) → ((𝑘 ∈ ℕ0 ↦ 𝐴) ∈ (𝐾 ↑𝑚
ℕ0) ↔ (𝑘 ∈ ℕ0 ↦ 𝐴):ℕ0⟶𝐾)) |
12 | 9, 10, 11 | sylancl 693 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ 𝐴) ∈ (𝐾 ↑𝑚
ℕ0) ↔ (𝑘 ∈ ℕ0 ↦ 𝐴):ℕ0⟶𝐾)) |
13 | 5, 12 | mpbird 246 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴) ∈ (𝐾 ↑𝑚
ℕ0)) |
14 | | gsummonply1.0 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
15 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝑅) ∈ V |
16 | 14, 15 | eqeltri 2684 |
. . . 4
⊢ 0 ∈
V |
17 | | fsuppmapnn0ub 12657 |
. . . 4
⊢ (((𝑘 ∈ ℕ0
↦ 𝐴) ∈ (𝐾 ↑𝑚
ℕ0) ∧ 0 ∈ V) → ((𝑘 ∈ ℕ0
↦ 𝐴) finSupp 0 →
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 ))) |
18 | 13, 16, 17 | sylancl 693 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ 𝐴) finSupp 0 → ∃𝑠 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → ((𝑘 ∈ ℕ0
↦ 𝐴)‘𝑥) = 0 ))) |
19 | 1, 18 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 )) |
20 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ 𝑥 ∈
ℕ0) |
21 | 2 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ∀𝑘 ∈
ℕ0 𝐴
∈ 𝐾) |
22 | | rspcsbela 3958 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 𝐴
∈ 𝐾) →
⦋𝑥 / 𝑘⦌𝐴 ∈ 𝐾) |
23 | 20, 21, 22 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ⦋𝑥 /
𝑘⦌𝐴 ∈ 𝐾) |
24 | 4 | fvmpts 6194 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ0
∧ ⦋𝑥 /
𝑘⦌𝐴 ∈ 𝐾) → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = ⦋𝑥 / 𝑘⦌𝐴) |
25 | 20, 23, 24 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑘 ∈
ℕ0 ↦ 𝐴)‘𝑥) = ⦋𝑥 / 𝑘⦌𝐴) |
26 | 25 | eqeq1d 2612 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (((𝑘 ∈
ℕ0 ↦ 𝐴)‘𝑥) = 0 ↔
⦋𝑥 / 𝑘⦌𝐴 = 0 )) |
27 | 26 | imbi2d 329 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 ) ↔ (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ))) |
28 | 27 | biimpd 218 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 ) → (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ))) |
29 | 28 | ralimdva 2945 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → ((𝑘 ∈ ℕ0
↦ 𝐴)‘𝑥) = 0 ) → ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ))) |
30 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝜑 ∧ 𝑠 ∈ ℕ0) |
31 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘ℕ0 |
32 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘 𝑠 < 𝑥 |
33 | | nfcsb1v 3515 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐴 |
34 | 33 | nfeq1 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐴 = 0 |
35 | 32, 34 | nfim 1813 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ) |
36 | 31, 35 | nfral 2929 |
. . . . . . . . . 10
⊢
Ⅎ𝑘∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ) |
37 | 30, 36 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) |
38 | | gsummonply1.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑃) |
39 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑃) = (0g‘𝑃) |
40 | | gsummonply1.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
41 | | gsummonply1.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Poly1‘𝑅) |
42 | 41 | ply1ring 19439 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
43 | | ringcmn 18404 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) |
44 | 40, 42, 43 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ CMnd) |
45 | 44 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → 𝑃 ∈ CMnd) |
46 | 40 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → 𝑅 ∈ Ring) |
47 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → 𝐴 ∈ 𝐾) |
48 | | simp2 1055 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → 𝑘 ∈ ℕ0) |
49 | | gsummonply1.x |
. . . . . . . . . . . . . . 15
⊢ 𝑋 = (var1‘𝑅) |
50 | | gsummonply1.m |
. . . . . . . . . . . . . . 15
⊢ ∗ = (
·𝑠 ‘𝑃) |
51 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
52 | | gsummonply1.e |
. . . . . . . . . . . . . . 15
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
53 | 6, 41, 49, 50, 51, 52, 38 | ply1tmcl 19463 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0) → (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
54 | 46, 47, 48, 53 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
55 | 54 | 3expia 1259 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 ∈ 𝐾 → (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵)) |
56 | 55 | ralimdva 2945 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑘 ∈ ℕ0
𝐴 ∈ 𝐾 → ∀𝑘 ∈ ℕ0 (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵)) |
57 | 2, 56 | mpd 15 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
58 | 57 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → ∀𝑘 ∈ ℕ0
(𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
59 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → 𝑠 ∈
ℕ0) |
60 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑠 < 𝑘 → ⦋𝑘 / 𝑘⦌𝐴 = 0 ) |
61 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (𝑠 < 𝑥 ↔ 𝑠 < 𝑘)) |
62 | | csbeq1 3502 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → ⦋𝑥 / 𝑘⦌𝐴 = ⦋𝑘 / 𝑘⦌𝐴) |
63 | 62 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (⦋𝑥 / 𝑘⦌𝐴 = 0 ↔
⦋𝑘 / 𝑘⦌𝐴 = 0 )) |
64 | 61, 63 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → ((𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ) ↔ (𝑠 < 𝑘 → ⦋𝑘 / 𝑘⦌𝐴 = 0 ))) |
65 | 35, 60, 64 | cbvral 3143 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) ↔ ∀𝑘 ∈ ℕ0
(𝑠 < 𝑘 → ⦋𝑘 / 𝑘⦌𝐴 = 0 )) |
66 | | csbid 3507 |
. . . . . . . . . . . . . . 15
⊢
⦋𝑘 /
𝑘⦌𝐴 = 𝐴 |
67 | 66 | eqeq1i 2615 |
. . . . . . . . . . . . . 14
⊢
(⦋𝑘 /
𝑘⦌𝐴 = 0 ↔ 𝐴 = 0 ) |
68 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = 0 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = ( 0 ∗ (𝑘 ↑ 𝑋))) |
69 | 41 | ply1sca 19444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
70 | 40, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
71 | 70 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
72 | 14, 71 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 =
(0g‘(Scalar‘𝑃))) |
73 | 72 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 0
= (0g‘(Scalar‘𝑃))) |
74 | 73 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ( 0 ∗ (𝑘 ↑ 𝑋)) =
((0g‘(Scalar‘𝑃)) ∗ (𝑘 ↑ 𝑋))) |
75 | 41 | ply1lmod 19443 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
76 | 40, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ LMod) |
77 | 76 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑃 ∈
LMod) |
78 | 51 | ringmgp 18376 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
79 | 40, 42, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd) |
80 | 79 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (mulGrp‘𝑃)
∈ Mnd) |
81 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℕ0) |
82 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝑃) =
(Base‘𝑃) |
83 | 49, 41, 82 | vr1cl 19408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
84 | 40, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑃)) |
85 | 84 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑋 ∈
(Base‘𝑃)) |
86 | 51, 82 | mgpbas 18318 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
87 | 86, 52 | mulgnn0cl 17381 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((mulGrp‘𝑃)
∈ Mnd ∧ 𝑘 ∈
ℕ0 ∧ 𝑋
∈ (Base‘𝑃))
→ (𝑘 ↑ 𝑋) ∈ (Base‘𝑃)) |
88 | 80, 81, 85, 87 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ↑ 𝑋) ∈ (Base‘𝑃)) |
89 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
90 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
91 | 82, 89, 50, 90, 39 | lmod0vs 18719 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ LMod ∧ (𝑘 ↑ 𝑋) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃)) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
92 | 77, 88, 91 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((0g‘(Scalar‘𝑃)) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
93 | 74, 92 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ( 0 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
94 | 68, 93 | sylan9eqr 2666 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝐴 = 0 ) →
(𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)) |
95 | 94 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐴 = 0 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃))) |
96 | 67, 95 | syl5bi 231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (⦋𝑘 /
𝑘⦌𝐴 = 0 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃))) |
97 | 96 | imim2d 55 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑠 < 𝑘 → ⦋𝑘 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝑘 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)))) |
98 | 97 | ralimdva 2945 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑘 ∈
ℕ0 (𝑠 <
𝑘 →
⦋𝑘 / 𝑘⦌𝐴 = 0 ) → ∀𝑘 ∈ ℕ0
(𝑠 < 𝑘 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)))) |
99 | 65, 98 | syl5bi 231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) → ∀𝑘 ∈ ℕ0
(𝑠 < 𝑘 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃)))) |
100 | 99 | imp 444 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → ∀𝑘 ∈ ℕ0
(𝑠 < 𝑘 → (𝐴 ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑃))) |
101 | 37, 38, 39, 45, 58, 59, 100 | gsummptnn0fz 18205 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑃 Σg
(𝑘 ∈
ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋))))) |
102 | 101 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) →
(coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋))))) = (coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))) |
103 | 102 | fveq1d 6105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ((coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿)) |
104 | 40 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → 𝑅 ∈ Ring) |
105 | | gsummonply1.l |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈
ℕ0) |
106 | 105 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → 𝐿 ∈
ℕ0) |
107 | | elfznn0 12302 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ0) |
108 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝜑) |
109 | 3 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈ 𝐾) |
110 | 108, 81, 109 | 3jca 1235 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝜑 ∧ 𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝐾)) |
111 | 107, 110 | sylan2 490 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → (𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾)) |
112 | 111, 54 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → (𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
113 | 112 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
∀𝑘 ∈ (0...𝑠)(𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
114 | 113 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → ∀𝑘 ∈ (0...𝑠)(𝐴 ∗ (𝑘 ↑ 𝑋)) ∈ 𝐵) |
115 | | fzfid 12634 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (0...𝑠) ∈ Fin) |
116 | 41, 38, 104, 106, 114, 115 | coe1fzgsumd 19493 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) →
((coe1‘(𝑃
Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 ∗ (𝑘 ↑ 𝑋)))‘𝐿)))) |
117 | 40 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring) |
118 | 3 | expcom 450 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (𝜑 → 𝐴 ∈ 𝐾)) |
119 | 107, 118 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...𝑠) → (𝜑 → 𝐴 ∈ 𝐾)) |
120 | 119 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ (0...𝑠) → 𝐴 ∈ 𝐾)) |
121 | 120 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑘 ∈ (0...𝑠) → 𝐴 ∈ 𝐾)) |
122 | 121 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝐴 ∈ 𝐾) |
123 | 107 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ0) |
124 | 14, 6, 41, 49, 50, 51, 52 | coe1tm 19464 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0) →
(coe1‘(𝐴
∗
(𝑘 ↑ 𝑋))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑘, 𝐴, 0 ))) |
125 | 117, 122,
123, 124 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → (coe1‘(𝐴 ∗ (𝑘 ↑ 𝑋))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑘, 𝐴, 0 ))) |
126 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝐿 → (𝑛 = 𝑘 ↔ 𝐿 = 𝑘)) |
127 | 126 | ifbid 4058 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝐿 → if(𝑛 = 𝑘, 𝐴, 0 ) = if(𝐿 = 𝑘, 𝐴, 0 )) |
128 | 127 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑛 = 𝐿) → if(𝑛 = 𝑘, 𝐴, 0 ) = if(𝐿 = 𝑘, 𝐴, 0 )) |
129 | 105 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝐿 ∈
ℕ0) |
130 | 6, 14 | ring0cl 18392 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐾) |
131 | 40, 130 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ 𝐾) |
132 | 131 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 0 ∈ 𝐾) |
133 | 122, 132 | ifcld 4081 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐿 = 𝑘, 𝐴, 0 ) ∈ 𝐾) |
134 | 125, 128,
129, 133 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → ((coe1‘(𝐴 ∗ (𝑘 ↑ 𝑋)))‘𝐿) = if(𝐿 = 𝑘, 𝐴, 0 )) |
135 | 37, 134 | mpteq2da 4671 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 ∗ (𝑘 ↑ 𝑋)))‘𝐿)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) |
136 | 135 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
((coe1‘(𝐴
∗
(𝑘 ↑ 𝑋)))‘𝐿))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )))) |
137 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐿 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐿)) |
138 | | csbeq1 3502 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐿 → ⦋𝑥 / 𝑘⦌𝐴 = ⦋𝐿 / 𝑘⦌𝐴) |
139 | 138 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐿 → (⦋𝑥 / 𝑘⦌𝐴 = 0 ↔
⦋𝐿 / 𝑘⦌𝐴 = 0 )) |
140 | 137, 139 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐿 → ((𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐴 = 0 ) ↔ (𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 ))) |
141 | 140 | rspcva 3280 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 )) |
142 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘(𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) |
143 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑘⦋𝐿 / 𝑘⦌𝐴 |
144 | 143 | nfeq1 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘⦋𝐿 / 𝑘⦌𝐴 = 0 |
145 | 142, 144 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑘((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) |
146 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝑘 ≤ 𝑠)) |
147 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
148 | 147 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑘 ∈
ℝ) |
149 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑠 ∈ ℕ0
→ 𝑠 ∈
ℝ) |
150 | 149 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → 𝑠 ∈ ℝ) |
151 | 150 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑠 ∈
ℝ) |
152 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
153 | 152 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈
ℝ) |
154 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿) → 𝑘 < 𝐿)) |
155 | 148, 151,
153, 154 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿) → 𝑘 < 𝐿)) |
156 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → 𝑘 < 𝐿) |
157 | 156 | olcd 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (𝐿 < 𝑘 ∨ 𝑘 < 𝐿)) |
158 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐿 ≠ 𝑘 ↔ ¬ 𝐿 = 𝑘) |
159 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → 𝑘 ∈ ℝ) |
160 | | lttri2 9999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐿 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐿 ≠ 𝑘 ↔ (𝐿 < 𝑘 ∨ 𝑘 < 𝐿))) |
161 | 152, 159,
160 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿 ≠ 𝑘 ↔ (𝐿 < 𝑘 ∨ 𝑘 < 𝐿))) |
162 | 161 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (𝐿 ≠ 𝑘 ↔ (𝐿 < 𝑘 ∨ 𝑘 < 𝐿))) |
163 | 158, 162 | syl5bbr 273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (¬ 𝐿 = 𝑘 ↔ (𝐿 < 𝑘 ∨ 𝑘 < 𝐿))) |
164 | 157, 163 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → ¬ 𝐿 = 𝑘) |
165 | 164 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑘 < 𝐿 → ¬ 𝐿 = 𝑘)) |
166 | 155, 165 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿) → ¬ 𝐿 = 𝑘)) |
167 | 166 | exp4b 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝐿 ∈ ℕ0 → (𝑘 ≤ 𝑠 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
168 | 167 | expimpd 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑘 ∈ ℕ0
→ ((𝑠 ∈
ℕ0 ∧ 𝐿
∈ ℕ0) → (𝑘 ≤ 𝑠 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
169 | 168 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑘 ∈ ℕ0
→ (𝑘 ≤ 𝑠 → ((𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
170 | 169 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑘 ∈ ℕ0
∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))) |
171 | 170 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0 ∧ 𝑘
≤ 𝑠) → ((𝑠 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))) |
172 | 146, 171 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))) |
173 | 172 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈ (0...𝑠) → (𝑠 ∈ ℕ0 → (𝐿 ∈ ℕ0
→ (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
174 | 105, 173 | syl7 72 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ (0...𝑠) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
175 | 174 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 ∈ ℕ0
→ (𝑘 ∈ (0...𝑠) → (𝜑 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))) |
176 | 175 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 ∈ ℕ0
→ (𝑠 < 𝐿 → (𝜑 → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘)))) |
177 | 176 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 ∈ ℕ0
∧ 𝑠 < 𝐿) → (𝜑 → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘))) |
178 | 177 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘)) |
179 | 178 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘)) |
180 | 179 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐿 = 𝑘) |
181 | 180 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐿 = 𝑘, 𝐴, 0 ) = 0 ) |
182 | 145, 181 | mpteq2da 4671 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )) = (𝑘 ∈ (0...𝑠) ↦ 0 )) |
183 | 182 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 ))) |
184 | | ringmnd 18379 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
185 | 40, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ∈ Mnd) |
186 | 185 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) → 𝑅 ∈ Mnd) |
187 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(0...𝑠) ∈
V |
188 | 14 | gsumz 17197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 ) |
189 | 186, 187,
188 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 ) |
190 | 189 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 ) |
191 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(⦋𝐿 /
𝑘⦌𝐴 = 0 →
⦋𝐿 / 𝑘⦌𝐴 = 0 ) |
192 | 191 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(⦋𝐿 /
𝑘⦌𝐴 = 0 → 0 = ⦋𝐿 / 𝑘⦌𝐴) |
193 | 192 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → 0 =
⦋𝐿 / 𝑘⦌𝐴) |
194 | 183, 190,
193 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) ∧ ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴) |
195 | 194 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿)) → (⦋𝐿 / 𝑘⦌𝐴 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)) |
196 | 195 | expr 641 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (𝑠 < 𝐿 → (⦋𝐿 / 𝑘⦌𝐴 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴))) |
197 | 196 | a2d 29 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → ((𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴))) |
198 | 197 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑠 ∈ ℕ0 → ((𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)))) |
199 | 198 | com13 86 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 < 𝐿 → ⦋𝐿 / 𝑘⦌𝐴 = 0 ) → (𝑠 ∈ ℕ0
→ (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)))) |
200 | 141, 199 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑠 ∈ ℕ0
→ (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)))) |
201 | 200 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) → (𝑠 ∈ ℕ0
→ (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴))))) |
202 | 201 | com24 93 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ ℕ0
→ (𝜑 → (𝑠 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴))))) |
203 | 105, 202 | mpcom 37 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ ℕ0 →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)))) |
204 | 203 | imp31 447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)) |
205 | 204 | com12 32 |
. . . . . . . 8
⊢ (𝑠 < 𝐿 → (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)) |
206 | | pm3.2 462 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (¬
𝑠 < 𝐿 → ((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿))) |
207 | 206 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (¬ 𝑠 < 𝐿 → ((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿))) |
208 | 185 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → 𝑅 ∈ Mnd) |
209 | 187 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → (0...𝑠) ∈ V) |
210 | 105 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ ℝ) |
211 | | lenlt 9995 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿)) |
212 | 210, 149,
211 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿)) |
213 | 105 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝐿 ≤ 𝑠) → 𝐿 ∈
ℕ0) |
214 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝐿 ≤ 𝑠) → 𝑠 ∈ ℕ0) |
215 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝐿 ≤ 𝑠) → 𝐿 ≤ 𝑠) |
216 | | elfz2nn0 12300 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ (0...𝑠) ↔ (𝐿 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝐿 ≤ 𝑠)) |
217 | 213, 214,
215, 216 | syl3anbrc 1239 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝐿 ≤ 𝑠) → 𝐿 ∈ (0...𝑠)) |
218 | 217 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (𝐿 ≤ 𝑠 → 𝐿 ∈ (0...𝑠))) |
219 | 212, 218 | sylbird 249 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (¬
𝑠 < 𝐿 → 𝐿 ∈ (0...𝑠))) |
220 | 219 | imp 444 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → 𝐿 ∈ (0...𝑠)) |
221 | | eqcom 2617 |
. . . . . . . . . . . 12
⊢ (𝐿 = 𝑘 ↔ 𝑘 = 𝐿) |
222 | | ifbi 4057 |
. . . . . . . . . . . 12
⊢ ((𝐿 = 𝑘 ↔ 𝑘 = 𝐿) → if(𝐿 = 𝑘, 𝐴, 0 ) = if(𝑘 = 𝐿, 𝐴, 0 )) |
223 | 221, 222 | ax-mp 5 |
. . . . . . . . . . 11
⊢ if(𝐿 = 𝑘, 𝐴, 0 ) = if(𝑘 = 𝐿, 𝐴, 0 ) |
224 | 223 | mpteq2i 4669 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐿, 𝐴, 0 )) |
225 | 3, 6 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (Base‘𝑅)) |
226 | 225 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ ℕ0 → 𝐴 ∈ (Base‘𝑅))) |
227 | 226 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → (𝑘 ∈ ℕ0
→ 𝐴 ∈
(Base‘𝑅))) |
228 | 107, 227 | syl5com 31 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑠) → ((𝜑 ∧ 𝑠 ∈ ℕ0) → 𝐴 ∈ (Base‘𝑅))) |
229 | 228 | impcom 445 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → 𝐴 ∈ (Base‘𝑅)) |
230 | 229 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
∀𝑘 ∈ (0...𝑠)𝐴 ∈ (Base‘𝑅)) |
231 | 230 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → ∀𝑘 ∈ (0...𝑠)𝐴 ∈ (Base‘𝑅)) |
232 | 14, 208, 209, 220, 224, 231 | gsummpt1n0 18187 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ ¬
𝑠 < 𝐿) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴) |
233 | 207, 232 | syl6com 36 |
. . . . . . . 8
⊢ (¬
𝑠 < 𝐿 → (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴)) |
234 | 205, 233 | pm2.61i 175 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = ⦋𝐿 / 𝑘⦌𝐴) |
235 | 136, 234 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
((coe1‘(𝐴
∗
(𝑘 ↑ 𝑋)))‘𝐿))) = ⦋𝐿 / 𝑘⦌𝐴) |
236 | 103, 116,
235 | 3eqtrd 2648 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 )) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴) |
237 | 236 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐴 = 0 ) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴)) |
238 | 29, 237 | syld 46 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → ((𝑘 ∈ ℕ0
↦ 𝐴)‘𝑥) = 0 ) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴)) |
239 | 238 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((𝑘 ∈ ℕ0 ↦ 𝐴)‘𝑥) = 0 ) →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴)) |
240 | 19, 239 | mpd 15 |
1
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴) |