Metamath Proof Explorer

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 
|- selectVars = ( i e. _V , r e. _V |-> ( j e. ~P i |-> ( f e. ( Base ` ( i mPoly r ) ) |-> [_ ( ( i \ j ) mPoly r ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslv 
 |-  selectVars
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vj 
 |-  j
5 1 cv 
 |-  i
6 5 cpw 
 |-  ~P i
7 vf 
 |-  f
8 cbs 
 |-  Base
9 cmpl 
 |-  mPoly
10 3 cv 
 |-  r
11 5 10 9 co 
 |-  ( i mPoly r )
12 11 8 cfv 
 |-  ( Base ` ( i mPoly r ) )
13 4 cv 
 |-  j
14 5 13 cdif 
 |-  ( i \ j )
15 14 10 9 co 
 |-  ( ( i \ j ) mPoly r )
16 vu 
 |-  u
17 16 cv 
 |-  u
18 13 17 9 co 
 |-  ( j mPoly u )
19 vt 
 |-  t
20 cascl 
 |-  algSc
21 19 cv 
 |-  t
22 21 20 cfv 
 |-  ( algSc ` t )
23 vc 
 |-  c
24 23 cv 
 |-  c
25 17 20 cfv 
 |-  ( algSc ` u )
26 24 25 ccom 
 |-  ( c o. ( algSc ` u ) )
27 vd 
 |-  d
28 ces 
 |-  evalSub
29 5 21 28 co 
 |-  ( i evalSub t )
30 27 cv 
 |-  d
31 30 crn 
 |-  ran d
32 31 29 cfv 
 |-  ( ( i evalSub t ) ` ran d )
33 7 cv 
 |-  f
34 30 33 ccom 
 |-  ( d o. f )
35 34 32 cfv 
 |-  ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) )
36 vx 
 |-  x
37 36 cv 
 |-  x
38 37 13 wcel 
 |-  x e. j
39 cmvr 
 |-  mVar
40 13 17 39 co 
 |-  ( j mVar u )
41 37 40 cfv 
 |-  ( ( j mVar u ) ` x )
42 14 10 39 co 
 |-  ( ( i \ j ) mVar r )
43 37 42 cfv 
 |-  ( ( ( i \ j ) mVar r ) ` x )
44 43 24 cfv 
 |-  ( c ` ( ( ( i \ j ) mVar r ) ` x ) )
45 38 41 44 cif 
 |-  if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) )
46 36 5 45 cmpt 
 |-  ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) )
47 46 35 cfv 
 |-  ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) )
48 27 26 47 csb 
 |-  [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) )
49 23 22 48 csb 
 |-  [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) )
50 19 18 49 csb 
 |-  [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) )
51 16 15 50 csb 
 |-  [_ ( ( i \ j ) mPoly r ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) )
52 7 12 51 cmpt 
 |-  ( f e. ( Base ` ( i mPoly r ) ) |-> [_ ( ( i \ j ) mPoly r ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) )
53 4 6 52 cmpt 
 |-  ( j e. ~P i |-> ( f e. ( Base ` ( i mPoly r ) ) |-> [_ ( ( i \ j ) mPoly r ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) ) )
54 1 3 2 2 53 cmpo 
 |-  ( i e. _V , r e. _V |-> ( j e. ~P i |-> ( f e. ( Base ` ( i mPoly r ) ) |-> [_ ( ( i \ j ) mPoly r ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) ) ) )
55 0 54 wceq 
 |-  selectVars = ( i e. _V , r e. _V |-> ( j e. ~P i |-> ( f e. ( Base ` ( i mPoly r ) ) |-> [_ ( ( i \ j ) mPoly r ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) ) ) ) ) )