MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-selv Unicode version

Definition df-selv 16123
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
StepHypRef Expression
1 cslv 16112 . 2  class selectVars
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
5 vj . . . 4  set  j
62cv 1631 . . . . 5  class  i
76cpw 3638 . . . 4  class  ~P i
8 vf . . . . 5  set  f
93cv 1631 . . . . . 6  class  r
10 cmpl 16105 . . . . . 6  class mPoly
116, 9, 10co 5874 . . . . 5  class  ( i mPoly 
r )
12 vs . . . . . 6  set  s
135cv 1631 . . . . . . . 8  class  j
146, 13cdif 3162 . . . . . . 7  class  ( i 
\  j )
1514, 9, 10co 5874 . . . . . 6  class  ( ( i  \  j ) mPoly 
r )
16 vc . . . . . . 7  set  c
17 vx . . . . . . . 8  set  x
1812cv 1631 . . . . . . . . 9  class  s
19 csca 13227 . . . . . . . . 9  class Scalar
2018, 19cfv 5271 . . . . . . . 8  class  (Scalar `  s )
2117cv 1631 . . . . . . . . 9  class  x
22 cur 15355 . . . . . . . . . 10  class  1r
2318, 22cfv 5271 . . . . . . . . 9  class  ( 1r
`  s )
24 cvsca 13228 . . . . . . . . . 10  class  .s
2518, 24cfv 5271 . . . . . . . . 9  class  ( .s
`  s )
2621, 23, 25co 5874 . . . . . . . 8  class  ( x ( .s `  s
) ( 1r `  s ) )
2717, 20, 26cmpt 4093 . . . . . . 7  class  ( x  e.  (Scalar `  s
)  |->  ( x ( .s `  s ) ( 1r `  s
) ) )
2817, 5wel 1697 . . . . . . . . . 10  wff  x  e.  j
29 cmvr 16104 . . . . . . . . . . . 12  class mVar
3013, 15, 29co 5874 . . . . . . . . . . 11  class  ( j mVar  ( ( i  \ 
j ) mPoly  r ) )
3121, 30cfv 5271 . . . . . . . . . 10  class  ( ( j mVar  ( ( i 
\  j ) mPoly  r
) ) `  x
)
3216cv 1631 . . . . . . . . . . 11  class  c
3314, 9, 29co 5874 . . . . . . . . . . . 12  class  ( ( i  \  j ) mVar  r )
3421, 33cfv 5271 . . . . . . . . . . 11  class  ( ( ( i  \  j
) mVar  r ) `  x )
3532, 34ccom 4709 . . . . . . . . . 10  class  ( c  o.  ( ( ( i  \  j ) mVar  r ) `  x
) )
3628, 31, 35cif 3578 . . . . . . . . 9  class  if ( x  e.  j ,  ( ( j mVar  (
( i  \  j
) mPoly  r ) ) `
 x ) ,  ( c  o.  (
( ( i  \ 
j ) mVar  r ) `
 x ) ) )
3717, 6, 36cmpt 4093 . . . . . . . 8  class  ( x  e.  i  |->  if ( x  e.  j ,  ( ( j mVar  (
( i  \  j
) mPoly  r ) ) `
 x ) ,  ( c  o.  (
( ( i  \ 
j ) mVar  r ) `
 x ) ) ) )
388cv 1631 . . . . . . . . . 10  class  f
3932, 38ccom 4709 . . . . . . . . 9  class  ( c  o.  f )
40 cimas 13423 . . . . . . . . . . 11  class  "s
4132, 9, 40co 5874 . . . . . . . . . 10  class  ( c 
"s  r )
42 ces 16106 . . . . . . . . . . 11  class evalSub
436, 18, 42co 5874 . . . . . . . . . 10  class  ( i evalSub 
s )
4441, 43cfv 5271 . . . . . . . . 9  class  ( ( i evalSub  s ) `  ( c  "s  r )
)
4539, 44cfv 5271 . . . . . . . 8  class  ( ( ( i evalSub  s ) `
 ( c  "s  r
) ) `  (
c  o.  f ) )
4637, 45cfv 5271 . . . . . . 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 ) ) ) ) )
4716, 27, 46csb 3094 . . . . . 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 )
) ) ) )
4812, 15, 47csb 3094 . . . . 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 ) ) ) ) )
498, 11, 48cmpt 4093 . . . 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 )
) ) ) ) )
505, 7, 49cmpt 4093 . . 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 ) ) ) ) ) ) )
512, 3, 4, 4, 50cmpt2 5876 . 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 ) ) ) ) ) ) ) )
521, 51wceq 1632 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 )
) ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator