ply1coefsupp

Description: The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe . (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 8-Aug-2019)

	Ref	Expression
Hypotheses	ply1coefsupp.p	$⊢ P = {Poly}_{1} (R)$
	ply1coefsupp.x	$⊢ X = {var}_{1} (R)$
	ply1coefsupp.b	$⊢ B = {Base}_{P}$
	ply1coefsupp.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	ply1coefsupp.m	$⊢ M = {mulGrp}_{P}$
	ply1coefsupp.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
	ply1coefsupp.a	$⊢ A = {coe}_{1} (K)$
Assertion	ply1coefsupp	$⊢ (R \in Ring \land K \in B) \to {finSupp}_{0_{P}} ((k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)))$

Proof

Step	Hyp	Ref	Expression
1		ply1coefsupp.p	$⊢ P = {Poly}_{1} (R)$
2		ply1coefsupp.x	$⊢ X = {var}_{1} (R)$
3		ply1coefsupp.b	$⊢ B = {Base}_{P}$
4		ply1coefsupp.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		ply1coefsupp.m	$⊢ M = {mulGrp}_{P}$
6		ply1coefsupp.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
7		ply1coefsupp.a	$⊢ A = {coe}_{1} (K)$
8		eqid	$⊢ Scalar (P) = Scalar (P)$
9	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
10	9	adantr	$⊢ (R \in Ring \land K \in B) \to P \in LMod$
11		nn0ex	$⊢ ℕ_{0} \in V$
12	11	a1i	$⊢ (R \in Ring \land K \in B) \to ℕ_{0} \in V$
13	5 3	mgpbas	$⊢ B = {Base}_{M}$
14	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
15	5	ringmgp	$⊢ P \in Ring \to M \in Mnd$
16	14 15	syl	$⊢ R \in Ring \to M \in Mnd$
17	16	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to M \in Mnd$
18		simpr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
19	2 1 3	vr1cl	$⊢ R \in Ring \to X \in B$
20	19	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to X \in B$
21	13 6 17 18 20	mulgnn0cld	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in B$
22		eqid	$⊢ {Base}_{R} = {Base}_{R}$
23	7 3 1 22	coe1f	$⊢ K \in B \to A : ℕ_{0} ⟶ {Base}_{R}$
24	23	adantl	$⊢ (R \in Ring \land K \in B) \to A : ℕ_{0} ⟶ {Base}_{R}$
25		eqid	$⊢ 0_{R} = 0_{R}$
26	7 3 1 25	coe1sfi	$⊢ K \in B \to {finSupp}_{0_{R}} (A)$
27	26	adantl	$⊢ (R \in Ring \land K \in B) \to {finSupp}_{0_{R}} (A)$
28	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
29	28	eqcomd	$⊢ R \in Ring \to Scalar (P) = R$
30	29	adantr	$⊢ (R \in Ring \land K \in B) \to Scalar (P) = R$
31	30	fveq2d	$⊢ (R \in Ring \land K \in B) \to 0_{Scalar (P)} = 0_{R}$
32	27 31	breqtrrd	$⊢ (R \in Ring \land K \in B) \to {finSupp}_{0_{Scalar (P)}} (A)$
33	3 8 4 10 12 21 24 32	mptscmfsuppd	$⊢ (R \in Ring \land K \in B) \to {finSupp}_{0_{P}} ((k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem ply1coefsupp

Proof