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

Step	Hyp	Ref	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 𝑗
6	2	cv 1474	. . . . 5 class 𝑖
7	6	cpw 4108	. . . 4 class 𝒫 𝑖
8		vf	. . . . 5 setvar 𝑓
9	3	cv 1474	. . . . . 6 class 𝑟
10		cmpl 19174	. . . . . 6 class mPoly
11	6, 9, 10	co 6549	. . . . 5 class (𝑖 mPoly 𝑟)
12		vs	. . . . . 6 setvar 𝑠
13	5	cv 1474	. . . . . . . 8 class 𝑗
14	6, 13	cdif 3537	. . . . . . 7 class (𝑖 ∖ 𝑗)
15	14, 9, 10	co 6549	. . . . . 6 class ((𝑖 ∖ 𝑗) mPoly 𝑟)
16		vc	. . . . . . 7 setvar 𝑐
17		vx	. . . . . . . 8 setvar 𝑥
18	12	cv 1474	. . . . . . . . 9 class 𝑠
19		csca 15771	. . . . . . . . 9 class Scalar
20	18, 19	cfv 5804	. . . . . . . 8 class (Scalar‘𝑠)
21	17	cv 1474	. . . . . . . . 9 class 𝑥
22		cur 18324	. . . . . . . . . 10 class 1r
23	18, 22	cfv 5804	. . . . . . . . 9 class (1r‘𝑠)
24		cvsca 15772	. . . . . . . . . 10 class ·𝑠
25	18, 24	cfv 5804	. . . . . . . . 9 class ( ·𝑠 ‘𝑠)
26	21, 23, 25	co 6549	. . . . . . . 8 class (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠))
27	17, 20, 26	cmpt 4643	. . . . . . 7 class (𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠)))
28	17, 5	wel 1978	. . . . . . . . . 10 wff 𝑥 ∈ 𝑗
29		cmvr 19173	. . . . . . . . . . . 12 class mVar
30	13, 15, 29	co 6549	. . . . . . . . . . 11 class (𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))
31	21, 30	cfv 5804	. . . . . . . . . 10 class ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥)
32	16	cv 1474	. . . . . . . . . . 11 class 𝑐
33	14, 9, 29	co 6549	. . . . . . . . . . . 12 class ((𝑖 ∖ 𝑗) mVar 𝑟)
34	21, 33	cfv 5804	. . . . . . . . . . 11 class (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)
35	32, 34	ccom 5042	. . . . . . . . . 10 class (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))
36	28, 31, 35	cif 4036	. . . . . . . . 9 class if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))
37	17, 6, 36	cmpt 4643	. . . . . . . 8 class (𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))
38	8	cv 1474	. . . . . . . . . 10 class 𝑓
39	32, 38	ccom 5042	. . . . . . . . 9 class (𝑐 ∘ 𝑓)
40		cimas 15987	. . . . . . . . . . 11 class “s
41	32, 9, 40	co 6549	. . . . . . . . . 10 class (𝑐 “s 𝑟)
42		ces 19325	. . . . . . . . . . 11 class evalSub
43	6, 18, 42	co 6549	. . . . . . . . . 10 class (𝑖 evalSub 𝑠)
44	41, 43	cfv 5804	. . . . . . . . 9 class ((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))
45	39, 44	cfv 5804	. . . . . . . 8 class (((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))
46	37, 45	cfv 5804	. . . . . . 7 class ((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))
47	16, 27, 46	csb 3499	. . . . . 6 class ⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))
48	12, 15, 47	csb 3499	. . . . 5 class ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))
49	8, 11, 48	cmpt 4643	. . . 4 class (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))
50	5, 7, 49	cmpt 4643	. . 3 class (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))))
51	2, 3, 4, 4, 50	cmpt2 6551	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))))
52	1, 51	wceq 1475	1 wff selectVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠 ‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))))

This definition is referenced by: (None)