This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑅 ) ↑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 eqtrid ⊢ ( ( ( ( ( ( 𝑅 ∈ 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 )