Definition df-selv 19543

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.)

Assertion

Ref	Expression
df-selv	|- selectVars = ( i e. _V , r e. _V |-> ( j e. ~P i |-> ( f e. ( i mPoly r ) |-> [_ ( ( i \ j ) mPoly r ) / s ]_ [_ ( x e. (Scalar ` s ) |-> ( x ( .s ` s ) ( 1r ` s ) ) ) / c ]_ ( ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) ) ) )

Distinct variable group:   f, c, i, j, r, s, x

Detailed syntax breakdown of Definition df-selv

Step	Hyp	Ref	Expression
1		cslv 19539	. 2 class selectVars
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5		vj	. . . 4 setvar j
6	2	cv 1482	. . . . 5 class i
7	6	cpw 4158	. . . 4 class ~P i
8		vf	. . . . 5 setvar f
9	3	cv 1482	. . . . . 6 class r
10		cmpl 19353	. . . . . 6 class mPoly
11	6, 9, 10	co 6650	. . . . 5 class ( i mPoly r )
12		vs	. . . . . 6 setvar s
13	5	cv 1482	. . . . . . . 8 class j
14	6, 13	cdif 3571	. . . . . . 7 class ( i \ j )
15	14, 9, 10	co 6650	. . . . . 6 class ( ( i \ j ) mPoly r )
16		vc	. . . . . . 7 setvar c
17		vx	. . . . . . . 8 setvar x
18	12	cv 1482	. . . . . . . . 9 class s
19		csca 15944	. . . . . . . . 9 class Scalar
20	18, 19	cfv 5888	. . . . . . . 8 class (Scalar ` s )
21	17	cv 1482	. . . . . . . . 9 class x
22		cur 18501	. . . . . . . . . 10 class 1r
23	18, 22	cfv 5888	. . . . . . . . 9 class ( 1r ` s )
24		cvsca 15945	. . . . . . . . . 10 class .s
25	18, 24	cfv 5888	. . . . . . . . 9 class ( .s ` s )
26	21, 23, 25	co 6650	. . . . . . . 8 class ( x ( .s ` s ) ( 1r ` s ) )
27	17, 20, 26	cmpt 4729	. . . . . . 7 class ( x e. (Scalar ` s ) |-> ( x ( .s ` s ) ( 1r ` s ) ) )
28	17, 5	wel 1991	. . . . . . . . . 10 wff x e. j
29		cmvr 19352	. . . . . . . . . . . 12 class mVar
30	13, 15, 29	co 6650	. . . . . . . . . . 11 class ( j mVar ( ( i \ j ) mPoly r ) )
31	21, 30	cfv 5888	. . . . . . . . . 10 class ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x )
32	16	cv 1482	. . . . . . . . . . 11 class c
33	14, 9, 29	co 6650	. . . . . . . . . . . 12 class ( ( i \ j ) mVar r )
34	21, 33	cfv 5888	. . . . . . . . . . 11 class ( ( ( i \ j ) mVar r ) ` x )
35	32, 34	ccom 5118	. . . . . . . . . 10 class ( c o. ( ( ( i \ j ) mVar r ) ` x ) )
36	28, 31, 35	cif 4086	. . . . . . . . 9 class if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) )
37	17, 6, 36	cmpt 4729	. . . . . . . 8 class ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) )
38	8	cv 1482	. . . . . . . . . 10 class f
39	32, 38	ccom 5118	. . . . . . . . 9 class ( c o. f )
40		cimas 16164	. . . . . . . . . . 11 class "s
41	32, 9, 40	co 6650	. . . . . . . . . 10 class ( c "s r )
42		ces 19504	. . . . . . . . . . 11 class evalSub
43	6, 18, 42	co 6650	. . . . . . . . . 10 class ( i evalSub s )
44	41, 43	cfv 5888	. . . . . . . . 9 class ( ( i evalSub s ) ` ( c "s r ) )
45	39, 44	cfv 5888	. . . . . . . 8 class ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) )
46	37, 45	cfv 5888	. . . . . . 7 class ( ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) ) )
47	16, 27, 46	csb 3533	. . . . . 6 class [_ ( x e. (Scalar ` s ) |-> ( x ( .s ` s ) ( 1r ` s ) ) ) / c ]_ ( ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) ) )
48	12, 15, 47	csb 3533	. . . . 5 class [_ ( ( i \ j ) mPoly r ) / s ]_ [_ ( x e. (Scalar ` s ) |-> ( x ( .s ` s ) ( 1r ` s ) ) ) / c ]_ ( ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) ) )
49	8, 11, 48	cmpt 4729	. . . 4 class ( f e. ( i mPoly r ) |-> [_ ( ( i \ j ) mPoly r ) / s ]_ [_ ( x e. (Scalar ` s ) |-> ( x ( .s ` s ) ( 1r ` s ) ) ) / c ]_ ( ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) )
50	5, 7, 49	cmpt 4729	. . 3 class ( j e. ~P i |-> ( f e. ( i mPoly r ) |-> [_ ( ( i \ j ) mPoly r ) / s ]_ [_ ( x e. (Scalar ` s ) |-> ( x ( .s ` s ) ( 1r ` s ) ) ) / c ]_ ( ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) ) )
51	2, 3, 4, 4, 50	cmpt2 6652	. 2 class ( i e. _V , r e. _V |-> ( j e. ~P i |-> ( f e. ( i mPoly r ) |-> [_ ( ( i \ j ) mPoly r ) / s ]_ [_ ( x e. (Scalar ` s ) |-> ( x ( .s ` s ) ( 1r ` s ) ) ) / c ]_ ( ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) ) ) )
52	1, 51	wceq 1483	1 wff selectVars = ( i e. _V , r e. _V |-> ( j e. ~P i |-> ( f e. ( i mPoly r ) |-> [_ ( ( i \ j ) mPoly r ) / s ]_ [_ ( x e. (Scalar ` s ) |-> ( x ( .s ` s ) ( 1r ` s ) ) ) / c ]_ ( ( ( ( i evalSub s ) ` ( c "s r ) ) ` ( c o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar ( ( i \ j ) mPoly r ) ) ` x ) , ( c o. ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) ) ) )

This definition is referenced by: (None)