Definition df-selv

Description: Define the "variable selection" function. The function ( ( I selectVars R )J ) maps elements of ( I mPoly R ) bijectively onto ( J mPoly ( ( I \ J ) mPoly R ) ) in the natural way, for example if I = { x , y } and J = { y } it would map 1 + x + y + x y e. ( { x , y } mPoly ZZ ) to ( 1 + x ) + ( 1 + x ) y e. ( { y } mPoly ( { x } mPoly ZZ ) ) . This, for example, allows one to treat a multivariate polynomial as a univariate polynomial with coefficients in a polynomial ring with one less variable. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	df-selv	$$⊢\mathrm{selectVars}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\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)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cslv	$$class\mathrm{selectVars}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		vj	$$setvarj$$
5	1	cv	$$setvari$$
6	5	cpw	$$class𝒫i$$
7		vf	$$setvarf$$
8		cbs	$$class\mathrm{Base}$$
9		cmpl	$$class\mathrm{mPoly}$$
10	3	cv	$$setvarr$$
11	5 10 9	co	$$class\left(i\mathrm{mPoly}r\right)$$
12	11 8	cfv	$$class{\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}$$
13	4	cv	$$setvarj$$
14	5 13	cdif	$$class\left(i\setminus j\right)$$
15	14 10 9	co	$$class\left(\left(i\setminus j\right)\mathrm{mPoly}r\right)$$
16		vu	$$setvaru$$
17	16	cv	$$setvaru$$
18	13 17 9	co	$$class\left(j\mathrm{mPoly}u\right)$$
19		vt	$$setvart$$
20		cascl	$$class\mathrm{algSc}$$
21	19	cv	$$setvart$$
22	21 20	cfv	$$class\mathrm{algSc}\left(t\right)$$
23		vc	$$setvarc$$
24	23	cv	$$setvarc$$
25	17 20	cfv	$$class\mathrm{algSc}\left(u\right)$$
26	24 25	ccom	$$class\left(c\circ \mathrm{algSc}\left(u\right)\right)$$
27		vd	$$setvard$$
28		ces	$$class\mathrm{evalSub}$$
29	5 21 28	co	$$class\left(i\mathrm{evalSub}t\right)$$
30	27	cv	$$setvard$$
31	30	crn	$$class\mathrm{ran}d$$
32	31 29	cfv	$$class\left(i\mathrm{evalSub}t\right)\left(\mathrm{ran}d\right)$$
33	7	cv	$$setvarf$$
34	30 33	ccom	$$class\left(d\circ f\right)$$
35	34 32	cfv	$$class\left(i\mathrm{evalSub}t\right)\left(\mathrm{ran}d\right)\left(d\circ f\right)$$
36		vx	$$setvarx$$
37	36	cv	$$setvarx$$
38	37 13	wcel	$$wffx\in j$$
39		cmvr	$$class\mathrm{mVar}$$
40	13 17 39	co	$$class\left(j\mathrm{mVar}u\right)$$
41	37 40	cfv	$$class\left(j\mathrm{mVar}u\right)\left(x\right)$$
42	14 10 39	co	$$class\left(\left(i\setminus j\right)\mathrm{mVar}r\right)$$
43	37 42	cfv	$$class\left(\left(i\setminus j\right)\mathrm{mVar}r\right)\left(x\right)$$
44	43 24	cfv	$$classc\left(\left(\left(i\setminus j\right)\mathrm{mVar}r\right)\left(x\right)\right)$$
45	38 41 44	cif	$$classif\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)$$
46	36 5 45	cmpt	$$class\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)$$
47	46 35	cfv	$$class\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)$$
48	27 26 47	csb	$$class⦋\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)$$
49	23 22 48	csb	$$class⦋\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)$$
50	19 18 49	csb	$$class⦋\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)$$
51	16 15 50	csb	$$class⦋\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)$$
52	7 12 51	cmpt	$$class\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)$$
53	4 6 52	cmpt	$$class\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)$$
54	1 3 2 2 53	cmpo	$$class\left(i\in \mathrm{V},r\in \mathrm{V}⟼\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)\right)$$
55	0 54	wceq	$$wff\mathrm{selectVars}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\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)\right)$$