mptcoe1fsupp

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

	Ref	Expression
Hypotheses	mptcoe1fsupp.p	$⊢ P = {Poly}_{1} (R)$
	mptcoe1fsupp.b	$⊢ B = {Base}_{P}$
	mptcoe1fsupp.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	mptcoe1fsupp	$⊢ (R \in Ring \land M \in B) \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ {coe}_{1} (M) (k)))$

Proof

Step	Hyp	Ref	Expression
1		mptcoe1fsupp.p	$⊢ P = {Poly}_{1} (R)$
2		mptcoe1fsupp.b	$⊢ B = {Base}_{P}$
3		mptcoe1fsupp.0	$⊢ \underset{˙}{0} = 0_{R}$
4	3	fvexi	$⊢ \underset{˙}{0} \in V$
5	4	a1i	$⊢ (R \in Ring \land M \in B) \to \underset{˙}{0} \in V$
6		eqid	$⊢ {coe}_{1} (M) = {coe}_{1} (M)$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	6 2 1 7	coe1fvalcl	$⊢ (M \in B \land k \in ℕ_{0}) \to {coe}_{1} (M) (k) \in {Base}_{R}$
9	8	adantll	$⊢ ((R \in Ring \land M \in B) \land k \in ℕ_{0}) \to {coe}_{1} (M) (k) \in {Base}_{R}$
10		simpr	$⊢ (R \in Ring \land M \in B) \to M \in B$
11	6 2 1 3 7	coe1fsupp	$⊢ M \in B \to {coe}_{1} (M) \in \{c \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (c)\}$
12		elrabi	$⊢ {coe}_{1} (M) \in \{c \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (c)\} \to {coe}_{1} (M) \in ({Base}_{R}^{ℕ_{0}})$
13	10 11 12	3syl	$⊢ (R \in Ring \land M \in B) \to {coe}_{1} (M) \in ({Base}_{R}^{ℕ_{0}})$
14	13 4	jctir	$⊢ (R \in Ring \land M \in B) \to ({coe}_{1} (M) \in ({Base}_{R}^{ℕ_{0}}) \land \underset{˙}{0} \in V)$
15	6 2 1 3	coe1sfi	$⊢ M \in B \to {finSupp}_{\underset{˙}{0}} ({coe}_{1} (M))$
16	15	adantl	$⊢ (R \in Ring \land M \in B) \to {finSupp}_{\underset{˙}{0}} ({coe}_{1} (M))$
17		fsuppmapnn0ub	$⊢ ({coe}_{1} (M) \in ({Base}_{R}^{ℕ_{0}}) \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ({coe}_{1} (M)) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (M) (x) = \underset{˙}{0}))$
18	14 16 17	sylc	$⊢ (R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (M) (x) = \underset{˙}{0})$
19		csbfv	$⊢ ⦋ x / k ⦌ {coe}_{1} (M) (k) = {coe}_{1} (M) (x)$
20		simpr	$⊢ (((((R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land s < x) \land {coe}_{1} (M) (x) = \underset{˙}{0}) \to {coe}_{1} (M) (x) = \underset{˙}{0}$
21	19 20	syl5eq	$⊢ (((((R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land s < x) \land {coe}_{1} (M) (x) = \underset{˙}{0}) \to ⦋ x / k ⦌ {coe}_{1} (M) (k) = \underset{˙}{0}$
22	21	exp31	$⊢ (((R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to (s < x \to ({coe}_{1} (M) (x) = \underset{˙}{0} \to ⦋ x / k ⦌ {coe}_{1} (M) (k) = \underset{˙}{0}))$
23	22	a2d	$⊢ (((R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to ((s < x \to {coe}_{1} (M) (x) = \underset{˙}{0}) \to (s < x \to ⦋ x / k ⦌ {coe}_{1} (M) (k) = \underset{˙}{0}))$
24	23	ralimdva	$⊢ ((R \in Ring \land M \in B) \land s \in ℕ_{0}) \to (\forall x \in ℕ_{0} (s < x \to {coe}_{1} (M) (x) = \underset{˙}{0}) \to \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ {coe}_{1} (M) (k) = \underset{˙}{0}))$
25	24	reximdva	$⊢ (R \in Ring \land M \in B) \to (\exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (M) (x) = \underset{˙}{0}) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ {coe}_{1} (M) (k) = \underset{˙}{0}))$
26	18 25	mpd	$⊢ (R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ {coe}_{1} (M) (k) = \underset{˙}{0})$
27	5 9 26	mptnn0fsupp	$⊢ (R \in Ring \land M \in B) \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ {coe}_{1} (M) (k)))$

Metamath Proof Explorer

Theorem mptcoe1fsupp

Proof