Metamath Proof Explorer

Definition df-evls

Description: Define the evaluation map for the polynomial algebra. The function ( ( I evalSub S )R ) : V --> ( S ^m ( S ^m I ) ) makes sense when I is an index set, S is a ring, R is a subring of S , and where V is the set of polynomials in ( I mPoly R ) . This function maps an element of the formal polynomial algebra (with coefficients in R ) to a function from assignments I --> S of the variables to elements of S formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015)

Ref Expression
Assertion df-evls ⊢ evalSub = i ∈ V , s ∈ CRing ⟼ ⦋ Base s / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ces class evalSub
1 vi setvar i
2 cvv class V
3 vs setvar s
4 ccrg class CRing
5 cbs class Base
6 3 cv setvar s
7 6 5 cfv class Base s
8 vb setvar b
9 vr setvar r
10 csubrg class SubRing
11 6 10 cfv class SubRing ⁡ s
12 1 cv setvar i
13 cmpl class mPoly
14 cress class ↾ 𝑠
15 9 cv setvar r
16 6 15 14 co class s ↾ 𝑠 r
17 12 16 13 co class i mPoly s ↾ 𝑠 r
18 vw setvar w
19 vf setvar f
20 18 cv setvar w
21 crh class RingHom
22 cpws class ↑ 𝑠
23 8 cv setvar b
24 cmap class ↑ 𝑚
25 23 12 24 co class b i
26 6 25 22 co class s ↑ 𝑠 b i
27 20 26 21 co class w RingHom s ↑ 𝑠 b i
28 19 cv setvar f
29 cascl class algSc
30 20 29 cfv class algSc ⁡ w
31 28 30 ccom class f ∘ algSc ⁡ w
32 vx setvar x
33 32 cv setvar x
34 33 csn class x
35 25 34 cxp class b i × x
36 32 15 35 cmpt class x ∈ r ⟼ b i × x
37 31 36 wceq wff f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x
38 cmvr class mVar
39 12 16 38 co class i mVar s ↾ 𝑠 r
40 28 39 ccom class f ∘ i mVar s ↾ 𝑠 r
41 vg setvar g
42 41 cv setvar g
43 33 42 cfv class g ⁡ x
44 41 25 43 cmpt class g ∈ b i ⟼ g ⁡ x
45 32 12 44 cmpt class x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
46 40 45 wceq wff f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
47 37 46 wa wff f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
48 47 19 27 crio class ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
49 18 17 48 csb class ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
50 9 11 49 cmpt class r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
51 8 7 50 csb class ⦋ Base s / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
52 1 3 2 4 51 cmpo class i ∈ V , s ∈ CRing ⟼ ⦋ Base s / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
53 0 52 wceq wff evalSub = i ∈ V , s ∈ CRing ⟼ ⦋ Base s / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x