Theorem selvply1rhmlem4

Description: Lemma for selvply1rhm : The mapping H is linear. (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	selvply1rhm.1	$$⊢B={\mathrm{Base}}_P$$
	selvply1rhm.2	$$⊢P=I\mathrm{mPoly}R$$
	selvply1rhm.3	$$⊢U=\left(I\setminus \left\{X\right\}\right)\mathrm{mPoly}R$$
	selvply1rhm.4	$$⊢Q={\mathrm{Poly}}_1\left(U\right)$$
	selvply1rhm.5	$$⊢H=\left(f\in B⟼\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(f\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)\right)$$
	selvply1rhm.6	$$⊢\phi \to I\in V$$
	selvply1rhm.7	$$⊢\phi \to X\in I$$
	selvply1rhm.8	$$⊢\phi \to R\in \mathrm{CRing}$$
	selvply1rhmlem4.f	$$⊢\phi \to F\in B$$
	selvply1rhmlem4.g	$$⊢\phi \to G\in B$$
Assertion	selvply1rhmlem4	$$⊢\phi \to H\left(F{+}_{P}G\right)=H\left(F\right){+}_{Q}H\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		selvply1rhm.1	$$⊢B={\mathrm{Base}}_P$$
2		selvply1rhm.2	$$⊢P=I\mathrm{mPoly}R$$
3		selvply1rhm.3	$$⊢U=\left(I\setminus \left\{X\right\}\right)\mathrm{mPoly}R$$
4		selvply1rhm.4	$$⊢Q={\mathrm{Poly}}_1\left(U\right)$$
5		selvply1rhm.5	$$⊢H=\left(f\in B⟼\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(f\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)\right)$$
6		selvply1rhm.6	$$⊢\phi \to I\in V$$
7		selvply1rhm.7	$$⊢\phi \to X\in I$$
8		selvply1rhm.8	$$⊢\phi \to R\in \mathrm{CRing}$$
9		selvply1rhmlem4.f	$$⊢\phi \to F\in B$$
10		selvply1rhmlem4.g	$$⊢\phi \to G\in B$$
11	1 2 3 4 5 6 7 8	selvply1rhmlem1	$$⊢\phi \to H:B⟶{\mathrm{Base}}_Q$$
12	11 9	ffvelcdmd	$$⊢\phi \to H\left(F\right)\in {\mathrm{Base}}_Q$$
13		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
14		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
15	4 13 14	ply1basf	$$⊢H\left(F\right)\in {\mathrm{Base}}_Q\to H\left(F\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_U$$
16	12 15	syl	$$⊢\phi \to H\left(F\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_U$$
17	16	ffnd	$$⊢\phi \to H\left(F\right)Fn\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
18	11 10	ffvelcdmd	$$⊢\phi \to H\left(G\right)\in {\mathrm{Base}}_Q$$
19	4 13 14	ply1basf	$$⊢H\left(G\right)\in {\mathrm{Base}}_Q\to H\left(G\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_U$$
20	18 19	syl	$$⊢\phi \to H\left(G\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_U$$
21	20	ffnd	$$⊢\phi \to H\left(G\right)Fn\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
22		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^{1_{𝑜}}\in \mathrm{V}$$
23		inidm	$$⊢\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\cap \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)={{\mathbb{N}}_0}^{1_{𝑜}}$$
24		eqidd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to H\left(F\right)\left(n\right)=H\left(F\right)\left(n\right)$$
25		eqidd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to H\left(G\right)\left(n\right)=H\left(G\right)\left(n\right)$$
26	17 21 22 22 23 24 25	ofval	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(H\left(F\right){{+}_U}_{f}H\left(G\right)\right)\left(n\right)=H\left(F\right)\left(n\right){+}_{U}H\left(G\right)\left(n\right)$$
27		eqid	$$⊢1_{𝑜}\mathrm{mPoly}U=1_{𝑜}\mathrm{mPoly}U$$
28	4 13	ply1bas	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}$$
29		eqid	$$⊢{+}_U={+}_U$$
30		eqid	$$⊢{+}_Q={+}_Q$$
31	4 27 30	ply1plusg	$$⊢{+}_Q={+}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}$$
32	27 28 29 31 12 18	mpladd	$$⊢\phi \to H\left(F\right){+}_{Q}H\left(G\right)=H\left(F\right){{+}_U}_{f}H\left(G\right)$$
33	32	fveq1d	$$⊢\phi \to \left(H\left(F\right){+}_{Q}H\left(G\right)\right)\left(n\right)=\left(H\left(F\right){{+}_U}_{f}H\left(G\right)\right)\left(n\right)$$
34	33	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(H\left(F\right){+}_{Q}H\left(G\right)\right)\left(n\right)=\left(H\left(F\right){{+}_U}_{f}H\left(G\right)\right)\left(n\right)$$
35		eqid	$$⊢\left\{X\right\}\mathrm{mPoly}U=\left\{X\right\}\mathrm{mPoly}U$$
36		eqid	$$⊢{\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}={\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}$$
37		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
38	7	snssd	$$⊢\phi \to \left\{X\right\}\subseteq I$$
39	2 1 3 35 36 8 38 9	selvcl	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\in {\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}$$
40	35 14 36 37 39	mplelf	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right):\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_U$$
41	40	ffnd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
42	41	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
43	2 1 3 35 36 8 38 10	selvcl	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\in {\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}$$
44	35 14 36 37 43	mplelf	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right):\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_U$$
45	44	ffnd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
46	45	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
47		ovex	$$⊢{{\mathbb{N}}_0}^{\left\{X\right\}}\in \mathrm{V}$$
48	47	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
49	48	a1i	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
50		breq1	$$⊢h=\left\{⟨X,n\left(\varnothing \right)⟩\right\}\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)$$
51		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
52	51	a1i	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
53		snex	$$⊢\left\{X\right\}\in \mathrm{V}$$
54	53	a1i	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left\{X\right\}\in \mathrm{V}$$
55	7	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to X\in I$$
56		simpr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
57	56	elmaprd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to n:1_{𝑜}⟶{\mathbb{N}}_0$$
58		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
59	58	a1i	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \varnothing \in 1_{𝑜}$$
60	57 59	ffvelcdmd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to n\left(\varnothing \right)\in {\mathbb{N}}_0$$
61	55 60	fsnd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left\{⟨X,n\left(\varnothing \right)⟩\right\}:\left\{X\right\}⟶{\mathbb{N}}_0$$
62	52 54 61	elmapdd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left\{⟨X,n\left(\varnothing \right)⟩\right\}\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)$$
63		c0ex	$$⊢0\in \mathrm{V}$$
64	63	a1i	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to 0\in \mathrm{V}$$
65		snopfsupp	$$⊢\left(X\in I\wedge n\left(\varnothing \right)\in {\mathbb{N}}_0\wedge 0\in \mathrm{V}\right)\to {finSupp}_0\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
66	55 60 64 65	syl3anc	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to {finSupp}_0\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
67	50 62 66	elrabd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left\{⟨X,n\left(\varnothing \right)⟩\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|{finSupp}_0\left(h\right)\right\}$$
68		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|{finSupp}_0\left(h\right)\right\}$$
69	68	psrbasfsupp	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
70	67 69	eleqtrdi	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left\{⟨X,n\left(\varnothing \right)⟩\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
71		fnfvof	$$⊢\left(\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge \left(\left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}\wedge \left\{⟨X,n\left(\varnothing \right)⟩\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^{\left\{X\right\}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\right)\to \left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){{+}_U}_f\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right){+}_U\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
72	42 46 49 70 71	syl22anc	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){{+}_U}_f\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right){+}_U\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
73		eqid	$$⊢{+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}={+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}$$
74	35 36 29 73 39 43	mpladd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){{+}_U}_f\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)$$
75	74	fveq1d	$$⊢\phi \to \left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)=\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){{+}_U}_f\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
76	75	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)=\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){{+}_U}_f\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
77	6	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to I\in V$$
78	8	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to R\in \mathrm{CRing}$$
79	9	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to F\in B$$
80	1 2 3 4 5 77 55 78 79 56	selvply1rhmlem3	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to H\left(F\right)\left(n\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
81	10	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to G\in B$$
82	1 2 3 4 5 77 55 78 81 56	selvply1rhmlem3	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to H\left(G\right)\left(n\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
83	80 82	oveq12d	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to H\left(F\right)\left(n\right){+}_{U}H\left(G\right)\left(n\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right){+}_U\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
84	72 76 83	3eqtr4d	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)=H\left(F\right)\left(n\right){+}_{U}H\left(G\right)\left(n\right)$$
85	26 34 84	3eqtr4rd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)=\left(H\left(F\right){+}_{Q}H\left(G\right)\right)\left(n\right)$$
86	85	mpteq2dva	$$⊢\phi \to \left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)=\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(H\left(F\right){+}_{Q}H\left(G\right)\right)\left(n\right)\right)$$
87		fveq2	$$⊢f=F{+}_{P}G\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(f\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F{+}_{P}G\right)$$
88		eqid	$$⊢{+}_P={+}_P$$
89	2 1 88 3 35 73 6 8 38 9 10	selvadd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F{+}_{P}G\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)$$
90	87 89	sylan9eqr	$$⊢\left(\phi \wedge f=F{+}_{P}G\right)\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(f\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)$$
91	90	fveq1d	$$⊢\left(\phi \wedge f=F{+}_{P}G\right)\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(f\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)=\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
92	91	mpteq2dv	$$⊢\left(\phi \wedge f=F{+}_{P}G\right)\to \left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(f\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)=\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)$$
93	8	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
94	2 6 93	mplringd	$$⊢\phi \to P\in \mathrm{Ring}$$
95	94	ringgrpd	$$⊢\phi \to P\in \mathrm{Grp}$$
96	1 88 95 9 10	grpcld	$$⊢\phi \to F{+}_{P}G\in B$$
97	22	mptexd	$$⊢\phi \to \left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)\in \mathrm{V}$$
98	5 92 96 97	fvmptd2	$$⊢\phi \to H\left(F{+}_{P}G\right)=\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right){+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(G\right)\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)$$
99	6	difexd	$$⊢\phi \to I\setminus \left\{X\right\}\in \mathrm{V}$$
100	3 99 93	mplringd	$$⊢\phi \to U\in \mathrm{Ring}$$
101	4	ply1ring	$$⊢U\in \mathrm{Ring}\to Q\in \mathrm{Ring}$$
102	100 101	syl	$$⊢\phi \to Q\in \mathrm{Ring}$$
103	102	ringgrpd	$$⊢\phi \to Q\in \mathrm{Grp}$$
104	13 30 103 12 18	grpcld	$$⊢\phi \to H\left(F\right){+}_{Q}H\left(G\right)\in {\mathrm{Base}}_Q$$
105	4 13 14	ply1basf	$$⊢H\left(F\right){+}_{Q}H\left(G\right)\in {\mathrm{Base}}_Q\to \left(H\left(F\right){+}_{Q}H\left(G\right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_U$$
106	104 105	syl	$$⊢\phi \to \left(H\left(F\right){+}_{Q}H\left(G\right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_U$$
107	106	feqmptd	$$⊢\phi \to H\left(F\right){+}_{Q}H\left(G\right)=\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(H\left(F\right){+}_{Q}H\left(G\right)\right)\left(n\right)\right)$$
108	86 98 107	3eqtr4d	$$⊢\phi \to H\left(F{+}_{P}G\right)=H\left(F\right){+}_{Q}H\left(G\right)$$