Theorem selvply1rhmlem3

Description: Lemma for selvply1rhm . (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}$$
	selvply1rhmlem3.f	$$⊢\phi \to F\in B$$
	selvply1rhmlem3.n	$$⊢\phi \to N\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
Assertion	selvply1rhmlem3	$$⊢\phi \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)$$

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		selvply1rhmlem3.f	$$⊢\phi \to F\in B$$
10		selvply1rhmlem3.n	$$⊢\phi \to N\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
11		fveq1	$$⊢m=N\to m\left(\varnothing \right)=N\left(\varnothing \right)$$
12	11	opeq2d	$$⊢m=N\to ⟨X,m\left(\varnothing \right)⟩=⟨X,N\left(\varnothing \right)⟩$$
13	12	sneqd	$$⊢m=N\to \left\{⟨X,m\left(\varnothing \right)⟩\right\}=\left\{⟨X,N\left(\varnothing \right)⟩\right\}$$
14	13	fveq2d	$$⊢m=N\to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,m\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)$$
15		fveq2	$$⊢f=F\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)$$
16	15	fveq1d	$$⊢f=F\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(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
17	16	mpteq2dv	$$⊢f=F\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(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)$$
18		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^{1_{𝑜}}\in \mathrm{V}$$
19	18	mptexd	$$⊢\phi \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)\in \mathrm{V}$$
20	5 17 9 19	fvmptd3	$$⊢\phi \to H\left(F\right)=\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)$$
21		fveq1	$$⊢n=m\to n\left(\varnothing \right)=m\left(\varnothing \right)$$
22	21	opeq2d	$$⊢n=m\to ⟨X,n\left(\varnothing \right)⟩=⟨X,m\left(\varnothing \right)⟩$$
23	22	sneqd	$$⊢n=m\to \left\{⟨X,n\left(\varnothing \right)⟩\right\}=\left\{⟨X,m\left(\varnothing \right)⟩\right\}$$
24	23	fveq2d	$$⊢n=m\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(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,m\left(\varnothing \right)⟩\right\}\right)$$
25	24	cbvmptv	$$⊢\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(m\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,m\left(\varnothing \right)⟩\right\}\right)\right)$$
26	20 25	eqtrdi	$$⊢\phi \to H\left(F\right)=\left(m\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,m\left(\varnothing \right)⟩\right\}\right)\right)$$
27		fvexd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\left(\left\{⟨X,N\left(\varnothing \right)⟩\right\}\right)\in \mathrm{V}$$
28	14 26 10 27	fvmptd4	$$⊢\phi \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)$$