Definition df-evls 22098

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

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

This definition is referenced by:  reldmevls  22108  mpfrcl  22109  evlsval  22110