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	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 )