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

Definition df-selv 20782
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 ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥))))))))
Distinct variable group:   𝑐,𝑑,𝑓,𝑖,𝑗,𝑟,𝑡,𝑢,𝑥

Detailed syntax breakdown of Definition df-selv
StepHypRef Expression
1 cslv 20778 . 2 class selectVars
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3469 . . 3 class V
5 vj . . . 4 setvar 𝑗
62cv 1537 . . . . 5 class 𝑖
76cpw 4511 . . . 4 class 𝒫 𝑖
8 vf . . . . 5 setvar 𝑓
93cv 1537 . . . . . . 7 class 𝑟
10 cmpl 20589 . . . . . . 7 class mPoly
116, 9, 10co 7140 . . . . . 6 class (𝑖 mPoly 𝑟)
12 cbs 16474 . . . . . 6 class Base
1311, 12cfv 6334 . . . . 5 class (Base‘(𝑖 mPoly 𝑟))
14 vu . . . . . 6 setvar 𝑢
155cv 1537 . . . . . . . 8 class 𝑗
166, 15cdif 3905 . . . . . . 7 class (𝑖𝑗)
1716, 9, 10co 7140 . . . . . 6 class ((𝑖𝑗) mPoly 𝑟)
18 vt . . . . . . 7 setvar 𝑡
1914cv 1537 . . . . . . . 8 class 𝑢
2015, 19, 10co 7140 . . . . . . 7 class (𝑗 mPoly 𝑢)
21 vc . . . . . . . 8 setvar 𝑐
2218cv 1537 . . . . . . . . 9 class 𝑡
23 cascl 20539 . . . . . . . . 9 class algSc
2422, 23cfv 6334 . . . . . . . 8 class (algSc‘𝑡)
25 vd . . . . . . . . 9 setvar 𝑑
2621cv 1537 . . . . . . . . . 10 class 𝑐
2719, 23cfv 6334 . . . . . . . . . 10 class (algSc‘𝑢)
2826, 27ccom 5536 . . . . . . . . 9 class (𝑐 ∘ (algSc‘𝑢))
29 vx . . . . . . . . . . 11 setvar 𝑥
3029, 5wel 2115 . . . . . . . . . . . 12 wff 𝑥𝑗
3129cv 1537 . . . . . . . . . . . . 13 class 𝑥
32 cmvr 20588 . . . . . . . . . . . . . 14 class mVar
3315, 19, 32co 7140 . . . . . . . . . . . . 13 class (𝑗 mVar 𝑢)
3431, 33cfv 6334 . . . . . . . . . . . 12 class ((𝑗 mVar 𝑢)‘𝑥)
3516, 9, 32co 7140 . . . . . . . . . . . . . 14 class ((𝑖𝑗) mVar 𝑟)
3631, 35cfv 6334 . . . . . . . . . . . . 13 class (((𝑖𝑗) mVar 𝑟)‘𝑥)
3736, 26cfv 6334 . . . . . . . . . . . 12 class (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥))
3830, 34, 37cif 4439 . . . . . . . . . . 11 class if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥)))
3929, 6, 38cmpt 5122 . . . . . . . . . 10 class (𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥))))
4025cv 1537 . . . . . . . . . . . 12 class 𝑑
418cv 1537 . . . . . . . . . . . 12 class 𝑓
4240, 41ccom 5536 . . . . . . . . . . 11 class (𝑑𝑓)
4340crn 5533 . . . . . . . . . . . 12 class ran 𝑑
44 ces 20741 . . . . . . . . . . . . 13 class evalSub
456, 22, 44co 7140 . . . . . . . . . . . 12 class (𝑖 evalSub 𝑡)
4643, 45cfv 6334 . . . . . . . . . . 11 class ((𝑖 evalSub 𝑡)‘ran 𝑑)
4742, 46cfv 6334 . . . . . . . . . 10 class (((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))
4839, 47cfv 6334 . . . . . . . . 9 class ((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥)))))
4925, 28, 48csb 3855 . . . . . . . 8 class (𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥)))))
5021, 24, 49csb 3855 . . . . . . 7 class (algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥)))))
5118, 20, 50csb 3855 . . . . . 6 class (𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥)))))
5214, 17, 51csb 3855 . . . . 5 class ((𝑖𝑗) mPoly 𝑟) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥)))))
538, 13, 52cmpt 5122 . . . 4 class (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥))))))
545, 7, 53cmpt 5122 . . 3 class (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥)))))))
552, 3, 4, 4, 54cmpo 7142 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥))))))))
561, 55wceq 1538 1 wff selectVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ((𝑖𝑗) mPoly 𝑟) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝑖 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖𝑗) mVar 𝑟)‘𝑥))))))))
Colors of variables: wff setvar class
This definition is referenced by:  selvffval  20786
  Copyright terms: Public domain W3C validator