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		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
57	56	a1i	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to 1_{𝑜}\in \mathrm{V}$$
58		simpr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
59	57 52 58	elmaprd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to n:1_{𝑜}⟶{\mathbb{N}}_0$$
60		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
61	60	a1i	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \varnothing \in 1_{𝑜}$$
62	59 61	ffvelcdmd	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to n\left(\varnothing \right)\in {\mathbb{N}}_0$$
63	55 62	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$$
64	52 54 63	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)$$
65		c0ex	$$⊢0\in \mathrm{V}$$
66	65	a1i	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to 0\in \mathrm{V}$$
67		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)$$
68	55 62 66 67	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)$$
69	50 64 68	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\}$$
70		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\}$$
71	70	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\}$$
72	69 71	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\}$$
73		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)$$
74	42 46 49 72 73	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)$$
75		eqid	$$⊢{+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}={+}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}$$
76	35 36 29 75 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)$$
77	76	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)$$
78	77	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)$$
79	6	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to I\in V$$
80	8	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to R\in \mathrm{CRing}$$
81	9	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to F\in B$$
82	1 2 3 4 5 79 55 80 81 58	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)$$
83	10	adantr	$$⊢\left(\phi \wedge n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to G\in B$$
84	1 2 3 4 5 79 55 80 83 58	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)$$
85	82 84	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)$$
86	74 78 85	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)$$
87	26 34 86	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)$$
88	87	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)$$
89		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)$$
90		eqid	$$⊢{+}_P={+}_P$$
91	2 1 90 3 35 75 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)$$
92	89 91	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)$$
93	92	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)$$
94	93	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)$$
95	8	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
96	2 6 95	mplringd	$$⊢\phi \to P\in \mathrm{Ring}$$
97	96	ringgrpd	$$⊢\phi \to P\in \mathrm{Grp}$$
98	1 90 97 9 10	grpcld	$$⊢\phi \to F{+}_{P}G\in B$$
99	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}$$
100	5 94 98 99	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)$$
101	6	difexd	$$⊢\phi \to I\setminus \left\{X\right\}\in \mathrm{V}$$
102	3 101 95	mplringd	$$⊢\phi \to U\in \mathrm{Ring}$$
103	4	ply1ring	$$⊢U\in \mathrm{Ring}\to Q\in \mathrm{Ring}$$
104	102 103	syl	$$⊢\phi \to Q\in \mathrm{Ring}$$
105	104	ringgrpd	$$⊢\phi \to Q\in \mathrm{Grp}$$
106	13 30 105 12 18	grpcld	$$⊢\phi \to H\left(F\right){+}_{Q}H\left(G\right)\in {\mathrm{Base}}_Q$$
107	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$$
108	106 107	syl	$$⊢\phi \to \left(H\left(F\right){+}_{Q}H\left(G\right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_U$$
109	108	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)$$
110	88 100 109	3eqtr4d	$$⊢\phi \to H\left(F{+}_{P}G\right)=H\left(F\right){+}_{Q}H\left(G\right)$$