Theorem selvfval

Description: Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023)

	Ref	Expression
Hypotheses	selvffval.i	$$⊢\phi \to I\in V$$
	selvffval.r	$$⊢\phi \to R\in W$$
	selvfval.j	$$⊢\phi \to J\subseteq I$$
Assertion	selvfval	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)=\left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus J\right)\mathrm{mPoly}R\right)/u⦌⦋\left(J\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)$$

Proof

Step	Hyp	Ref	Expression
1		selvffval.i	$$⊢\phi \to I\in V$$
2		selvffval.r	$$⊢\phi \to R\in W$$
3		selvfval.j	$$⊢\phi \to J\subseteq I$$
4	1 2	selvffval	$$⊢\phi \to I\mathrm{selectVars}R=\left(j\in 𝒫I⟼\left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus j\right)\mathrm{mPoly}R\right)/u⦌⦋\left(j\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)\right)$$
5		difeq2	$$⊢j=J\to I\setminus j=I\setminus J$$
6	5	oveq1d	$$⊢j=J\to \left(I\setminus j\right)\mathrm{mPoly}R=\left(I\setminus J\right)\mathrm{mPoly}R$$
7		oveq1	$$⊢j=J\to j\mathrm{mPoly}u=J\mathrm{mPoly}u$$
8		eleq2	$$⊢j=J\to \left(x\in j\leftrightarrow x\in J\right)$$
9		oveq1	$$⊢j=J\to j\mathrm{mVar}u=J\mathrm{mVar}u$$
10	9	fveq1d	$$⊢j=J\to \left(j\mathrm{mVar}u\right)\left(x\right)=\left(J\mathrm{mVar}u\right)\left(x\right)$$
11	5	oveq1d	$$⊢j=J\to \left(I\setminus j\right)\mathrm{mVar}R=\left(I\setminus J\right)\mathrm{mVar}R$$
12	11	fveq1d	$$⊢j=J\to \left(\left(I\setminus j\right)\mathrm{mVar}R\right)\left(x\right)=\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)$$
13	12	fveq2d	$$⊢j=J\to c\left(\left(\left(I\setminus j\right)\mathrm{mVar}R\right)\left(x\right)\right)=c\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)$$
14	8 10 13	ifbieq12d	$$⊢j=J\to 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)=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)$$
15	14	mpteq2dv	$$⊢j=J\to \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)=\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)$$
16	15	fveq2d	$$⊢j=J\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{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)$$
17	16	csbeq2dv	$$⊢j=J\to ⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)$$
18	17	csbeq2dv	$$⊢j=J\to ⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)=⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)$$
19	7 18	csbeq12dv	$$⊢j=J\to ⦋\left(j\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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(J\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)$$
20	6 19	csbeq12dv	$$⊢j=J\to ⦋\left(\left(I\setminus j\right)\mathrm{mPoly}R\right)/u⦌⦋\left(j\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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(\left(I\setminus J\right)\mathrm{mPoly}R\right)/u⦌⦋\left(J\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)$$
21	20	mpteq2dv	$$⊢j=J\to \left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus j\right)\mathrm{mPoly}R\right)/u⦌⦋\left(j\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)=\left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus J\right)\mathrm{mPoly}R\right)/u⦌⦋\left(J\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)$$
22	21	adantl	$$⊢\left(\phi \wedge j=J\right)\to \left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus j\right)\mathrm{mPoly}R\right)/u⦌⦋\left(j\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)=\left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus J\right)\mathrm{mPoly}R\right)/u⦌⦋\left(J\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)$$
23	1 3	sselpwd	$$⊢\phi \to J\in 𝒫I$$
24		fvex	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}\in \mathrm{V}$$
25		mptexg	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}\in \mathrm{V}\to \left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus J\right)\mathrm{mPoly}R\right)/u⦌⦋\left(J\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)\in \mathrm{V}$$
26	24 25	mp1i	$$⊢\phi \to \left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus J\right)\mathrm{mPoly}R\right)/u⦌⦋\left(J\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)\in \mathrm{V}$$
27	4 22 23 26	fvmptd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)=\left(f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼⦋\left(\left(I\setminus J\right)\mathrm{mPoly}R\right)/u⦌⦋\left(J\mathrm{mPoly}u\right)/t⦌⦋\mathrm{algSc}\left(t\right)/c⦌⦋\left(c\circ \mathrm{algSc}\left(u\right)\right)/d⦌\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)\right)$$