Theorem evls1subd

Description: Univariate polynomial evaluation of a difference of polynomials. (Contributed by Thierry Arnoux, 25-Apr-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$$
	evls1subd.1	$$⊢D={-}_W$$
	evls1subd.2	$$⊢\underset{\dot{}}{-}={-}_S$$
	evls1subd.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1subd.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1subd.m	$$⊢\phi \to M\in B$$
	evls1subd.n	$$⊢\phi \to N\in B$$
	evls1subd.y	$$⊢\phi \to C\in K$$
Assertion	evls1subd	$$⊢\phi \to Q\left(MDN\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		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		evls1subd.1	$$⊢D={-}_W$$
7		evls1subd.2	$$⊢\underset{\dot{}}{-}={-}_S$$
8		evls1subd.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evls1subd.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		evls1subd.m	$$⊢\phi \to M\in B$$
11		evls1subd.n	$$⊢\phi \to N\in B$$
12		evls1subd.y	$$⊢\phi \to C\in K$$
13	6	oveqi	$$⊢MDN=M{-}_{W}N$$
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 10 11	ressply1sub	$$⊢\phi \to M{-}_{W}N=M{-}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
17	13 16	eqtrid	$$⊢\phi \to MDN=M{-}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
18	14 4 3 5	subrgply1	$$⊢R\in \mathrm{SubRing}\left(S\right)\to B\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(S\right)\right)$$
19		subrgsubg	$$⊢B\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(S\right)\right)\to B\in \mathrm{SubGrp}\left({\mathrm{Poly}}_1\left(S\right)\right)$$
20	9 18 19	3syl	$$⊢\phi \to B\in \mathrm{SubGrp}\left({\mathrm{Poly}}_1\left(S\right)\right)$$
21		eqid	$$⊢{-}_{{\mathrm{Poly}}_1\left(S\right)}={-}_{{\mathrm{Poly}}_1\left(S\right)}$$
22		eqid	$$⊢{-}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}={-}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}$$
23	21 15 22	subgsub	$$⊢\left(B\in \mathrm{SubGrp}\left({\mathrm{Poly}}_1\left(S\right)\right)\wedge M\in B\wedge N\in B\right)\to M{-}_{{\mathrm{Poly}}_1\left(S\right)}N=M{-}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
24	20 10 11 23	syl3anc	$$⊢\phi \to M{-}_{{\mathrm{Poly}}_1\left(S\right)}N=M{-}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
25	17 24	eqtr4d	$$⊢\phi \to MDN=M{-}_{{\mathrm{Poly}}_1\left(S\right)}N$$
26	25	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(MDN\right)={\mathrm{eval}}_1\left(S\right)\left(M{-}_{{\mathrm{Poly}}_1\left(S\right)}N\right)$$
27	26	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(MDN\right)\left(C\right)={\mathrm{eval}}_1\left(S\right)\left(M{-}_{{\mathrm{Poly}}_1\left(S\right)}N\right)\left(C\right)$$
28		eqid	$$⊢{\mathrm{eval}}_1\left(S\right)={\mathrm{eval}}_1\left(S\right)$$
29	1 2 3 4 5 28 8 9	ressply1evl	$$⊢\phi \to Q={{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B$$
30	29	fveq1d	$$⊢\phi \to Q\left(MDN\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(MDN\right)$$
31	4	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
32	3	ply1ring	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
33	9 31 32	3syl	$$⊢\phi \to W\in \mathrm{Ring}$$
34	33	ringgrpd	$$⊢\phi \to W\in \mathrm{Grp}$$
35	5 6	grpsubcl	$$⊢\left(W\in \mathrm{Grp}\wedge M\in B\wedge N\in B\right)\to MDN\in B$$
36	34 10 11 35	syl3anc	$$⊢\phi \to MDN\in B$$
37	36	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(MDN\right)={\mathrm{eval}}_1\left(S\right)\left(MDN\right)$$
38	30 37	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(MDN\right)=Q\left(MDN\right)$$
39	38	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(MDN\right)\left(C\right)=Q\left(MDN\right)\left(C\right)$$
40		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
41		eqid	$$⊢{\mathrm{PwSer}}_1\left(U\right)={\mathrm{PwSer}}_1\left(U\right)$$
42		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}$$
43	14 4 3 5 9 41 42 40	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
44		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)}$$
45	43 44	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
46	45 10	sseldd	$$⊢\phi \to M\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
47	29	fveq1d	$$⊢\phi \to Q\left(M\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(M\right)$$
48	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)$$
49	47 48	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\right)=Q\left(M\right)$$
50	49	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\right)\left(C\right)=Q\left(M\right)\left(C\right)$$
51	46 50	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)$$
52	45 11	sseldd	$$⊢\phi \to N\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
53	29	fveq1d	$$⊢\phi \to Q\left(N\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(N\right)$$
54	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)$$
55	53 54	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(N\right)=Q\left(N\right)$$
56	55	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(N\right)\left(C\right)=Q\left(N\right)\left(C\right)$$
57	52 56	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)$$
58	28 14 2 40 8 12 51 57 21 7	evl1subd	$$⊢\phi \to \left(M{-}_{{\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{-}_{{\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)$$
59	58	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M{-}_{{\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)$$
60	27 39 59	3eqtr3d	$$⊢\phi \to Q\left(MDN\right)\left(C\right)=Q\left(M\right)\left(C\right)\underset{\dot{}}{-}Q\left(N\right)\left(C\right)$$