Theorem 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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1coefsupp.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1coefsupp.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1coefsupp.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
	ply1coefsupp.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
	ply1coefsupp.e	⊢ ↑ = ( .g ‘ 𝑀 )
	ply1coefsupp.a	⊢ 𝐴 = ( coe1 ‘ 𝐾 )
Assertion	ply1coefsupp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1coefsupp.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1coefsupp.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		ply1coefsupp.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		ply1coefsupp.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
5		ply1coefsupp.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
6		ply1coefsupp.e	⊢ ↑ = ( .g ‘ 𝑀 )
7		ply1coefsupp.a	⊢ 𝐴 = ( coe1 ‘ 𝐾 )
8		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
9	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
10	9	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝑃 ∈ LMod )
11		nn0ex	⊢ ℕ0 ∈ V
12	11	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ℕ0 ∈ V )
13	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
14	5	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑀 ∈ Mnd )
15	13 14	syl	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
16	15	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
17		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
18	2 1 3	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
19	18	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
20	5 3	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
21	20 6	mulgnn0cl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
22	16 17 19 21	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
23		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24	7 3 1 23	coe1f	⊢ ( 𝐾 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
25	24	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
26		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
27	7 3 1 26	coe1sfi	⊢ ( 𝐾 ∈ 𝐵 → 𝐴 finSupp ( 0g ‘ 𝑅 ) )
28	27	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 finSupp ( 0g ‘ 𝑅 ) )
29	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
30	29	eqcomd	⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
31	30	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
32	31	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ 𝑅 ) )
33	28 32	breqtrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
34	3 8 4 10 12 22 25 33	mptscmfsuppd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )