Theorem selvval

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

	Ref	Expression
Hypotheses	selvval.p	$$⊢P=I\mathrm{mPoly}R$$
	selvval.b	$$⊢B={\mathrm{Base}}_P$$
	selvval.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
	selvval.t	$$⊢T=J\mathrm{mPoly}U$$
	selvval.c	$$⊢C=\mathrm{algSc}\left(T\right)$$
	selvval.d	$$⊢D=C\circ \mathrm{algSc}\left(U\right)$$
	selvval.i	$$⊢\phi \to I\in V$$
	selvval.r	$$⊢\phi \to R\in W$$
	selvval.j	$$⊢\phi \to J\subseteq I$$
	selvval.f	$$⊢\phi \to F\in B$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		selvval.p	$$⊢P=I\mathrm{mPoly}R$$
2		selvval.b	$$⊢B={\mathrm{Base}}_P$$
3		selvval.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
4		selvval.t	$$⊢T=J\mathrm{mPoly}U$$
5		selvval.c	$$⊢C=\mathrm{algSc}\left(T\right)$$
6		selvval.d	$$⊢D=C\circ \mathrm{algSc}\left(U\right)$$
7		selvval.i	$$⊢\phi \to I\in V$$
8		selvval.r	$$⊢\phi \to R\in W$$
9		selvval.j	$$⊢\phi \to J\subseteq I$$
10		selvval.f	$$⊢\phi \to F\in B$$
11	7 8 9	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)$$
12		coeq2	$$⊢f=F\to d\circ f=d\circ F$$
13	12	fveq2d	$$⊢f=F\to \left(I\mathrm{evalSub}t\right)\left(\mathrm{ran}d\right)\left(d\circ f\right)=\left(I\mathrm{evalSub}t\right)\left(\mathrm{ran}d\right)\left(d\circ F\right)$$
14	13	fveq1d	$$⊢f=F\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)$$
15	14	csbeq2dv	$$⊢f=F\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)$$
16	15	csbeq2dv	$$⊢f=F\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)$$
17	16	csbeq2dv	$$⊢f=F\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)$$
18	17	csbeq2dv	$$⊢f=F\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)$$
19	18	adantl	$$⊢\left(\phi \wedge f=F\right)\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)$$
20	1	fveq2i	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
21	2 20	eqtri	$$⊢B={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
22	10 21	eleqtrdi	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
23		fvex	$$⊢\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)\in \mathrm{V}$$
24	23	csbex	$$⊢⦋\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)\in \mathrm{V}$$
25	24	csbex	$$⊢⦋\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)\in \mathrm{V}$$
26	25	csbex	$$⊢⦋\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)\in \mathrm{V}$$
27	26	csbex	$$⊢⦋\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)\in \mathrm{V}$$
28	27	a1i	$$⊢\phi \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)\in \mathrm{V}$$
29	11 19 22 28	fvmptd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)\left(F\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)$$
30		ovex	$$⊢\left(I\setminus J\right)\mathrm{mPoly}R\in \mathrm{V}$$
31	3	eqeq2i	$$⊢u=U\leftrightarrow u=\left(I\setminus J\right)\mathrm{mPoly}R$$
32		oveq2	$$⊢u=U\to J\mathrm{mPoly}u=J\mathrm{mPoly}U$$
33		fveq2	$$⊢u=U\to \mathrm{algSc}\left(u\right)=\mathrm{algSc}\left(U\right)$$
34	33	coeq2d	$$⊢u=U\to c\circ \mathrm{algSc}\left(u\right)=c\circ \mathrm{algSc}\left(U\right)$$
35		oveq2	$$⊢u=U\to J\mathrm{mVar}u=J\mathrm{mVar}U$$
36	35	fveq1d	$$⊢u=U\to \left(J\mathrm{mVar}u\right)\left(x\right)=\left(J\mathrm{mVar}U\right)\left(x\right)$$
37	36	ifeq1d	$$⊢u=U\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)$$
38	37	mpteq2dv	$$⊢u=U\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)$$
39	38	fveq2d	$$⊢u=U\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)$$
40	34 39	csbeq12dv	$$⊢u=U\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)$$
41	40	csbeq2dv	$$⊢u=U\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)$$
42	32 41	csbeq12dv	$$⊢u=U\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)$$
43		ovex	$$⊢J\mathrm{mPoly}U\in \mathrm{V}$$
44	4	eqeq2i	$$⊢t=T\leftrightarrow t=J\mathrm{mPoly}U$$
45		fveq2	$$⊢t=T\to \mathrm{algSc}\left(t\right)=\mathrm{algSc}\left(T\right)$$
46		oveq2	$$⊢t=T\to I\mathrm{evalSub}t=I\mathrm{evalSub}T$$
47	46	fveq1d	$$⊢t=T\to \left(I\mathrm{evalSub}t\right)\left(\mathrm{ran}d\right)=\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}d\right)$$
48	47	fveq1d	$$⊢t=T\to \left(I\mathrm{evalSub}t\right)\left(\mathrm{ran}d\right)\left(d\circ F\right)=\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}d\right)\left(d\circ F\right)$$
49	48	fveq1d	$$⊢t=T\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)$$
50	49	csbeq2dv	$$⊢t=T\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)$$
51	45 50	csbeq12dv	$$⊢t=T\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)$$
52		fvex	$$⊢\mathrm{algSc}\left(T\right)\in \mathrm{V}$$
53	5	eqeq2i	$$⊢c=C\leftrightarrow c=\mathrm{algSc}\left(T\right)$$
54		coeq1	$$⊢c=C\to c\circ \mathrm{algSc}\left(U\right)=C\circ \mathrm{algSc}\left(U\right)$$
55		fveq1	$$⊢c=C\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)$$
56	55	ifeq2d	$$⊢c=C\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)$$
57	56	mpteq2dv	$$⊢c=C\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)$$
58	57	fveq2d	$$⊢c=C\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)$$
59	54 58	csbeq12dv	$$⊢c=C\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)$$
60	5	fvexi	$$⊢C\in \mathrm{V}$$
61		fvex	$$⊢\mathrm{algSc}\left(U\right)\in \mathrm{V}$$
62	60 61	coex	$$⊢C\circ \mathrm{algSc}\left(U\right)\in \mathrm{V}$$
63	6	eqeq2i	$$⊢d=D\leftrightarrow d=C\circ \mathrm{algSc}\left(U\right)$$
64		rneq	$$⊢d=D\to \mathrm{ran}d=\mathrm{ran}D$$
65	64	fveq2d	$$⊢d=D\to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}d\right)=\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}D\right)$$
66		coeq1	$$⊢d=D\to d\circ F=D\circ F$$
67	65 66	fveq12d	$$⊢d=D\to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}d\right)\left(d\circ F\right)=\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}D\right)\left(D\circ F\right)$$
68	67	fveq1d	$$⊢d=D\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)$$
69	63 68	sylbir	$$⊢d=C\circ \mathrm{algSc}\left(U\right)\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)$$
70	62 69	csbie	$$⊢⦋\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(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)$$
71	59 70	eqtrdi	$$⊢c=C\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(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)$$
72	53 71	sylbir	$$⊢c=\mathrm{algSc}\left(T\right)\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(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)$$
73	52 72	csbie	$$⊢⦋\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(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)$$
74	51 73	eqtrdi	$$⊢t=T\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)=\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)$$
75	44 74	sylbir	$$⊢t=J\mathrm{mPoly}U\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)=\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)$$
76	43 75	csbie	$$⊢⦋\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(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)$$
77	42 76	eqtrdi	$$⊢u=U\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(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)$$
78	31 77	sylbir	$$⊢u=\left(I\setminus J\right)\mathrm{mPoly}R\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(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)$$
79	30 78	csbie	$$⊢⦋\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(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)$$
80	29 79	eqtrdi	$$⊢\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)$$