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 = ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ces	⊢ evalSub
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		ccrg	⊢ CRing
5		cbs	⊢ Base
6	3	cv	⊢ 𝑠
7	6 5	cfv	⊢ ( Base ‘ 𝑠 )
8		vb	⊢ 𝑏
9		vr	⊢ 𝑟
10		csubrg	⊢ SubRing
11	6 10	cfv	⊢ ( SubRing ‘ 𝑠 )
12	1	cv	⊢ 𝑖
13		cmpl	⊢ mPoly
14		cress	⊢ ↾s
15	9	cv	⊢ 𝑟
16	6 15 14	co	⊢ ( 𝑠 ↾s 𝑟 )
17	12 16 13	co	⊢ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) )
18		vw	⊢ 𝑤
19		vf	⊢ 𝑓
20	18	cv	⊢ 𝑤
21		crh	⊢ RingHom
22		cpws	⊢ ↑s
23	8	cv	⊢ 𝑏
24		cmap	⊢ ↑m
25	23 12 24	co	⊢ ( 𝑏 ↑m 𝑖 )
26	6 25 22	co	⊢ ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) )
27	20 26 21	co	⊢ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) )
28	19	cv	⊢ 𝑓
29		cascl	⊢ algSc
30	20 29	cfv	⊢ ( algSc ‘ 𝑤 )
31	28 30	ccom	⊢ ( 𝑓 ∘ ( algSc ‘ 𝑤 ) )
32		vx	⊢ 𝑥
33	32	cv	⊢ 𝑥
34	33	csn	⊢ { 𝑥 }
35	25 34	cxp	⊢ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } )
36	32 15 35	cmpt	⊢ ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) )
37	31 36	wceq	⊢ ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) )
38		cmvr	⊢ mVar
39	12 16 38	co	⊢ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) )
40	28 39	ccom	⊢ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) )
41		vg	⊢ 𝑔
42	41	cv	⊢ 𝑔
43	33 42	cfv	⊢ ( 𝑔 ‘ 𝑥 )
44	41 25 43	cmpt	⊢ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) )
45	32 12 44	cmpt	⊢ ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
46	40 45	wceq	⊢ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
47	37 46	wa	⊢ ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) )
48	47 19 27	crio	⊢ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) )
49	18 17 48	csb	⊢ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) )
50	9 11 49	cmpt	⊢ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
51	8 7 50	csb	⊢ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
52	1 3 2 4 51	cmpo	⊢ ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
53	0 52	wceq	⊢ evalSub = ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )