Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-evls Structured version   Visualization version   GIF version

Definition df-evls 19327
 Description: Define the evaluation map for the polynomial algebra. The function ((𝐼 evalSub 𝑆)‘𝑅):𝑉⟶(𝑆 ↑𝑚 (𝑆 ↑𝑚 𝐼)) makes sense when 𝐼 is an index set, 𝑆 is a ring, 𝑅 is a subring of 𝑆, and where 𝑉 is the set of polynomials in (𝐼 mPoly 𝑅). This function maps an element of the formal polynomial algebra (with coefficients in 𝑅) to a function from assignments 𝐼⟶𝑆 of the variables to elements of 𝑆 formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015.)
Assertion
Ref Expression
df-evls evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ (Base‘𝑠) / 𝑏(𝑟 ∈ (SubRing‘𝑠) ↦ (𝑖 mPoly (𝑠s 𝑟)) / 𝑤(𝑓 ∈ (𝑤 RingHom (𝑠s (𝑏𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥)))))))
Distinct variable group:   𝑓,𝑏,𝑔,𝑖,𝑟,𝑠,𝑤,𝑥

Detailed syntax breakdown of Definition df-evls
StepHypRef Expression
1 ces 19325 . 2 class evalSub
2 vi . . 3 setvar 𝑖
3 vs . . 3 setvar 𝑠
4 cvv 3173 . . 3 class V
5 ccrg 18371 . . 3 class CRing
6 vb . . . 4 setvar 𝑏
73cv 1474 . . . . 5 class 𝑠
8 cbs 15695 . . . . 5 class Base
97, 8cfv 5804 . . . 4 class (Base‘𝑠)
10 vr . . . . 5 setvar 𝑟
11 csubrg 18599 . . . . . 6 class SubRing
127, 11cfv 5804 . . . . 5 class (SubRing‘𝑠)
13 vw . . . . . 6 setvar 𝑤
142cv 1474 . . . . . . 7 class 𝑖
1510cv 1474 . . . . . . . 8 class 𝑟
16 cress 15696 . . . . . . . 8 class s
177, 15, 16co 6549 . . . . . . 7 class (𝑠s 𝑟)
18 cmpl 19174 . . . . . . 7 class mPoly
1914, 17, 18co 6549 . . . . . 6 class (𝑖 mPoly (𝑠s 𝑟))
20 vf . . . . . . . . . . 11 setvar 𝑓
2120cv 1474 . . . . . . . . . 10 class 𝑓
2213cv 1474 . . . . . . . . . . 11 class 𝑤
23 cascl 19132 . . . . . . . . . . 11 class algSc
2422, 23cfv 5804 . . . . . . . . . 10 class (algSc‘𝑤)
2521, 24ccom 5042 . . . . . . . . 9 class (𝑓 ∘ (algSc‘𝑤))
26 vx . . . . . . . . . 10 setvar 𝑥
276cv 1474 . . . . . . . . . . . 12 class 𝑏
28 cmap 7744 . . . . . . . . . . . 12 class 𝑚
2927, 14, 28co 6549 . . . . . . . . . . 11 class (𝑏𝑚 𝑖)
3026cv 1474 . . . . . . . . . . . 12 class 𝑥
3130csn 4125 . . . . . . . . . . 11 class {𝑥}
3229, 31cxp 5036 . . . . . . . . . 10 class ((𝑏𝑚 𝑖) × {𝑥})
3326, 15, 32cmpt 4643 . . . . . . . . 9 class (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥}))
3425, 33wceq 1475 . . . . . . . 8 wff (𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥}))
35 cmvr 19173 . . . . . . . . . . 11 class mVar
3614, 17, 35co 6549 . . . . . . . . . 10 class (𝑖 mVar (𝑠s 𝑟))
3721, 36ccom 5042 . . . . . . . . 9 class (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟)))
38 vg . . . . . . . . . . 11 setvar 𝑔
3938cv 1474 . . . . . . . . . . . 12 class 𝑔
4030, 39cfv 5804 . . . . . . . . . . 11 class (𝑔𝑥)
4138, 29, 40cmpt 4643 . . . . . . . . . 10 class (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥))
4226, 14, 41cmpt 4643 . . . . . . . . 9 class (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥)))
4337, 42wceq 1475 . . . . . . . 8 wff (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥)))
4434, 43wa 383 . . . . . . 7 wff ((𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥))))
45 cpws 15930 . . . . . . . . 9 class s
467, 29, 45co 6549 . . . . . . . 8 class (𝑠s (𝑏𝑚 𝑖))
47 crh 18535 . . . . . . . 8 class RingHom
4822, 46, 47co 6549 . . . . . . 7 class (𝑤 RingHom (𝑠s (𝑏𝑚 𝑖)))
4944, 20, 48crio 6510 . . . . . 6 class (𝑓 ∈ (𝑤 RingHom (𝑠s (𝑏𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥)))))
5013, 19, 49csb 3499 . . . . 5 class (𝑖 mPoly (𝑠s 𝑟)) / 𝑤(𝑓 ∈ (𝑤 RingHom (𝑠s (𝑏𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥)))))
5110, 12, 50cmpt 4643 . . . 4 class (𝑟 ∈ (SubRing‘𝑠) ↦ (𝑖 mPoly (𝑠s 𝑟)) / 𝑤(𝑓 ∈ (𝑤 RingHom (𝑠s (𝑏𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥))))))
526, 9, 51csb 3499 . . 3 class (Base‘𝑠) / 𝑏(𝑟 ∈ (SubRing‘𝑠) ↦ (𝑖 mPoly (𝑠s 𝑟)) / 𝑤(𝑓 ∈ (𝑤 RingHom (𝑠s (𝑏𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥))))))
532, 3, 4, 5, 52cmpt2 6551 . 2 class (𝑖 ∈ V, 𝑠 ∈ CRing ↦ (Base‘𝑠) / 𝑏(𝑟 ∈ (SubRing‘𝑠) ↦ (𝑖 mPoly (𝑠s 𝑟)) / 𝑤(𝑓 ∈ (𝑤 RingHom (𝑠s (𝑏𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥)))))))
541, 53wceq 1475 1 wff evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ (Base‘𝑠) / 𝑏(𝑟 ∈ (SubRing‘𝑠) ↦ (𝑖 mPoly (𝑠s 𝑟)) / 𝑤(𝑓 ∈ (𝑤 RingHom (𝑠s (𝑏𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥𝑟 ↦ ((𝑏𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠s 𝑟))) = (𝑥𝑖 ↦ (𝑔 ∈ (𝑏𝑚 𝑖) ↦ (𝑔𝑥)))))))
 Colors of variables: wff setvar class This definition is referenced by:  reldmevls  19338  mpfrcl  19339  evlsval  19340
 Copyright terms: Public domain W3C validator