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

Definition df-selv 19364
 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 1 + 𝑥 + 𝑦 + 𝑥𝑦 ∈ ({𝑥, 𝑦} mPoly ℤ) to (1 + 𝑥) + (1 + 𝑥)𝑦 ∈ ({𝑦} 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 = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑠(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠𝑠)(1r𝑠))) / 𝑐((((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥))))))))
Distinct variable group:   𝑓,𝑐,𝑖,𝑗,𝑟,𝑠,𝑥

Detailed syntax breakdown of Definition df-selv
StepHypRef Expression
1 cslv 19360 . 2 class selectVars
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3173 . . 3 class V
5 vj . . . 4 setvar 𝑗
62cv 1474 . . . . 5 class 𝑖
76cpw 4108 . . . 4 class 𝒫 𝑖
8 vf . . . . 5 setvar 𝑓
93cv 1474 . . . . . 6 class 𝑟
10 cmpl 19174 . . . . . 6 class mPoly
116, 9, 10co 6549 . . . . 5 class (𝑖 mPoly 𝑟)
12 vs . . . . . 6 setvar 𝑠
135cv 1474 . . . . . . . 8 class 𝑗
146, 13cdif 3537 . . . . . . 7 class (𝑖𝑗)
1514, 9, 10co 6549 . . . . . 6 class ((𝑖𝑗) mPoly 𝑟)
16 vc . . . . . . 7 setvar 𝑐
17 vx . . . . . . . 8 setvar 𝑥
1812cv 1474 . . . . . . . . 9 class 𝑠
19 csca 15771 . . . . . . . . 9 class Scalar
2018, 19cfv 5804 . . . . . . . 8 class (Scalar‘𝑠)
2117cv 1474 . . . . . . . . 9 class 𝑥
22 cur 18324 . . . . . . . . . 10 class 1r
2318, 22cfv 5804 . . . . . . . . 9 class (1r𝑠)
24 cvsca 15772 . . . . . . . . . 10 class ·𝑠
2518, 24cfv 5804 . . . . . . . . 9 class ( ·𝑠𝑠)
2621, 23, 25co 6549 . . . . . . . 8 class (𝑥( ·𝑠𝑠)(1r𝑠))
2717, 20, 26cmpt 4643 . . . . . . 7 class (𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠𝑠)(1r𝑠)))
2817, 5wel 1978 . . . . . . . . . 10 wff 𝑥𝑗
29 cmvr 19173 . . . . . . . . . . . 12 class mVar
3013, 15, 29co 6549 . . . . . . . . . . 11 class (𝑗 mVar ((𝑖𝑗) mPoly 𝑟))
3121, 30cfv 5804 . . . . . . . . . 10 class ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥)
3216cv 1474 . . . . . . . . . . 11 class 𝑐
3314, 9, 29co 6549 . . . . . . . . . . . 12 class ((𝑖𝑗) mVar 𝑟)
3421, 33cfv 5804 . . . . . . . . . . 11 class (((𝑖𝑗) mVar 𝑟)‘𝑥)
3532, 34ccom 5042 . . . . . . . . . 10 class (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥))
3628, 31, 35cif 4036 . . . . . . . . 9 class if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥)))
3717, 6, 36cmpt 4643 . . . . . . . 8 class (𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥))))
388cv 1474 . . . . . . . . . 10 class 𝑓
3932, 38ccom 5042 . . . . . . . . 9 class (𝑐𝑓)
40 cimas 15987 . . . . . . . . . . 11 class s
4132, 9, 40co 6549 . . . . . . . . . 10 class (𝑐s 𝑟)
42 ces 19325 . . . . . . . . . . 11 class evalSub
436, 18, 42co 6549 . . . . . . . . . 10 class (𝑖 evalSub 𝑠)
4441, 43cfv 5804 . . . . . . . . 9 class ((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))
4539, 44cfv 5804 . . . . . . . 8 class (((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))
4637, 45cfv 5804 . . . . . . 7 class ((((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥)))))
4716, 27, 46csb 3499 . . . . . 6 class (𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠𝑠)(1r𝑠))) / 𝑐((((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥)))))
4812, 15, 47csb 3499 . . . . 5 class ((𝑖𝑗) mPoly 𝑟) / 𝑠(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠𝑠)(1r𝑠))) / 𝑐((((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥)))))
498, 11, 48cmpt 4643 . . . 4 class (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑠(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠𝑠)(1r𝑠))) / 𝑐((((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥))))))
505, 7, 49cmpt 4643 . . 3 class (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑠(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠𝑠)(1r𝑠))) / 𝑐((((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥)))))))
512, 3, 4, 4, 50cmpt2 6551 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑠(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠𝑠)(1r𝑠))) / 𝑐((((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥))))))))
521, 51wceq 1475 1 wff selectVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑠(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠𝑠)(1r𝑠))) / 𝑐((((𝑖 evalSub 𝑠)‘(𝑐s 𝑟))‘(𝑐𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar ((𝑖𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖𝑗) mVar 𝑟)‘𝑥))))))))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator