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 = i ∈ V , r ∈ V ⟼ j ∈ 𝒫 i ⟼ f ∈ Base i mPoly r ⟼ ⦋ i ∖ j mPoly r / u⦌ ⦋ j mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslv class selectVars
1 vi setvar i
2 cvv class V
3 vr setvar r
4 vj setvar j
5 1 cv setvar i
6 5 cpw class 𝒫 i
7 vf setvar f
8 cbs class Base
9 cmpl class mPoly
10 3 cv setvar r
11 5 10 9 co class i mPoly r
12 11 8 cfv class Base i mPoly r
13 4 cv setvar j
14 5 13 cdif class i ∖ j
15 14 10 9 co class i ∖ j mPoly r
16 vu setvar u
17 16 cv setvar u
18 13 17 9 co class j mPoly u
19 vt setvar t
20 cascl class algSc
21 19 cv setvar t
22 21 20 cfv class algSc ⁡ t
23 vc setvar c
24 23 cv setvar c
25 17 20 cfv class algSc ⁡ u
26 24 25 ccom class c ∘ algSc ⁡ u
27 vd setvar d
28 ces class evalSub
29 5 21 28 co class i evalSub t
30 27 cv setvar d
31 30 crn class ran ⁡ d
32 31 29 cfv class i evalSub t ⁡ ran ⁡ d
33 7 cv setvar f
34 30 33 ccom class d ∘ f
35 34 32 cfv class i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f
36 vx setvar x
37 36 cv setvar x
38 37 13 wcel wff x ∈ j
39 cmvr class mVar
40 13 17 39 co class j mVar u
41 37 40 cfv class j mVar u ⁡ x
42 14 10 39 co class i ∖ j mVar r
43 37 42 cfv class i ∖ j mVar r ⁡ x
44 43 24 cfv class c ⁡ i ∖ j mVar r ⁡ x
45 38 41 44 cif class if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
46 36 5 45 cmpt class x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
47 46 35 cfv class i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
48 27 26 47 csb class ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
49 23 22 48 csb class ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
50 19 18 49 csb class ⦋ j mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
51 16 15 50 csb class ⦋ i ∖ j mPoly r / u⦌ ⦋ j mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
52 7 12 51 cmpt class f ∈ Base i mPoly r ⟼ ⦋ i ∖ j mPoly r / u⦌ ⦋ j mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
53 4 6 52 cmpt class j ∈ 𝒫 i ⟼ f ∈ Base i mPoly r ⟼ ⦋ i ∖ j mPoly r / u⦌ ⦋ j mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
54 1 3 2 2 53 cmpo class i ∈ V , r ∈ V ⟼ j ∈ 𝒫 i ⟼ f ∈ Base i mPoly r ⟼ ⦋ i ∖ j mPoly r / u⦌ ⦋ j mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x
55 0 54 wceq wff selectVars = i ∈ V , r ∈ V ⟼ j ∈ 𝒫 i ⟼ f ∈ Base i mPoly r ⟼ ⦋ i ∖ j mPoly r / u⦌ ⦋ j mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ i evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ i ⟼ if x ∈ j j mVar u ⁡ x c ⁡ i ∖ j mVar r ⁡ x