Step |
Hyp |
Ref |
Expression |
1 |
|
mptcoe1fsupp.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
2 |
|
mptcoe1fsupp.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
3 |
|
mptcoe1fsupp.0 |
⊢ 0 = ( 0g ‘ 𝑅 ) |
4 |
3
|
fvexi |
⊢ 0 ∈ V |
5 |
4
|
a1i |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 0 ∈ V ) |
6 |
|
eqid |
⊢ ( coe1 ‘ 𝑀 ) = ( coe1 ‘ 𝑀 ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
8 |
6 2 1 7
|
coe1fvalcl |
⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) ) |
9 |
8
|
adantll |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) ) |
10 |
|
simpr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 ) |
11 |
6 2 1 3 7
|
coe1fsupp |
⊢ ( 𝑀 ∈ 𝐵 → ( coe1 ‘ 𝑀 ) ∈ { 𝑐 ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ∣ 𝑐 finSupp 0 } ) |
12 |
|
elrabi |
⊢ ( ( coe1 ‘ 𝑀 ) ∈ { 𝑐 ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ∣ 𝑐 finSupp 0 } → ( coe1 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ) |
13 |
10 11 12
|
3syl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( coe1 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ) |
14 |
13 4
|
jctir |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ∧ 0 ∈ V ) ) |
15 |
6 2 1 3
|
coe1sfi |
⊢ ( 𝑀 ∈ 𝐵 → ( coe1 ‘ 𝑀 ) finSupp 0 ) |
16 |
15
|
adantl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( coe1 ‘ 𝑀 ) finSupp 0 ) |
17 |
|
fsuppmapnn0ub |
⊢ ( ( ( coe1 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ∧ 0 ∈ V ) → ( ( coe1 ‘ 𝑀 ) finSupp 0 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 ) ) ) |
18 |
14 16 17
|
sylc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 ) ) |
19 |
|
csbfv |
⊢ ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) |
20 |
|
simpr |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑠 < 𝑥 ) ∧ ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 ) → ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 ) |
21 |
19 20
|
syl5eq |
⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑠 < 𝑥 ) ∧ ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 ) → ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) = 0 ) |
22 |
21
|
exp31 |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑠 < 𝑥 → ( ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 → ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) = 0 ) ) ) |
23 |
22
|
a2d |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 ) → ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) = 0 ) ) ) |
24 |
23
|
ralimdva |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) = 0 ) ) ) |
25 |
24
|
reximdva |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑀 ) ‘ 𝑥 ) = 0 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) = 0 ) ) ) |
26 |
18 25
|
mpd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) = 0 ) ) |
27 |
5 9 26
|
mptnn0fsupp |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑀 ) ‘ 𝑘 ) ) finSupp 0 ) |