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

Definition df-evls 21634
Description: Define the evaluation map for the polynomial algebra. The function ((𝐼 evalSub 𝑆)β€˜π‘…):π‘‰βŸΆ(𝑆 ↑m (𝑆 ↑m 𝐼)) 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 (𝑏 ↑m 𝑖)))((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯)))))))
Distinct variable group:   𝑓,𝑏,𝑔,𝑖,π‘Ÿ,𝑠,𝑀,π‘₯

Detailed syntax breakdown of Definition df-evls
StepHypRef Expression
1 ces 21632 . 2 class evalSub
2 vi . . 3 setvar 𝑖
3 vs . . 3 setvar 𝑠
4 cvv 3474 . . 3 class V
5 ccrg 20056 . . 3 class CRing
6 vb . . . 4 setvar 𝑏
73cv 1540 . . . . 5 class 𝑠
8 cbs 17143 . . . . 5 class Base
97, 8cfv 6543 . . . 4 class (Baseβ€˜π‘ )
10 vr . . . . 5 setvar π‘Ÿ
11 csubrg 20314 . . . . . 6 class SubRing
127, 11cfv 6543 . . . . 5 class (SubRingβ€˜π‘ )
13 vw . . . . . 6 setvar 𝑀
142cv 1540 . . . . . . 7 class 𝑖
1510cv 1540 . . . . . . . 8 class π‘Ÿ
16 cress 17172 . . . . . . . 8 class β†Ύs
177, 15, 16co 7408 . . . . . . 7 class (𝑠 β†Ύs π‘Ÿ)
18 cmpl 21458 . . . . . . 7 class mPoly
1914, 17, 18co 7408 . . . . . 6 class (𝑖 mPoly (𝑠 β†Ύs π‘Ÿ))
20 vf . . . . . . . . . . 11 setvar 𝑓
2120cv 1540 . . . . . . . . . 10 class 𝑓
2213cv 1540 . . . . . . . . . . 11 class 𝑀
23 cascl 21406 . . . . . . . . . . 11 class algSc
2422, 23cfv 6543 . . . . . . . . . 10 class (algScβ€˜π‘€)
2521, 24ccom 5680 . . . . . . . . 9 class (𝑓 ∘ (algScβ€˜π‘€))
26 vx . . . . . . . . . 10 setvar π‘₯
276cv 1540 . . . . . . . . . . . 12 class 𝑏
28 cmap 8819 . . . . . . . . . . . 12 class ↑m
2927, 14, 28co 7408 . . . . . . . . . . 11 class (𝑏 ↑m 𝑖)
3026cv 1540 . . . . . . . . . . . 12 class π‘₯
3130csn 4628 . . . . . . . . . . 11 class {π‘₯}
3229, 31cxp 5674 . . . . . . . . . 10 class ((𝑏 ↑m 𝑖) Γ— {π‘₯})
3326, 15, 32cmpt 5231 . . . . . . . . 9 class (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯}))
3425, 33wceq 1541 . . . . . . . 8 wff (𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯}))
35 cmvr 21457 . . . . . . . . . . 11 class mVar
3614, 17, 35co 7408 . . . . . . . . . 10 class (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))
3721, 36ccom 5680 . . . . . . . . 9 class (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ)))
38 vg . . . . . . . . . . 11 setvar 𝑔
3938cv 1540 . . . . . . . . . . . 12 class 𝑔
4030, 39cfv 6543 . . . . . . . . . . 11 class (π‘”β€˜π‘₯)
4138, 29, 40cmpt 5231 . . . . . . . . . 10 class (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯))
4226, 14, 41cmpt 5231 . . . . . . . . 9 class (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯)))
4337, 42wceq 1541 . . . . . . . 8 wff (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯)))
4434, 43wa 396 . . . . . . 7 wff ((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯))))
45 cpws 17391 . . . . . . . . 9 class ↑s
467, 29, 45co 7408 . . . . . . . 8 class (𝑠 ↑s (𝑏 ↑m 𝑖))
47 crh 20247 . . . . . . . 8 class RingHom
4822, 46, 47co 7408 . . . . . . 7 class (𝑀 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))
4944, 20, 48crio 7363 . . . . . 6 class (℩𝑓 ∈ (𝑀 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯)))))
5013, 19, 49csb 3893 . . . . 5 class ⦋(𝑖 mPoly (𝑠 β†Ύs π‘Ÿ)) / π‘€β¦Œ(℩𝑓 ∈ (𝑀 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯)))))
5110, 12, 50cmpt 5231 . . . 4 class (π‘Ÿ ∈ (SubRingβ€˜π‘ ) ↦ ⦋(𝑖 mPoly (𝑠 β†Ύs π‘Ÿ)) / π‘€β¦Œ(℩𝑓 ∈ (𝑀 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯))))))
526, 9, 51csb 3893 . . 3 class ⦋(Baseβ€˜π‘ ) / π‘β¦Œ(π‘Ÿ ∈ (SubRingβ€˜π‘ ) ↦ ⦋(𝑖 mPoly (𝑠 β†Ύs π‘Ÿ)) / π‘€β¦Œ(℩𝑓 ∈ (𝑀 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯))))))
532, 3, 4, 5, 52cmpo 7410 . 2 class (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Baseβ€˜π‘ ) / π‘β¦Œ(π‘Ÿ ∈ (SubRingβ€˜π‘ ) ↦ ⦋(𝑖 mPoly (𝑠 β†Ύs π‘Ÿ)) / π‘€β¦Œ(℩𝑓 ∈ (𝑀 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯)))))))
541, 53wceq 1541 1 wff evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Baseβ€˜π‘ ) / π‘β¦Œ(π‘Ÿ ∈ (SubRingβ€˜π‘ ) ↦ ⦋(𝑖 mPoly (𝑠 β†Ύs π‘Ÿ)) / π‘€β¦Œ(℩𝑓 ∈ (𝑀 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algScβ€˜π‘€)) = (π‘₯ ∈ π‘Ÿ ↦ ((𝑏 ↑m 𝑖) Γ— {π‘₯})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 β†Ύs π‘Ÿ))) = (π‘₯ ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (π‘”β€˜π‘₯)))))))
Colors of variables: wff setvar class
This definition is referenced by:  reldmevls  21646  mpfrcl  21647  evlsval  21648
  Copyright terms: Public domain W3C validator