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

Definition df-selv 16418
 Description: Define the "variable selection" function. The function selectVars maps elements of mPoly bijectively onto mPoly mPoly in the natural way, for example if and it would map mPoly to mPoly mPoly . 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 mPoly mPoly Scalar evalSub s mVar mPoly mVar
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-selv
StepHypRef Expression
1 cslv 16407 . 2 selectVars
2 vi . . 3
3 vr . . 3
4 cvv 2948 . . 3
5 vj . . . 4
62cv 1651 . . . . 5
76cpw 3791 . . . 4
8 vf . . . . 5
93cv 1651 . . . . . 6
10 cmpl 16400 . . . . . 6 mPoly
116, 9, 10co 6073 . . . . 5 mPoly
12 vs . . . . . 6
135cv 1651 . . . . . . . 8
146, 13cdif 3309 . . . . . . 7
1514, 9, 10co 6073 . . . . . 6 mPoly
16 vc . . . . . . 7
17 vx . . . . . . . 8
1812cv 1651 . . . . . . . . 9
19 csca 13524 . . . . . . . . 9 Scalar
2018, 19cfv 5446 . . . . . . . 8 Scalar
2117cv 1651 . . . . . . . . 9
22 cur 15654 . . . . . . . . . 10
2318, 22cfv 5446 . . . . . . . . 9
24 cvsca 13525 . . . . . . . . . 10
2518, 24cfv 5446 . . . . . . . . 9
2621, 23, 25co 6073 . . . . . . . 8
2717, 20, 26cmpt 4258 . . . . . . 7 Scalar
2817, 5wel 1726 . . . . . . . . . 10
29 cmvr 16399 . . . . . . . . . . . 12 mVar
3013, 15, 29co 6073 . . . . . . . . . . 11 mVar mPoly
3121, 30cfv 5446 . . . . . . . . . 10 mVar mPoly
3216cv 1651 . . . . . . . . . . 11
3314, 9, 29co 6073 . . . . . . . . . . . 12 mVar
3421, 33cfv 5446 . . . . . . . . . . 11 mVar
3532, 34ccom 4874 . . . . . . . . . 10 mVar
3628, 31, 35cif 3731 . . . . . . . . 9 mVar mPoly mVar
3717, 6, 36cmpt 4258 . . . . . . . 8 mVar mPoly mVar
388cv 1651 . . . . . . . . . 10
3932, 38ccom 4874 . . . . . . . . 9
40 cimas 13722 . . . . . . . . . . 11 s
4132, 9, 40co 6073 . . . . . . . . . 10 s
42 ces 16401 . . . . . . . . . . 11 evalSub
436, 18, 42co 6073 . . . . . . . . . 10 evalSub
4441, 43cfv 5446 . . . . . . . . 9 evalSub s
4539, 44cfv 5446 . . . . . . . 8 evalSub s
4637, 45cfv 5446 . . . . . . 7 evalSub s mVar mPoly mVar
4716, 27, 46csb 3243 . . . . . 6 Scalar evalSub s mVar mPoly mVar
4812, 15, 47csb 3243 . . . . 5 mPoly Scalar evalSub s mVar mPoly mVar
498, 11, 48cmpt 4258 . . . 4 mPoly mPoly Scalar evalSub s mVar mPoly mVar
505, 7, 49cmpt 4258 . . 3 mPoly mPoly Scalar evalSub s mVar mPoly mVar
512, 3, 4, 4, 50cmpt2 6075 . 2 mPoly mPoly Scalar evalSub s mVar mPoly mVar
521, 51wceq 1652 1 selectVars mPoly mPoly Scalar evalSub s mVar mPoly mVar
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator