Theorem evl1fpws

Description: Evaluation of a univariate polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025)

	Ref	Expression
Hypotheses	evl1fpws.q	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	evl1fpws.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
	evl1fpws.b	$$⊢B={\mathrm{Base}}_R$$
	evl1fpws.u	$$⊢U={\mathrm{Base}}_W$$
	evl1fpws.s	$$⊢\phi \to R\in \mathrm{CRing}$$
	evl1fpws.y	$$⊢\phi \to M\in U$$
	evl1fpws.1	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	evl1fpws.2	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	evl1fpws.a	$$⊢A={\mathrm{coe}}_1\left(M\right)$$
Assertion	evl1fpws	$$⊢\phi \to O\left(M\right)=\left(x\in B⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_R}\left(A\left(k\right)\underset{\dot{}}{·}\left(k\underset{\dot{}}{\times }x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evl1fpws.q	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
2		evl1fpws.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
3		evl1fpws.b	$$⊢B={\mathrm{Base}}_R$$
4		evl1fpws.u	$$⊢U={\mathrm{Base}}_W$$
5		evl1fpws.s	$$⊢\phi \to R\in \mathrm{CRing}$$
6		evl1fpws.y	$$⊢\phi \to M\in U$$
7		evl1fpws.1	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		evl1fpws.2	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
9		evl1fpws.a	$$⊢A={\mathrm{coe}}_1\left(M\right)$$
10	1 3	evl1fval1	$$⊢O=R{\mathrm{evalSub}}_{1}B$$
11	10	fveq1i	$$⊢O\left(M\right)=\left(R{\mathrm{evalSub}}_{1}B\right)\left(M\right)$$
12		eqid	$$⊢R{\mathrm{evalSub}}_{1}B=R{\mathrm{evalSub}}_{1}B$$
13		eqid	$$⊢{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)$$
14		eqid	$$⊢R{\upharpoonright }_{𝑠}B=R{\upharpoonright }_{𝑠}B$$
15		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}$$
16	5	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
17	3	subrgid	$$⊢R\in \mathrm{Ring}\to B\in \mathrm{SubRing}\left(R\right)$$
18	16 17	syl	$$⊢\phi \to B\in \mathrm{SubRing}\left(R\right)$$
19	3	ressid	$$⊢R\in \mathrm{CRing}\to R{\upharpoonright }_{𝑠}B=R$$
20	5 19	syl	$$⊢\phi \to R{\upharpoonright }_{𝑠}B=R$$
21	20	fveq2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)={\mathrm{Poly}}_1\left(R\right)$$
22	21 2	eqtr4di	$$⊢\phi \to {\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)=W$$
23	22	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}={\mathrm{Base}}_W$$
24	23 4	eqtr4di	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}=U$$
25	6 24	eleqtrrd	$$⊢\phi \to M\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}$$
26	12 3 13 14 15 5 18 25 7 8 9	evls1fpws	$$⊢\phi \to \left(R{\mathrm{evalSub}}_{1}B\right)\left(M\right)=\left(x\in B⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_R}\left(A\left(k\right)\underset{\dot{}}{·}\left(k\underset{\dot{}}{\times }x\right)\right)\right)$$
27	11 26	eqtrid	$$⊢\phi \to O\left(M\right)=\left(x\in B⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_R}\left(A\left(k\right)\underset{\dot{}}{·}\left(k\underset{\dot{}}{\times }x\right)\right)\right)$$