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	5 3	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
14	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15	5	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑀 ∈ Mnd )
16	14 15	syl	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
17	16	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
18		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
19	2 1 3	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
20	19	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
21	13 6 17 18 20	mulgnn0cld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
22		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23	7 3 1 22	coe1f	⊢ ( 𝐾 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
24	23	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
25		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26	7 3 1 25	coe1sfi	⊢ ( 𝐾 ∈ 𝐵 → 𝐴 finSupp ( 0g ‘ 𝑅 ) )
27	26	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 finSupp ( 0g ‘ 𝑅 ) )
28	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
29	28	eqcomd	⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
30	29	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
31	30	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ 𝑅 ) )
32	27 31	breqtrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
33	3 8 4 10 12 21 24 32	mptscmfsuppd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )