Theorem evls1addd

Description: Univariate polynomial evaluation of a sum of polynomials. (Contributed by Thierry Arnoux, 8-Feb-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$$
	evls1addd.1	$$⊢\underset{\dot{}}{⨣}={+}_W$$
	evls1addd.2	$$⊢\underset{\dot{}}{+}={+}_S$$
	evls1addd.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1addd.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1addd.m	$$⊢\phi \to M\in B$$
	evls1addd.n	$$⊢\phi \to N\in B$$
	evls1addd.y	$$⊢\phi \to C\in K$$
Assertion	evls1addd	$$⊢\phi \to Q\left(M\underset{\dot{}}{⨣}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		evls1addd.1	$$⊢\underset{\dot{}}{⨣}={+}_W$$
7		evls1addd.2	$$⊢\underset{\dot{}}{+}={+}_S$$
8		evls1addd.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evls1addd.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		evls1addd.m	$$⊢\phi \to M\in B$$
11		evls1addd.n	$$⊢\phi \to N\in B$$
12		evls1addd.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	ressply1add	$$⊢\left(\phi \wedge \left(M\in B\wedge N\in B\right)\right)\to M{+}_{W}N=M{+}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
17	13 10 11 16	syl12anc	$$⊢\phi \to M{+}_{W}N=M{+}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
18	6	oveqi	$$⊢M\underset{\dot{}}{⨣}N=M{+}_{W}N$$
19	5	fvexi	$$⊢B\in \mathrm{V}$$
20		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(S\right)}={+}_{{\mathrm{Poly}}_1\left(S\right)}$$
21	15 20	ressplusg	$$⊢B\in \mathrm{V}\to {+}_{{\mathrm{Poly}}_1\left(S\right)}={+}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}$$
22	19 21	ax-mp	$$⊢{+}_{{\mathrm{Poly}}_1\left(S\right)}={+}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}$$
23	22	oveqi	$$⊢M{+}_{{\mathrm{Poly}}_1\left(S\right)}N=M{+}_{\left({\mathrm{Poly}}_1\left(S\right){\upharpoonright }_{𝑠}B\right)}N$$
24	17 18 23	3eqtr4g	$$⊢\phi \to M\underset{\dot{}}{⨣}N=M{+}_{{\mathrm{Poly}}_1\left(S\right)}N$$
25	24	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{⨣}N\right)={\mathrm{eval}}_1\left(S\right)\left(M{+}_{{\mathrm{Poly}}_1\left(S\right)}N\right)$$
26	25	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{⨣}N\right)\left(C\right)={\mathrm{eval}}_1\left(S\right)\left(M{+}_{{\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{}}{⨣}N\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(M\underset{\dot{}}{⨣}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	32	ringgrpd	$$⊢\phi \to W\in \mathrm{Grp}$$
34	5 6 33 10 11	grpcld	$$⊢\phi \to M\underset{\dot{}}{⨣}N\in B$$
35	34	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(M\underset{\dot{}}{⨣}N\right)={\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{⨣}N\right)$$
36	29 35	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{⨣}N\right)=Q\left(M\underset{\dot{}}{⨣}N\right)$$
37	36	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\underset{\dot{}}{⨣}N\right)\left(C\right)=Q\left(M\underset{\dot{}}{⨣}N\right)\left(C\right)$$
38		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
39		eqid	$$⊢{\mathrm{PwSer}}_1\left(U\right)={\mathrm{PwSer}}_1\left(U\right)$$
40		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}$$
41	14 4 3 5 9 39 40 38	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
42		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)}$$
43	41 42	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
44	43 10	sseldd	$$⊢\phi \to M\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
45	28	fveq1d	$$⊢\phi \to Q\left(M\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(M\right)$$
46	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)$$
47	45 46	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\right)=Q\left(M\right)$$
48	47	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(M\right)\left(C\right)=Q\left(M\right)\left(C\right)$$
49	44 48	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)$$
50	43 11	sseldd	$$⊢\phi \to N\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
51	28	fveq1d	$$⊢\phi \to Q\left(N\right)=\left({{\mathrm{eval}}_1\left(S\right)\upharpoonright }_B\right)\left(N\right)$$
52	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)$$
53	51 52	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(N\right)=Q\left(N\right)$$
54	53	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left(N\right)\left(C\right)=Q\left(N\right)\left(C\right)$$
55	50 54	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)$$
56	27 14 2 38 8 12 49 55 20 7	evl1addd	$$⊢\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)$$
57	56	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)$$
58	26 37 57	3eqtr3d	$$⊢\phi \to Q\left(M\underset{\dot{}}{⨣}N\right)\left(C\right)=Q\left(M\right)\left(C\right)\underset{\dot{}}{+}Q\left(N\right)\left(C\right)$$