Definition df-evls 19506

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

Step	Hyp	Ref	Expression
1		ces 19504	. 2 class evalSub
2		vi	. . 3 setvar 𝑖
3		vs	. . 3 setvar 𝑠
4		cvv 3200	. . 3 class V
5		ccrg 18548	. . 3 class CRing
6		vb	. . . 4 setvar 𝑏
7	3	cv 1482	. . . . 5 class 𝑠
8		cbs 15857	. . . . 5 class Base
9	7, 8	cfv 5888	. . . 4 class (Base‘𝑠)
10		vr	. . . . 5 setvar 𝑟
11		csubrg 18776	. . . . . 6 class SubRing
12	7, 11	cfv 5888	. . . . 5 class (SubRing‘𝑠)
13		vw	. . . . . 6 setvar 𝑤
14	2	cv 1482	. . . . . . 7 class 𝑖
15	10	cv 1482	. . . . . . . 8 class 𝑟
16		cress 15858	. . . . . . . 8 class ↾s
17	7, 15, 16	co 6650	. . . . . . 7 class (𝑠 ↾s 𝑟)
18		cmpl 19353	. . . . . . 7 class mPoly
19	14, 17, 18	co 6650	. . . . . 6 class (𝑖 mPoly (𝑠 ↾s 𝑟))
20		vf	. . . . . . . . . . 11 setvar 𝑓
21	20	cv 1482	. . . . . . . . . 10 class 𝑓
22	13	cv 1482	. . . . . . . . . . 11 class 𝑤
23		cascl 19311	. . . . . . . . . . 11 class algSc
24	22, 23	cfv 5888	. . . . . . . . . 10 class (algSc‘𝑤)
25	21, 24	ccom 5118	. . . . . . . . 9 class (𝑓 ∘ (algSc‘𝑤))
26		vx	. . . . . . . . . 10 setvar 𝑥
27	6	cv 1482	. . . . . . . . . . . 12 class 𝑏
28		cmap 7857	. . . . . . . . . . . 12 class ↑𝑚
29	27, 14, 28	co 6650	. . . . . . . . . . 11 class (𝑏 ↑𝑚 𝑖)
30	26	cv 1482	. . . . . . . . . . . 12 class 𝑥
31	30	csn 4177	. . . . . . . . . . 11 class {𝑥}
32	29, 31	cxp 5112	. . . . . . . . . 10 class ((𝑏 ↑𝑚 𝑖) × {𝑥})
33	26, 15, 32	cmpt 4729	. . . . . . . . 9 class (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥}))
34	25, 33	wceq 1483	. . . . . . . 8 wff (𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥}))
35		cmvr 19352	. . . . . . . . . . 11 class mVar
36	14, 17, 35	co 6650	. . . . . . . . . 10 class (𝑖 mVar (𝑠 ↾s 𝑟))
37	21, 36	ccom 5118	. . . . . . . . 9 class (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟)))
38		vg	. . . . . . . . . . 11 setvar 𝑔
39	38	cv 1482	. . . . . . . . . . . 12 class 𝑔
40	30, 39	cfv 5888	. . . . . . . . . . 11 class (𝑔‘𝑥)
41	38, 29, 40	cmpt 4729	. . . . . . . . . 10 class (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥))
42	26, 14, 41	cmpt 4729	. . . . . . . . 9 class (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥)))
43	37, 42	wceq 1483	. . . . . . . 8 wff (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥)))
44	34, 43	wa 384	. . . . . . 7 wff ((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥))))
45		cpws 16107	. . . . . . . . 9 class ↑s
46	7, 29, 45	co 6650	. . . . . . . 8 class (𝑠 ↑s (𝑏 ↑𝑚 𝑖))
47		crh 18712	. . . . . . . 8 class RingHom
48	22, 46, 47	co 6650	. . . . . . 7 class (𝑤 RingHom (𝑠 ↑s (𝑏 ↑𝑚 𝑖)))
49	44, 20, 48	crio 6610	. . . . . 6 class (℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥)))))
50	13, 19, 49	csb 3533	. . . . 5 class ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥)))))
51	10, 12, 50	cmpt 4729	. . . 4 class (𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥))))))
52	6, 9, 51	csb 3533	. . 3 class ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥))))))
53	2, 3, 4, 5, 52	cmpt2 6652	. 2 class (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥)))))))
54	1, 53	wceq 1483	1 wff evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑𝑚 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑𝑚 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑𝑚 𝑖) ↦ (𝑔‘𝑥)))))))

This definition is referenced by:  reldmevls  19517  mpfrcl  19518  evlsval  19519