Step | Hyp | Ref
| Expression |
1 | | coe1tm.k |
. . . 4
⊢ 𝐾 = (Base‘𝑅) |
2 | | coe1tm.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
3 | | coe1tm.x |
. . . 4
⊢ 𝑋 = (var1‘𝑅) |
4 | | coe1tm.m |
. . . 4
⊢ · = (
·𝑠 ‘𝑃) |
5 | | coe1tm.n |
. . . 4
⊢ 𝑁 = (mulGrp‘𝑃) |
6 | | coe1tm.e |
. . . 4
⊢ ↑ =
(.g‘𝑁) |
7 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
8 | 1, 2, 3, 4, 5, 6, 7 | ply1tmcl 19463 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ (Base‘𝑃)) |
9 | | eqid 2610 |
. . . 4
⊢
(coe1‘(𝐶 · (𝐷 ↑ 𝑋))) = (coe1‘(𝐶 · (𝐷 ↑ 𝑋))) |
10 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ ℕ0
↦ (1𝑜 × {𝑥})) = (𝑥 ∈ ℕ0 ↦
(1𝑜 × {𝑥})) |
11 | 9, 7, 2, 10 | coe1fval2 19401 |
. . 3
⊢ ((𝐶 · (𝐷 ↑ 𝑋)) ∈ (Base‘𝑃) → (coe1‘(𝐶 · (𝐷 ↑ 𝑋))) = ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ0 ↦
(1𝑜 × {𝑥})))) |
12 | 8, 11 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
(coe1‘(𝐶
·
(𝐷 ↑ 𝑋))) = ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ0 ↦
(1𝑜 × {𝑥})))) |
13 | | fconst6g 6007 |
. . . . 5
⊢ (𝑥 ∈ ℕ0
→ (1𝑜 × {𝑥}):1𝑜⟶ℕ0) |
14 | | nn0ex 11175 |
. . . . . 6
⊢
ℕ0 ∈ V |
15 | | 1on 7454 |
. . . . . . 7
⊢
1𝑜 ∈ On |
16 | 15 | elexi 3186 |
. . . . . 6
⊢
1𝑜 ∈ V |
17 | 14, 16 | elmap 7772 |
. . . . 5
⊢
((1𝑜 × {𝑥}) ∈ (ℕ0
↑𝑚 1𝑜) ↔ (1𝑜
× {𝑥}):1𝑜⟶ℕ0) |
18 | 13, 17 | sylibr 223 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ (1𝑜 × {𝑥}) ∈ (ℕ0
↑𝑚 1𝑜)) |
19 | 18 | adantl 481 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (1𝑜 × {𝑥}) ∈ (ℕ0
↑𝑚 1𝑜)) |
20 | | eqidd 2611 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ ℕ0
↦ (1𝑜 × {𝑥})) = (𝑥 ∈ ℕ0 ↦
(1𝑜 × {𝑥}))) |
21 | | eqid 2610 |
. . . . . . . 8
⊢
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅))) =
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
22 | 5, 7 | mgpbas 18318 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘𝑁) |
23 | 22 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑃) =
(Base‘𝑁)) |
24 | | eqid 2610 |
. . . . . . . . . 10
⊢
(mulGrp‘(1𝑜 mPoly 𝑅)) = (mulGrp‘(1𝑜
mPoly 𝑅)) |
25 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(PwSer1‘𝑅) = (PwSer1‘𝑅) |
26 | 2, 25, 7 | ply1bas 19386 |
. . . . . . . . . 10
⊢
(Base‘𝑃) =
(Base‘(1𝑜 mPoly 𝑅)) |
27 | 24, 26 | mgpbas 18318 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑃) =
(Base‘(mulGrp‘(1𝑜 mPoly 𝑅)))) |
29 | | ssv 3588 |
. . . . . . . . 9
⊢
(Base‘𝑃)
⊆ V |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑃) ⊆
V) |
31 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑥(+g‘𝑁)𝑦) ∈ V |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+g‘𝑁)𝑦) ∈ V) |
33 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(.r‘𝑃) = (.r‘𝑃) |
34 | 5, 33 | mgpplusg 18316 |
. . . . . . . . . . 11
⊢
(.r‘𝑃) = (+g‘𝑁) |
35 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(1𝑜 mPoly 𝑅) = (1𝑜 mPoly 𝑅) |
36 | 2, 35, 33 | ply1mulr 19418 |
. . . . . . . . . . . 12
⊢
(.r‘𝑃) =
(.r‘(1𝑜 mPoly 𝑅)) |
37 | 24, 36 | mgpplusg 18316 |
. . . . . . . . . . 11
⊢
(.r‘𝑃) =
(+g‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
38 | 34, 37 | eqtr3i 2634 |
. . . . . . . . . 10
⊢
(+g‘𝑁) =
(+g‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
39 | 38 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(+g‘𝑁) =
(+g‘(mulGrp‘(1𝑜 mPoly 𝑅)))) |
40 | 39 | oveqdr 6573 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+g‘𝑁)𝑦) = (𝑥(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑦)) |
41 | 6, 21, 23, 28, 30, 32, 40 | mulgpropd 17407 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ↑ =
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅)))) |
42 | 41 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → ↑ =
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅)))) |
43 | | eqidd 2611 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝐷 = 𝐷) |
44 | 3 | vr1val 19383 |
. . . . . . 7
⊢ 𝑋 = ((1𝑜 mVar
𝑅)‘∅) |
45 | 44 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝑋 = ((1𝑜 mVar
𝑅)‘∅)) |
46 | 42, 43, 45 | oveq123d 6570 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐷 ↑ 𝑋) = (𝐷(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅))) |
47 | 46 | oveq2d 6565 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) = (𝐶 · (𝐷(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)))) |
48 | | psr1baslem 19376 |
. . . . . 6
⊢
(ℕ0 ↑𝑚 1𝑜) =
{𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑎 “ ℕ) ∈
Fin} |
49 | | coe1tm.z |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
50 | | eqid 2610 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
51 | 15 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
1𝑜 ∈ On) |
52 | | eqid 2610 |
. . . . . 6
⊢
(1𝑜 mVar 𝑅) = (1𝑜 mVar 𝑅) |
53 | | simp1 1054 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝑅 ∈ Ring) |
54 | | 0lt1o 7471 |
. . . . . . 7
⊢ ∅
∈ 1𝑜 |
55 | 54 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → ∅
∈ 1𝑜) |
56 | | simp3 1056 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝐷 ∈
ℕ0) |
57 | 35, 48, 49, 50, 51, 24, 21, 52, 53, 55, 56 | mplcoe3 19287 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑦 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑦 = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)),
(1r‘𝑅),
0 )) =
(𝐷(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅))) |
58 | 57 | oveq2d 6565 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝑦 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑦 = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)),
(1r‘𝑅),
0 ))) =
(𝐶 · (𝐷(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)))) |
59 | 2, 35, 4 | ply1vsca 19417 |
. . . . 5
⊢ · = (
·𝑠 ‘(1𝑜 mPoly 𝑅)) |
60 | | elsni 4142 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ {∅} → 𝑏 = ∅) |
61 | | df1o2 7459 |
. . . . . . . . . . 11
⊢
1𝑜 = {∅} |
62 | 60, 61 | eleq2s 2706 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 1𝑜
→ 𝑏 =
∅) |
63 | 62 | iftrued 4044 |
. . . . . . . . 9
⊢ (𝑏 ∈ 1𝑜
→ if(𝑏 = ∅,
𝐷, 0) = 𝐷) |
64 | 63 | adantl 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑏 ∈ 1𝑜)
→ if(𝑏 = ∅,
𝐷, 0) = 𝐷) |
65 | 64 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑏 ∈ 1𝑜
↦ if(𝑏 = ∅,
𝐷, 0)) = (𝑏 ∈ 1𝑜
↦ 𝐷)) |
66 | | fconstmpt 5085 |
. . . . . . 7
⊢
(1𝑜 × {𝐷}) = (𝑏 ∈ 1𝑜 ↦ 𝐷) |
67 | 65, 66 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑏 ∈ 1𝑜
↦ if(𝑏 = ∅,
𝐷, 0)) =
(1𝑜 × {𝐷})) |
68 | | fconst6g 6007 |
. . . . . . . 8
⊢ (𝐷 ∈ ℕ0
→ (1𝑜 × {𝐷}):1𝑜⟶ℕ0) |
69 | 14, 16 | elmap 7772 |
. . . . . . . 8
⊢
((1𝑜 × {𝐷}) ∈ (ℕ0
↑𝑚 1𝑜) ↔ (1𝑜
× {𝐷}):1𝑜⟶ℕ0) |
70 | 68, 69 | sylibr 223 |
. . . . . . 7
⊢ (𝐷 ∈ ℕ0
→ (1𝑜 × {𝐷}) ∈ (ℕ0
↑𝑚 1𝑜)) |
71 | 70 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
(1𝑜 × {𝐷}) ∈ (ℕ0
↑𝑚 1𝑜)) |
72 | 67, 71 | eqeltrd 2688 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑏 ∈ 1𝑜
↦ if(𝑏 = ∅,
𝐷, 0)) ∈
(ℕ0 ↑𝑚
1𝑜)) |
73 | | simp2 1055 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝐶 ∈ 𝐾) |
74 | 35, 59, 48, 50, 49, 1, 51, 53, 72, 73 | mplmon2 19314 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝑦 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑦 = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)),
(1r‘𝑅),
0 ))) =
(𝑦 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
if(𝑦 = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ))) |
75 | 47, 58, 74 | 3eqtr2d 2650 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) = (𝑦 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑦 = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ))) |
76 | | eqeq1 2614 |
. . . 4
⊢ (𝑦 = (1𝑜
× {𝑥}) → (𝑦 = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)) ↔
(1𝑜 × {𝑥}) = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)))) |
77 | 76 | ifbid 4058 |
. . 3
⊢ (𝑦 = (1𝑜
× {𝑥}) →
if(𝑦 = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ) =
if((1𝑜 × {𝑥}) = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 )) |
78 | 19, 20, 75, 77 | fmptco 6303 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ0 ↦
(1𝑜 × {𝑥}))) = (𝑥 ∈ ℕ0 ↦
if((1𝑜 × {𝑥}) = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ))) |
79 | 67 | adantr 480 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (𝑏 ∈
1𝑜 ↦ if(𝑏 = ∅, 𝐷, 0)) = (1𝑜 ×
{𝐷})) |
80 | 79 | eqeq2d 2620 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1𝑜 × {𝑥}) = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)) ↔
(1𝑜 × {𝑥}) = (1𝑜 × {𝐷}))) |
81 | | fveq1 6102 |
. . . . . . 7
⊢
((1𝑜 × {𝑥}) = (1𝑜 × {𝐷}) →
((1𝑜 × {𝑥})‘∅) = ((1𝑜
× {𝐷})‘∅)) |
82 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
83 | 82 | fvconst2 6374 |
. . . . . . . . 9
⊢ (∅
∈ 1𝑜 → ((1𝑜 × {𝑥})‘∅) = 𝑥) |
84 | 54, 83 | mp1i 13 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1𝑜 × {𝑥})‘∅) = 𝑥) |
85 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ 𝐷 ∈
ℕ0) |
86 | | fvconst2g 6372 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℕ0
∧ ∅ ∈ 1𝑜) → ((1𝑜
× {𝐷})‘∅)
= 𝐷) |
87 | 85, 54, 86 | sylancl 693 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1𝑜 × {𝐷})‘∅) = 𝐷) |
88 | 84, 87 | eqeq12d 2625 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (((1𝑜 × {𝑥})‘∅) = ((1𝑜
× {𝐷})‘∅)
↔ 𝑥 = 𝐷)) |
89 | 81, 88 | syl5ib 233 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1𝑜 × {𝑥}) = (1𝑜 × {𝐷}) → 𝑥 = 𝐷)) |
90 | | sneq 4135 |
. . . . . . 7
⊢ (𝑥 = 𝐷 → {𝑥} = {𝐷}) |
91 | 90 | xpeq2d 5063 |
. . . . . 6
⊢ (𝑥 = 𝐷 → (1𝑜 ×
{𝑥}) =
(1𝑜 × {𝐷})) |
92 | 89, 91 | impbid1 214 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1𝑜 × {𝑥}) = (1𝑜 × {𝐷}) ↔ 𝑥 = 𝐷)) |
93 | 80, 92 | bitrd 267 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1𝑜 × {𝑥}) = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)) ↔ 𝑥 = 𝐷)) |
94 | 93 | ifbid 4058 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ if((1𝑜 × {𝑥}) = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ) = if(𝑥 = 𝐷, 𝐶, 0 )) |
95 | 94 | mpteq2dva 4672 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ ℕ0
↦ if((1𝑜 × {𝑥}) = (𝑏 ∈ 1𝑜 ↦
if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 )) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 𝐷, 𝐶, 0 ))) |
96 | 12, 78, 95 | 3eqtrd 2648 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
(coe1‘(𝐶
·
(𝐷 ↑ 𝑋))) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 𝐷, 𝐶, 0 ))) |