Theorem evls1vsca

Description: Univariate polynomial evaluation of a scalar product of polynomials. (Contributed by Thierry Arnoux, 25-Feb-2025)

	Ref	Expression
Hypotheses	ressply1evl.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	ressply1evl.k	$$⊢K={\mathrm{Base}}_S$$
	ressply1evl.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	ressply1evl.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	ressply1evl.b	$$⊢B={\mathrm{Base}}_W$$
	evls1vsca.1	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
	evls1vsca.2	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	evls1vsca.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1vsca.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1vsca.m	$$⊢\phi \to A\in R$$
	evls1vsca.n	$$⊢\phi \to N\in B$$
	evls1vsca.y	$$⊢\phi \to C\in K$$
Assertion	evls1vsca	$$⊢\phi \to Q\left(A\underset{\dot{}}{\times }N\right)\left(C\right)=A\underset{\dot{}}{·}Q\left(N\right)\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		ressply1evl.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		ressply1evl.k	$$⊢K={\mathrm{Base}}_S$$
3		ressply1evl.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		ressply1evl.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		ressply1evl.b	$$⊢B={\mathrm{Base}}_W$$
6		evls1vsca.1	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
7		evls1vsca.2	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
8		evls1vsca.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evls1vsca.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		evls1vsca.m	$$⊢\phi \to A\in R$$
11		evls1vsca.n	$$⊢\phi \to N\in B$$
12		evls1vsca.y	$$⊢\phi \to C\in K$$
13		id	$$⊢\phi \to \phi$$
14		eqid	$$⊢{\mathrm{Poly}}_1\left(S\right)={\mathrm{Poly}}_1\left(S\right)$$
15		eqid	$$⊢{\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B={\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B$$
16	14 4 3 5 9 15	ressply1vsca	$$⊢\left(\phi \wedge \left(A\in R\wedge N\in B\right)\right)\to A{\cdot }_{W}N=A{\cdot }_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
17	13 10 11 16	syl12anc	$$⊢\phi \to A{\cdot }_{W}N=A{\cdot }_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
18	6	oveqi	$$⊢A\underset{\dot{}}{\times }N=A{\cdot }_{W}N$$
19	5	fvexi	$$⊢B\in \mathrm{V}$$
20		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}={\cdot }_{{\mathrm{Poly}}_1\left(S\right)}$$
21	15 20	ressvsca	$$⊢B\in \mathrm{V}\to {\cdot }_{{\mathrm{Poly}}_1\left(S\right)}={\cdot }_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}$$
22	19 21	ax-mp	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}={\cdot }_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}$$
23	22	oveqi	$$⊢A{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N=A{\cdot }_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
24	17 18 23	3eqtr4g	$$⊢\phi \to A\underset{\dot{}}{\times }N=A{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N$$
25	24	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(A\underset{\dot{}}{\times }N\right)={\mathrm{eval}}_1\left(S\right)\left(A{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N\right)$$
26	25	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(A\underset{\dot{}}{\times }N\right)\left(C\right)={\mathrm{eval}}_1\left(S\right)\left(A{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N\right)\left(C\right)$$
27		eqid	$$⊢{\mathrm{eval}}_1\left(S\right)={\mathrm{eval}}_1\left(S\right)$$
28	1 2 3 4 5 27 8 9	ressply1evl	$$⊢\phi \to Q={{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B$$
29	28	fveq1d	$$⊢\phi \to Q\left(A\underset{\dot{}}{\times }N\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(A\underset{\dot{}}{\times }N\right)$$
30	4	subrgcrng	$$⊢\left(S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to U\in \mathrm{CRing}$$
31	8 9 30	syl2anc	$$⊢\phi \to U\in \mathrm{CRing}$$
32		crngring	$$⊢U\in \mathrm{CRing}\to U\in \mathrm{Ring}$$
33	3	ply1lmod	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{LMod}$$
34	31 32 33	3syl	$$⊢\phi \to W\in \mathrm{LMod}$$
35	2	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq K$$
36	9 35	syl	$$⊢\phi \to R\subseteq K$$
37	4 2	ressbas2	$$⊢R\subseteq K\to R={\mathrm{Base}}_U$$
38	36 37	syl	$$⊢\phi \to R={\mathrm{Base}}_U$$
39	4	ovexi	$$⊢U\in \mathrm{V}$$
40	3	ply1sca	$$⊢U\in \mathrm{V}\to U=\mathrm{Scalar}\left(W\right)$$
41	39 40	mp1i	$$⊢\phi \to U=\mathrm{Scalar}\left(W\right)$$
42	41	fveq2d	$$⊢\phi \to {\mathrm{Base}}_U={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
43	38 42	eqtrd	$$⊢\phi \to R={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
44	10 43	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
45		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
46		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
47	5 45 6 46	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge N\in B\right)\to A\underset{\dot{}}{\times }N\in B$$
48	34 44 11 47	syl3anc	$$⊢\phi \to A\underset{\dot{}}{\times }N\in B$$
49	48	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(A\underset{\dot{}}{\times }N\right)={\mathrm{eval}}_1\left(S\right)\left(A\underset{\dot{}}{\times }N\right)$$
50	29 49	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(A\underset{\dot{}}{\times }N\right)=Q\left(A\underset{\dot{}}{\times }N\right)$$
51	50	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(A\underset{\dot{}}{\times }N\right)\left(C\right)=Q\left(A\underset{\dot{}}{\times }N\right)\left(C\right)$$
52		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
53		eqid	$$⊢{\mathrm{PwSer}}_1\left(U\right)={\mathrm{PwSer}}_1\left(U\right)$$
54		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}$$
55	14 4 3 5 9 53 54 52	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
56		inss2	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
57	55 56	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
58	57 11	sseldd	$$⊢\phi \to N\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
59	28	fveq1d	$$⊢\phi \to Q\left(N\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(N\right)$$
60	11	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(N\right)={\mathrm{eval}}_1\left(S\right)\left(N\right)$$
61	59 60	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(N\right)=Q\left(N\right)$$
62	61	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(N\right)\left(C\right)=Q\left(N\right)\left(C\right)$$
63	58 62	jca	$$⊢\phi \to \left(N\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}\wedge {\mathrm{eval}}_1\left(S\right)\left(N\right)\left(C\right)=Q\left(N\right)\left(C\right)\right)$$
64	36 10	sseldd	$$⊢\phi \to A\in K$$
65	27 14 2 52 8 12 63 64 20 7	evl1vsd	$$⊢\phi \to \left(A{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}\wedge {\mathrm{eval}}_1\left(S\right)\left(A{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N\right)\left(C\right)=A\underset{\dot{}}{·}Q\left(N\right)\left(C\right)\right)$$
66	65	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(A{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N\right)\left(C\right)=A\underset{\dot{}}{·}Q\left(N\right)\left(C\right)$$
67	26 51 66	3eqtr3d	$$⊢\phi \to Q\left(A\underset{\dot{}}{\times }N\right)\left(C\right)=A\underset{\dot{}}{·}Q\left(N\right)\left(C\right)$$