Theorem selvply1rhmlem5

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}$$
	selvply1rhmlem5.f	$$⊢\phi \to F\in B$$
	selvply1rhmlem5.m	$$⊢M=\left(q\in {\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}⟼\left(s\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼q\left(\left\{⟨X,s\left(\varnothing \right)⟩\right\}\right)\right)\right)$$
Assertion	selvply1rhmlem5	$$⊢\phi \to H\left(F\right)=M\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\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		selvply1rhmlem5.f	$$⊢\phi \to F\in B$$
10		selvply1rhmlem5.m	$$⊢M=\left(q\in {\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}⟼\left(s\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼q\left(\left\{⟨X,s\left(\varnothing \right)⟩\right\}\right)\right)\right)$$
11		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)$$
12	11	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)$$
13	12	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)$$
14		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^{1_{𝑜}}\in \mathrm{V}$$
15	14	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}$$
16	5 13 9 15	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)$$
17		fveq1	$$⊢s=n\to s\left(\varnothing \right)=n\left(\varnothing \right)$$
18	17	opeq2d	$$⊢s=n\to ⟨X,s\left(\varnothing \right)⟩=⟨X,n\left(\varnothing \right)⟩$$
19	18	sneqd	$$⊢s=n\to \left\{⟨X,s\left(\varnothing \right)⟩\right\}=\left\{⟨X,n\left(\varnothing \right)⟩\right\}$$
20	19	fveq2d	$$⊢s=n\to q\left(\left\{⟨X,s\left(\varnothing \right)⟩\right\}\right)=q\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)$$
21	20	cbvmptv	$$⊢\left(s\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼q\left(\left\{⟨X,s\left(\varnothing \right)⟩\right\}\right)\right)=\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼q\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)$$
22	21	mpteq2i	$$⊢\left(q\in {\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}⟼\left(s\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼q\left(\left\{⟨X,s\left(\varnothing \right)⟩\right\}\right)\right)\right)=\left(q\in {\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}⟼\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼q\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)\right)$$
23	10 22	eqtri	$$⊢M=\left(q\in {\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}⟼\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼q\left(\left\{⟨X,n\left(\varnothing \right)⟩\right\}\right)\right)\right)$$
24		fveq1	$$⊢q=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\to q\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)$$
25	24	mpteq2dv	$$⊢q=\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\to \left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼q\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)$$
26		eqid	$$⊢\left\{X\right\}\mathrm{mPoly}U=\left\{X\right\}\mathrm{mPoly}U$$
27		eqid	$$⊢{\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}={\mathrm{Base}}_{\left(\left\{X\right\}\mathrm{mPoly}U\right)}$$
28	7	snssd	$$⊢\phi \to \left\{X\right\}\subseteq I$$
29	2 1 3 26 27 8 28 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)}$$
30	23 25 29 15	fvmptd3	$$⊢\phi \to M\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\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)$$
31	16 30	eqtr4d	$$⊢\phi \to H\left(F\right)=M\left(\left(I\mathrm{selectVars}R\right)\left(\left\{X\right\}\right)\left(F\right)\right)$$