Definition df-selv

Description: Define the "variable selection" function. The function ( ( I selectVars R )J ) maps elements of ( I mPoly R ) bijectively onto ( J mPoly ( ( I \ J ) mPoly R ) ) in the natural way, for example if I = { x , y } and J = { y } it would map 1 + x + y + x y e. ( { x , y } mPoly ZZ ) to ( 1 + x ) + ( 1 + x ) y e. ( { y } mPoly ( { x } mPoly ZZ ) ) . 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)

	Ref	Expression
Assertion	df-selv	⊢ selectVars = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ⦋ ( ( 𝑖 ∖ 𝑗 ) mPoly 𝑟 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) ) ) )

Detailed syntax breakdown

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