Theorem evladdval

Description: Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025)

	Ref	Expression
Hypotheses	evladdval.q	$$⊢Q=I\mathrm{eval}S$$
	evladdval.p	$$⊢P=I\mathrm{mPoly}S$$
	evladdval.k	$$⊢K={\mathrm{Base}}_S$$
	evladdval.b	$$⊢B={\mathrm{Base}}_P$$
	evladdval.g	$$⊢\underset{\dot{}}{✚}={+}_P$$
	evladdval.f	$$⊢\underset{\dot{}}{+}={+}_S$$
	evladdval.i	$$⊢\phi \to I\in Z$$
	evladdval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evladdval.a	$$⊢\phi \to A\in \left(K^I\right)$$
	evladdval.m	$$⊢\phi \to \left(M\in B\wedge Q\left(M\right)\left(A\right)=V\right)$$
	evladdval.n	$$⊢\phi \to \left(N\in B\wedge Q\left(N\right)\left(A\right)=W\right)$$
Assertion	evladdval	$$⊢\phi \to \left(M\underset{\dot{}}{✚}N\in B\wedge Q\left(M\underset{\dot{}}{✚}N\right)\left(A\right)=V\underset{\dot{}}{+}W\right)$$

Proof

Step	Hyp	Ref	Expression
1		evladdval.q	$$⊢Q=I\mathrm{eval}S$$
2		evladdval.p	$$⊢P=I\mathrm{mPoly}S$$
3		evladdval.k	$$⊢K={\mathrm{Base}}_S$$
4		evladdval.b	$$⊢B={\mathrm{Base}}_P$$
5		evladdval.g	$$⊢\underset{\dot{}}{✚}={+}_P$$
6		evladdval.f	$$⊢\underset{\dot{}}{+}={+}_S$$
7		evladdval.i	$$⊢\phi \to I\in Z$$
8		evladdval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evladdval.a	$$⊢\phi \to A\in \left(K^I\right)$$
10		evladdval.m	$$⊢\phi \to \left(M\in B\wedge Q\left(M\right)\left(A\right)=V\right)$$
11		evladdval.n	$$⊢\phi \to \left(N\in B\wedge Q\left(N\right)\left(A\right)=W\right)$$
12		eqid	$$⊢S{\uparrow }_{𝑠}\left(K^I\right)=S{\uparrow }_{𝑠}\left(K^I\right)$$
13	1 3 2 12	evlrhm	$$⊢\left(I\in Z\wedge S\in \mathrm{CRing}\right)\to Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)$$
14	7 8 13	syl2anc	$$⊢\phi \to Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)$$
15		rhmghm	$$⊢Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)\to Q\in \left(P\mathrm{GrpHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)$$
16	14 15	syl	$$⊢\phi \to Q\in \left(P\mathrm{GrpHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)$$
17		ghmgrp1	$$⊢Q\in \left(P\mathrm{GrpHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)\to P\in \mathrm{Grp}$$
18	16 17	syl	$$⊢\phi \to P\in \mathrm{Grp}$$
19	10	simpld	$$⊢\phi \to M\in B$$
20	11	simpld	$$⊢\phi \to N\in B$$
21	4 5 18 19 20	grpcld	$$⊢\phi \to M\underset{\dot{}}{✚}N\in B$$
22		eqid	$$⊢{+}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={+}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
23	4 5 22	ghmlin	$$⊢\left(Q\in \left(P\mathrm{GrpHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)\wedge M\in B\wedge N\in B\right)\to Q\left(M\underset{\dot{}}{✚}N\right)=Q\left(M\right){+}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}Q\left(N\right)$$
24	16 19 20 23	syl3anc	$$⊢\phi \to Q\left(M\underset{\dot{}}{✚}N\right)=Q\left(M\right){+}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}Q\left(N\right)$$
25		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
26		ovexd	$$⊢\phi \to K^I\in \mathrm{V}$$
27	4 25	rhmf	$$⊢Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)\to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
28	14 27	syl	$$⊢\phi \to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
29	28 19	ffvelcdmd	$$⊢\phi \to Q\left(M\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
30	28 20	ffvelcdmd	$$⊢\phi \to Q\left(N\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
31	12 25 8 26 29 30 6 22	pwsplusgval	$$⊢\phi \to Q\left(M\right){+}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}Q\left(N\right)=Q\left(M\right){\underset{\dot{}}{+}}_{f}Q\left(N\right)$$
32	24 31	eqtrd	$$⊢\phi \to Q\left(M\underset{\dot{}}{✚}N\right)=Q\left(M\right){\underset{\dot{}}{+}}_{f}Q\left(N\right)$$
33	32	fveq1d	$$⊢\phi \to Q\left(M\underset{\dot{}}{✚}N\right)\left(A\right)=\left(Q\left(M\right){\underset{\dot{}}{+}}_{f}Q\left(N\right)\right)\left(A\right)$$
34	12 3 25 8 26 29	pwselbas	$$⊢\phi \to Q\left(M\right):K^I⟶K$$
35	34	ffnd	$$⊢\phi \to Q\left(M\right)Fn\left(K^I\right)$$
36	12 3 25 8 26 30	pwselbas	$$⊢\phi \to Q\left(N\right):K^I⟶K$$
37	36	ffnd	$$⊢\phi \to Q\left(N\right)Fn\left(K^I\right)$$
38		fnfvof	$$⊢\left(\left(Q\left(M\right)Fn\left(K^I\right)\wedge Q\left(N\right)Fn\left(K^I\right)\right)\wedge \left(K^I\in \mathrm{V}\wedge A\in \left(K^I\right)\right)\right)\to \left(Q\left(M\right){\underset{\dot{}}{+}}_{f}Q\left(N\right)\right)\left(A\right)=Q\left(M\right)\left(A\right)\underset{\dot{}}{+}Q\left(N\right)\left(A\right)$$
39	35 37 26 9 38	syl22anc	$$⊢\phi \to \left(Q\left(M\right){\underset{\dot{}}{+}}_{f}Q\left(N\right)\right)\left(A\right)=Q\left(M\right)\left(A\right)\underset{\dot{}}{+}Q\left(N\right)\left(A\right)$$
40	10	simprd	$$⊢\phi \to Q\left(M\right)\left(A\right)=V$$
41	11	simprd	$$⊢\phi \to Q\left(N\right)\left(A\right)=W$$
42	40 41	oveq12d	$$⊢\phi \to Q\left(M\right)\left(A\right)\underset{\dot{}}{+}Q\left(N\right)\left(A\right)=V\underset{\dot{}}{+}W$$
43	33 39 42	3eqtrd	$$⊢\phi \to Q\left(M\underset{\dot{}}{✚}N\right)\left(A\right)=V\underset{\dot{}}{+}W$$
44	21 43	jca	$$⊢\phi \to \left(M\underset{\dot{}}{✚}N\in B\wedge Q\left(M\underset{\dot{}}{✚}N\right)\left(A\right)=V\underset{\dot{}}{+}W\right)$$