Metamath Proof Explorer


Theorem mptcoe1fsupp

Description: A mapping involving coefficients of polynomials is finitely supported. (Contributed by AV, 12-Oct-2019)

Ref Expression
Hypotheses mptcoe1fsupp.p 𝑃 = ( Poly1𝑅 )
mptcoe1fsupp.b 𝐵 = ( Base ‘ 𝑃 )
mptcoe1fsupp.0 0 = ( 0g𝑅 )
Assertion mptcoe1fsupp ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( coe1𝑀 ) ‘ 𝑘 ) ) finSupp 0 )

Proof

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 ‘ 𝑅 ) ↑m0 ) ∣ 𝑐 finSupp 0 } )
12 elrabi ( ( coe1𝑀 ) ∈ { 𝑐 ∈ ( ( Base ‘ 𝑅 ) ↑m0 ) ∣ 𝑐 finSupp 0 } → ( coe1𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m0 ) )
13 10 11 12 3syl ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( coe1𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m0 ) )
14 13 4 jctir ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( coe1𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m0 ) ∧ 0 ∈ V ) )
15 6 2 1 3 coe1sfi ( 𝑀𝐵 → ( coe1𝑀 ) finSupp 0 )
16 15 adantl ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( coe1𝑀 ) finSupp 0 )
17 fsuppmapnn0ub ( ( ( coe1𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m0 ) ∧ 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 )