This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑟 ) ‘ 𝑥 ) ) ) ) ) ) ) )