Definition df-selv 22136

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

Step	Hyp	Ref	Expression
1		cslv 22132	. 2 class selectVars
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3480	. . 3 class V
5		vj	. . . 4 setvar 𝑗
6	2	cv 1539	. . . . 5 class 𝑖
7	6	cpw 4600	. . . 4 class 𝒫 𝑖
8		vf	. . . . 5 setvar 𝑓
9	3	cv 1539	. . . . . . 7 class 𝑟
10		cmpl 21926	. . . . . . 7 class mPoly
11	6, 9, 10	co 7431	. . . . . 6 class (𝑖 mPoly 𝑟)
12		cbs 17247	. . . . . 6 class Base
13	11, 12	cfv 6561	. . . . 5 class (Base‘(𝑖 mPoly 𝑟))
14		vu	. . . . . 6 setvar 𝑢
15	5	cv 1539	. . . . . . . 8 class 𝑗
16	6, 15	cdif 3948	. . . . . . 7 class (𝑖 ∖ 𝑗)
17	16, 9, 10	co 7431	. . . . . 6 class ((𝑖 ∖ 𝑗) mPoly 𝑟)
18		vt	. . . . . . 7 setvar 𝑡
19	14	cv 1539	. . . . . . . 8 class 𝑢
20	15, 19, 10	co 7431	. . . . . . 7 class (𝑗 mPoly 𝑢)
21		vc	. . . . . . . 8 setvar 𝑐
22	18	cv 1539	. . . . . . . . 9 class 𝑡
23		cascl 21872	. . . . . . . . 9 class algSc
24	22, 23	cfv 6561	. . . . . . . 8 class (algSc‘𝑡)
25		vd	. . . . . . . . 9 setvar 𝑑
26	21	cv 1539	. . . . . . . . . 10 class 𝑐
27	19, 23	cfv 6561	. . . . . . . . . 10 class (algSc‘𝑢)
28	26, 27	ccom 5689	. . . . . . . . 9 class (𝑐 ∘ (algSc‘𝑢))
29		vx	. . . . . . . . . . 11 setvar 𝑥
30	29, 5	wel 2109	. . . . . . . . . . . 12 wff 𝑥 ∈ 𝑗
31	29	cv 1539	. . . . . . . . . . . . 13 class 𝑥
32		cmvr 21925	. . . . . . . . . . . . . 14 class mVar
33	15, 19, 32	co 7431	. . . . . . . . . . . . 13 class (𝑗 mVar 𝑢)
34	31, 33	cfv 6561	. . . . . . . . . . . 12 class ((𝑗 mVar 𝑢)‘𝑥)
35	16, 9, 32	co 7431	. . . . . . . . . . . . . 14 class ((𝑖 ∖ 𝑗) mVar 𝑟)
36	31, 35	cfv 6561	. . . . . . . . . . . . 13 class (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)
37	36, 26	cfv 6561	. . . . . . . . . . . 12 class (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))
38	30, 34, 37	cif 4525	. . . . . . . . . . 11 class if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))
39	29, 6, 38	cmpt 5225	. . . . . . . . . 10 class (𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))
40	25	cv 1539	. . . . . . . . . . . 12 class 𝑑
41	8	cv 1539	. . . . . . . . . . . 12 class 𝑓
42	40, 41	ccom 5689	. . . . . . . . . . 11 class (𝑑 ∘ 𝑓)
43	40	crn 5686	. . . . . . . . . . . 12 class ran 𝑑
44		ces 22096	. . . . . . . . . . . . 13 class evalSub
45	6, 22, 44	co 7431	. . . . . . . . . . . 12 class (𝑖 evalSub 𝑡)
46	43, 45	cfv 6561	. . . . . . . . . . 11 class ((𝑖 evalSub 𝑡)‘ran 𝑑)
47	42, 46	cfv 6561	. . . . . . . . . 10 class (((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))
48	39, 47	cfv 6561	. . . . . . . . 9 class ((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))
49	25, 28, 48	csb 3899	. . . . . . . 8 class ⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))
50	21, 24, 49	csb 3899	. . . . . . 7 class ⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))
51	18, 20, 50	csb 3899	. . . . . 6 class ⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))
52	14, 17, 51	csb 3899	. . . . 5 class ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))
53	8, 13, 52	cmpt 5225	. . . 4 class (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))
54	5, 7, 53	cmpt 5225	. . 3 class (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))))
55	2, 3, 4, 4, 54	cmpo 7433	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))))
56	1, 55	wceq 1540	1 wff selectVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))))

This definition is referenced by:  selvffval  22137