Theorem selvcl

Description: Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024)

	Ref	Expression
Hypotheses	selvcl.p	$$⊢P=I\mathrm{mPoly}R$$
	selvcl.b	$$⊢B={\mathrm{Base}}_P$$
	selvcl.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
	selvcl.t	$$⊢T=J\mathrm{mPoly}U$$
	selvcl.e	$$⊢E={\mathrm{Base}}_T$$
	selvcl.i	$$⊢\phi \to I\in V$$
	selvcl.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	selvcl.j	$$⊢\phi \to J\subseteq I$$
	selvcl.f	$$⊢\phi \to F\in B$$
Assertion	selvcl	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)\left(F\right)\in E$$

Proof

Step	Hyp	Ref	Expression
1		selvcl.p	$$⊢P=I\mathrm{mPoly}R$$
2		selvcl.b	$$⊢B={\mathrm{Base}}_P$$
3		selvcl.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
4		selvcl.t	$$⊢T=J\mathrm{mPoly}U$$
5		selvcl.e	$$⊢E={\mathrm{Base}}_T$$
6		selvcl.i	$$⊢\phi \to I\in V$$
7		selvcl.r	$$⊢\phi \to R\in \mathrm{CRing}$$
8		selvcl.j	$$⊢\phi \to J\subseteq I$$
9		selvcl.f	$$⊢\phi \to F\in B$$
10		eqid	$$⊢\mathrm{algSc}\left(T\right)=\mathrm{algSc}\left(T\right)$$
11		eqid	$$⊢\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)=\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)$$
12	1 2 3 4 10 11 6 7 8 9	selvval	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)\left(F\right)=\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\left(\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\circ F\right)\left(\left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),\mathrm{algSc}\left(T\right)\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)\right)$$
13		eqid	$$⊢T{\uparrow }_{𝑠}\left(E^I\right)=T{\uparrow }_{𝑠}\left(E^I\right)$$
14		eqid	$$⊢{\mathrm{Base}}_{\left(T{\uparrow }_{𝑠}\left(E^I\right)\right)}={\mathrm{Base}}_{\left(T{\uparrow }_{𝑠}\left(E^I\right)\right)}$$
15	6 8	ssexd	$$⊢\phi \to J\in \mathrm{V}$$
16	6	difexd	$$⊢\phi \to I\setminus J\in \mathrm{V}$$
17	3	mplcrng	$$⊢\left(I\setminus J\in \mathrm{V}\wedge R\in \mathrm{CRing}\right)\to U\in \mathrm{CRing}$$
18	16 7 17	syl2anc	$$⊢\phi \to U\in \mathrm{CRing}$$
19	4	mplcrng	$$⊢\left(J\in \mathrm{V}\wedge U\in \mathrm{CRing}\right)\to T\in \mathrm{CRing}$$
20	15 18 19	syl2anc	$$⊢\phi \to T\in \mathrm{CRing}$$
21		ovexd	$$⊢\phi \to E^I\in \mathrm{V}$$
22		eqid	$$⊢\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)=\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)$$
23		eqid	$$⊢I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)=I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)$$
24		eqid	$$⊢T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)=T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)$$
25	3 4 10 11 22 23 24 13 5 6 7 8	selvval2lemn	$$⊢\phi \to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\in \left(\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\right)\mathrm{RingHom}\left(T{\uparrow }_{𝑠}\left(E^I\right)\right)\right)$$
26		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\right)}$$
27	26 14	rhmf	$$⊢\left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\in \left(\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\right)\mathrm{RingHom}\left(T{\uparrow }_{𝑠}\left(E^I\right)\right)\right)\to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right):{\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\right)}⟶{\mathrm{Base}}_{\left(T{\uparrow }_{𝑠}\left(E^I\right)\right)}$$
28	25 27	syl	$$⊢\phi \to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right):{\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\right)}⟶{\mathrm{Base}}_{\left(T{\uparrow }_{𝑠}\left(E^I\right)\right)}$$
29	1 2 3 4 10 11 24 23 26 6 7 8 9	selvval2lem4	$$⊢\phi \to \left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\circ F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(T{\upharpoonright }_{𝑠}\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\right)}$$
30	28 29	ffvelrnd	$$⊢\phi \to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\left(\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\circ F\right)\in {\mathrm{Base}}_{\left(T{\uparrow }_{𝑠}\left(E^I\right)\right)}$$
31	13 5 14 20 21 30	pwselbas	$$⊢\phi \to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\left(\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\circ F\right):E^I⟶E$$
32		eqid	$$⊢\left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),\mathrm{algSc}\left(T\right)\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),\mathrm{algSc}\left(T\right)\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)$$
33	3 4 10 5 32 6 7 8	selvval2lem5	$$⊢\phi \to \left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),\mathrm{algSc}\left(T\right)\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)\in \left(E^I\right)$$
34	31 33	ffvelrnd	$$⊢\phi \to \left(I\mathrm{evalSub}T\right)\left(\mathrm{ran}\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\right)\left(\left(\mathrm{algSc}\left(T\right)\circ \mathrm{algSc}\left(U\right)\right)\circ F\right)\left(\left(x\in I⟼if\left(x\in J,\left(J\mathrm{mVar}U\right)\left(x\right),\mathrm{algSc}\left(T\right)\left(\left(\left(I\setminus J\right)\mathrm{mVar}R\right)\left(x\right)\right)\right)\right)\right)\in E$$
35	12 34	eqeltrd	$$⊢\phi \to \left(I\mathrm{selectVars}R\right)\left(J\right)\left(F\right)\in E$$