Theorem selvval2

Description: Value of the "variable selection" function. Convert selvval into a simpler form by using evlsevl . (Contributed by SN, 9-Feb-2025)

	Ref	Expression
Hypotheses	selvval2.p	$$⊢P=I\mathrm{mPoly}R$$
	selvval2.b	$$⊢B={\mathrm{Base}}_P$$
	selvval2.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
	selvval2.t	$$⊢T=J\mathrm{mPoly}U$$
	selvval2.c	$$⊢C=\mathrm{algSc}\left(T\right)$$
	selvval2.d	$$⊢D=C\circ \mathrm{algSc}\left(U\right)$$
	selvval2.i	$$⊢\phi \to I\in V$$
	selvval2.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	selvval2.j	$$⊢\phi \to J\subseteq I$$
	selvval2.f	$$⊢\phi \to F\in B$$
Assertion	selvval2	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)\left(F\right)=\left(I\mathrm{eval}T\right)\left(D\circ F\right)\left(\left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),C\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		selvval2.p	$$⊢P=I\mathrm{mPoly}R$$
2		selvval2.b	$$⊢B={\mathrm{Base}}_P$$
3		selvval2.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
4		selvval2.t	$$⊢T=J\mathrm{mPoly}U$$
5		selvval2.c	$$⊢C=\mathrm{algSc}\left(T\right)$$
6		selvval2.d	$$⊢D=C\circ \mathrm{algSc}\left(U\right)$$
7		selvval2.i	$$⊢\phi \to I\in V$$
8		selvval2.r	$$⊢\phi \to R\in \mathrm{CRing}$$
9		selvval2.j	$$⊢\phi \to J\subseteq I$$
10		selvval2.f	$$⊢\phi \to F\in B$$
11	1 2 3 4 5 6 7 8 9 10	selvval	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)\left(F\right)=\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}D\right)\left(D\circ F\right)\left(\left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),C\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)\right)$$
12		eqid	$$⊢\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}D\right)=\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}D\right)$$
13		eqid	$$⊢I\mathrm{eval}T=I\mathrm{eval}T$$
14		eqid	$$⊢I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}D\right)=I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}D\right)$$
15		eqid	$$⊢T{\upharpoonright }_{𝑠}\mathrm{ran}D=T{\upharpoonright }_{𝑠}\mathrm{ran}D$$
16		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}D\right)\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}D\right)\right)}$$
17	7 9	ssexd	$$⊢\phi \to J\in \mathrm{V}$$
18	7	difexd	$$⊢\phi \to I\setminus J\in \mathrm{V}$$
19	3 18 8	mplcrngd	$$⊢\phi \to U\in \mathrm{CRing}$$
20	4 17 19	mplcrngd	$$⊢\phi \to T\in \mathrm{CRing}$$
21	3 4 5 6 18 17 8	selvcllem3	$$⊢\phi \to \mathrm{ran}D\in \mathrm{SubRing}\left(T\right)$$
22	1 2 3 4 5 6 15 14 16 7 8 9 10	selvcllem4	$$⊢\phi \to D\circ F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}D\right)\right)}$$
23	12 13 14 15 16 7 20 21 22	evlsevl	$$⊢\phi \to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}D\right)\left(D\circ F\right)=\left(I\mathrm{eval}T\right)\left(D\circ F\right)$$
24	23	fveq1d	$$⊢\phi \to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}D\right)\left(D\circ F\right)\left(\left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),C\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)\right)=\left(I\mathrm{eval}T\right)\left(D\circ F\right)\left(\left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),C\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)\right)$$
25	11 24	eqtrd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)\left(F\right)=\left(I\mathrm{eval}T\right)\left(D\circ F\right)\left(\left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),C\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)\right)$$