Theorem selvply1rhm0

Description: The ring homomorphism H built in selvply1rhm is injective. (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}$$
	selvply1rhm0.1	$$⊢\underset{\dot{}}{0}=0_Q$$
	selvply1rhm0.2	$$⊢Z=0_P$$
	selvply1rhm0.3	$$⊢\phi \to F\in B$$
	selvply1rhm0.4	$$⊢\phi \to H\left(F\right)=\underset{\dot{}}{0}$$
Assertion	selvply1rhm0	$$⊢\phi \to F=Z$$

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		selvply1rhm0.1	$$⊢\underset{\dot{}}{0}=0_Q$$
10		selvply1rhm0.2	$$⊢Z=0_P$$
11		selvply1rhm0.3	$$⊢\phi \to F\in B$$
12		selvply1rhm0.4	$$⊢\phi \to H\left(F\right)=\underset{\dot{}}{0}$$
13		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
14		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
15	14	psrbasfsupp	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
16	2 13 1 15 11	mplelf	$$⊢\phi \to F:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
17	16	feqmptd	$$⊢\phi \to F=\left(p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(p\right)\right)$$
18		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
19	18	a1i	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
20		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
21	20	a1i	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1_{𝑜}\in \mathrm{V}$$
22		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
23	22	eqcomi	$$⊢\left\{\varnothing \right\}=1_{𝑜}$$
24	23	a1i	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{\varnothing \right\}=1_{𝑜}$$
25		0ex	$$⊢\varnothing \in \mathrm{V}$$
26	25	a1i	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \varnothing \in \mathrm{V}$$
27		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
28	27	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
29	28	sselda	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to p\in \left({{\mathbb{N}}_0}^I\right)$$
30	29	elmaprd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to p:I⟶{\mathbb{N}}_0$$
31	7	adantr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to X\in I$$
32	30 31	ffvelcdmd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to p\left(X\right)\in {\mathbb{N}}_0$$
33	26 32	fsnd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{⟨\varnothing ,p\left(X\right)⟩\right\}:\left\{\varnothing \right\}⟶{\mathbb{N}}_0$$
34	24 33	feq2dd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{⟨\varnothing ,p\left(X\right)⟩\right\}:1_{𝑜}⟶{\mathbb{N}}_0$$
35	19 21 34	elmapdd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{⟨\varnothing ,p\left(X\right)⟩\right\}\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
36		psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
37		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}$$
38	37	psrbasfsupp	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
39	36 38	eqtr4i	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}$$
40	35 39	eleqtrdi	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{⟨\varnothing ,p\left(X\right)⟩\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}$$
41		fvex	$$⊢0_U\in \mathrm{V}$$
42	41	fvconst2	$$⊢\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}\to \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_U\right\}\right)\left(\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\right)=0_U$$
43	40 42	syl	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_U\right\}\right)\left(\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\right)=0_U$$
44	30	ffnd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to pFnI$$
45		fnressn	$$⊢\left(pFnI\wedge X\in I\right)\to {p\upharpoonright }_{\left\{X\right\}}=\left\{⟨X,p\left(X\right)⟩\right\}$$
46	44 31 45	syl2anc	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {p\upharpoonright }_{\left\{X\right\}}=\left\{⟨X,p\left(X\right)⟩\right\}$$
47		fvex	$$⊢p\left(X\right)\in \mathrm{V}$$
48	25 47	fvsn	$$⊢\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\left(\varnothing \right)=p\left(X\right)$$
49	48	opeq2i	$$⊢⟨X,\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\left(\varnothing \right)⟩=⟨X,p\left(X\right)⟩$$
50	49	sneqi	$$⊢\left\{⟨X,\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\left(\varnothing \right)⟩\right\}=\left\{⟨X,p\left(X\right)⟩\right\}$$
51	46 50	eqtr4di	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {p\upharpoonright }_{\left\{X\right\}}=\left\{⟨X,\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\left(\varnothing \right)⟩\right\}$$
52	51	fveq2d	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left({p\upharpoonright }_{\left\{X\right\}}\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\left(\varnothing \right)⟩\right\}\right)$$
53	6	adantr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to I\in V$$
54	8	adantr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to R\in \mathrm{CRing}$$
55	11	adantr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to F\in B$$
56	1 2 3 4 5 53 31 54 55 35	selvply1rhmlem3	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to H\left(F\right)\left(\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\left(\varnothing \right)⟩\right\}\right)$$
57		eqid	$$⊢1_{𝑜}\mathrm{mPoly}U=1_{𝑜}\mathrm{mPoly}U$$
58		eqid	$$⊢0_U=0_U$$
59	57 4 9	ply1mpl0	$$⊢\underset{\dot{}}{0}=0_{\left(1_{𝑜}\mathrm{mPoly}U\right)}$$
60	20	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
61	6	difexd	$$⊢\phi \to I\setminus \left\{X\right\}\in \mathrm{V}$$
62	8	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
63	3 61 62	mplringd	$$⊢\phi \to U\in \mathrm{Ring}$$
64	63	ringgrpd	$$⊢\phi \to U\in \mathrm{Grp}$$
65	57 38 58 59 60 64	mpl0	$$⊢\phi \to \underset{\dot{}}{0}=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_U\right\}$$
66	12 65	eqtrd	$$⊢\phi \to H\left(F\right)=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_U\right\}$$
67	66	fveq1d	$$⊢\phi \to H\left(F\right)\left(\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\right)=\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_U\right\}\right)\left(\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\right)$$
68	67	adantr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to H\left(F\right)\left(\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\right)=\left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_U\right\}\right)\left(\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\right)$$
69	52 56 68	3eqtr2rd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_U\right\}\right)\left(\left\{⟨\varnothing ,p\left(X\right)⟩\right\}\right)=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left({p\upharpoonright }_{\left\{X\right\}}\right)$$
70		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}$$
71	70	psrbasfsupp	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
72		eqid	$$⊢0_R=0_R$$
73	61	adantr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to I\setminus \left\{X\right\}\in \mathrm{V}$$
74	62	ringgrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
75	74	adantr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to R\in \mathrm{Grp}$$
76	3 71 72 58 73 75	mpl0	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 0_U=\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_R\right\}$$
77	43 69 76	3eqtr3d	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left({p\upharpoonright }_{\left\{X\right\}}\right)=\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_R\right\}$$
78	77	fveq1d	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left({p\upharpoonright }_{\left\{X\right\}}\right)\left({p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)=\left(\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_R\right\}\right)\left({p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)$$
79	7	snssd	$$⊢\phi \to \left\{X\right\}\subseteq I$$
80	79	adantr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{X\right\}\subseteq I$$
81		simpr	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
82	15 2 1 54 80 55 81	selvvvval	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left({p\upharpoonright }_{\left\{X\right\}}\right)\left({p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)=F\left(p\right)$$
83		breq1	$$⊢h={p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left({p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\right)$$
84		difssd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to I\setminus \left\{X\right\}\subseteq I$$
85	29 84	elmapssresd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)$$
86		breq1	$$⊢h=p\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(p\right)\right)$$
87	86 81	elrabrd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_0\left(p\right)$$
88		c0ex	$$⊢0\in \mathrm{V}$$
89	88	a1i	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 0\in \mathrm{V}$$
90	87 89	fsuppres	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_0\left(\left({p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$
91	83 85 90	elrabd	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\in \left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}$$
92		fvex	$$⊢0_R\in \mathrm{V}$$
93	92	fvconst2	$$⊢{p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\in \left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}\to \left(\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_R\right\}\right)\left({p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)=0_R$$
94	91 93	syl	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(\left\{h\in \left({{\mathbb{N}}_0}^{\left(I\setminus \left\{X\right\}\right)}\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_R\right\}\right)\left({p\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)=0_R$$
95	78 82 94	3eqtr3d	$$⊢\left(\phi \wedge p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to F\left(p\right)=0_R$$
96	95	mpteq2dva	$$⊢\phi \to \left(p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(p\right)\right)=\left(p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼0_R\right)$$
97	2 15 72 10 6 74	mpl0	$$⊢\phi \to Z=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_R\right\}$$
98		fconstmpt	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\times \left\{0_R\right\}=\left(p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼0_R\right)$$
99	97 98	eqtr2di	$$⊢\phi \to \left(p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼0_R\right)=Z$$
100	17 96 99	3eqtrd	$$⊢\phi \to F=Z$$