Theorem evls1muld

Description: Univariate polynomial evaluation of a product of polynomials. (Contributed by Thierry Arnoux, 24-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ressply1evl2.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		ressply1evl2.k	$$⊢K={\mathrm{Base}}_S$$
3		ressply1evl2.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		ressply1evl2.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		ressply1evl2.b	$$⊢B={\mathrm{Base}}_W$$
6		evls1muld.1	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
7		evls1muld.2	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
8		evls1muld.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evls1muld.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		evls1muld.m	$$⊢\phi \to M\in B$$
11		evls1muld.n	$$⊢\phi \to N\in B$$
12		evls1muld.c	$$⊢\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	ressply1mul	$$⊢\left(\phi \wedge \left(M\in B\wedge N\in B\right)\right)\to M{\cdot }_{W}N=M{\cdot }_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
17	13 10 11 16	syl12anc	$$⊢\phi \to M{\cdot }_{W}N=M{\cdot }_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
18	6	oveqi	$$⊢M\underset{\dot{}}{\times }N=M{\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	ressmulr	$$⊢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	$$⊢M{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N=M{\cdot }_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
24	17 18 23	3eqtr4g	$$⊢\phi \to M\underset{\dot{}}{\times }N=M{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N$$
25	24	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{\times }N\right)={\mathrm{eval}}_1\left(S\right)\left(M{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N\right)$$
26	25	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{\times }N\right)\left(C\right)={\mathrm{eval}}_1\left(S\right)\left(M{\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(M\underset{\dot{}}{\times }N\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(M\underset{\dot{}}{\times }N\right)$$
30	4	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
31	3	ply1ring	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
32	9 30 31	3syl	$$⊢\phi \to W\in \mathrm{Ring}$$
33	5 6 32 10 11	ringcld	$$⊢\phi \to M\underset{\dot{}}{\times }N\in B$$
34	33	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(M\underset{\dot{}}{\times }N\right)={\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{\times }N\right)$$
35	29 34	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{\times }N\right)=Q\left(M\underset{\dot{}}{\times }N\right)$$
36	35	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{\times }N\right)\left(C\right)=Q\left(M\underset{\dot{}}{\times }N\right)\left(C\right)$$
37		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
38		eqid	$$⊢{\mathrm{PwSer}}_1\left(U\right)={\mathrm{PwSer}}_1\left(U\right)$$
39		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}$$
40	14 4 3 5 9 38 39 37	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
41		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)}$$
42	40 41	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
43	42 10	sseldd	$$⊢\phi \to M\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
44	28	fveq1d	$$⊢\phi \to Q\left(M\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(M\right)$$
45	10	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(M\right)={\mathrm{eval}}_1\left(S\right)\left(M\right)$$
46	44 45	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\right)=Q\left(M\right)$$
47	46	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\right)\left(C\right)=Q\left(M\right)\left(C\right)$$
48	43 47	jca	$$⊢\phi \to \left(M\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}\wedge {\mathrm{eval}}_1\left(S\right)\left(M\right)\left(C\right)=Q\left(M\right)\left(C\right)\right)$$
49	42 11	sseldd	$$⊢\phi \to N\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
50	28	fveq1d	$$⊢\phi \to Q\left(N\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(N\right)$$
51	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)$$
52	50 51	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(N\right)=Q\left(N\right)$$
53	52	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(N\right)\left(C\right)=Q\left(N\right)\left(C\right)$$
54	49 53	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)$$
55	27 14 2 37 8 12 48 54 20 7	evl1muld	$$⊢\phi \to \left(M{\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(M{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N\right)\left(C\right)=Q\left(M\right)\left(C\right)\underset{\dot{}}{·}Q\left(N\right)\left(C\right)\right)$$
56	55	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M{\cdot }_{{\mathrm{Poly}}_1\left(S\right)}N\right)\left(C\right)=Q\left(M\right)\left(C\right)\underset{\dot{}}{·}Q\left(N\right)\left(C\right)$$
57	26 36 56	3eqtr3d	$$⊢\phi \to Q\left(M\underset{\dot{}}{\times }N\right)\left(C\right)=Q\left(M\right)\left(C\right)\underset{\dot{}}{·}Q\left(N\right)\left(C\right)$$