Theorem evlsevl

Description: Evaluation in a subring is the same as evaluation in the ring itself. (Contributed by SN, 9-Feb-2025)

	Ref	Expression
Hypotheses	evlsevl.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsevl.o	$$⊢O=I\mathrm{eval}S$$
	evlsevl.w	$$⊢W=I\mathrm{mPoly}U$$
	evlsevl.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsevl.b	$$⊢B={\mathrm{Base}}_W$$
	evlsevl.i	$$⊢\phi \to I\in V$$
	evlsevl.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsevl.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsevl.f	$$⊢\phi \to F\in B$$
Assertion	evlsevl	$$⊢\phi \to Q\left(F\right)=O\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlsevl.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		evlsevl.o	$$⊢O=I\mathrm{eval}S$$
3		evlsevl.w	$$⊢W=I\mathrm{mPoly}U$$
4		evlsevl.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		evlsevl.b	$$⊢B={\mathrm{Base}}_W$$
6		evlsevl.i	$$⊢\phi \to I\in V$$
7		evlsevl.s	$$⊢\phi \to S\in \mathrm{CRing}$$
8		evlsevl.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
9		evlsevl.f	$$⊢\phi \to F\in B$$
10		eqid	$$⊢\left(x\in R⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)=\left(x\in R⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)$$
11		sneq	$$⊢x=F\left(b\right)\to \left\{x\right\}=\left\{F\left(b\right)\right\}$$
12	11	xpeq2d	$$⊢x=F\left(b\right)\to \left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}=\left({{\mathrm{Base}}_S}^I\right)\times \left\{F\left(b\right)\right\}$$
13		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
14		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
15	3 13 5 14 9	mplelf	$$⊢\phi \to F:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_U$$
16	15	ffvelcdmda	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to F\left(b\right)\in {\mathrm{Base}}_U$$
17	4	subrgbas	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R={\mathrm{Base}}_U$$
18	8 17	syl	$$⊢\phi \to R={\mathrm{Base}}_U$$
19	18	adantr	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to R={\mathrm{Base}}_U$$
20	16 19	eleqtrrd	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to F\left(b\right)\in R$$
21		ovexd	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to {{\mathrm{Base}}_S}^I\in \mathrm{V}$$
22		snex	$$⊢\left\{F\left(b\right)\right\}\in \mathrm{V}$$
23	22	a1i	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left\{F\left(b\right)\right\}\in \mathrm{V}$$
24	21 23	xpexd	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left({{\mathrm{Base}}_S}^I\right)\times \left\{F\left(b\right)\right\}\in \mathrm{V}$$
25	10 12 20 24	fvmptd3	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(x\in R⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)=\left({{\mathrm{Base}}_S}^I\right)\times \left\{F\left(b\right)\right\}$$
26		eqid	$$⊢\left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)=\left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)$$
27		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
28	27	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq {\mathrm{Base}}_S$$
29	8 28	syl	$$⊢\phi \to R\subseteq {\mathrm{Base}}_S$$
30	29	adantr	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to R\subseteq {\mathrm{Base}}_S$$
31	30 20	sseldd	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to F\left(b\right)\in {\mathrm{Base}}_S$$
32	26 12 31 24	fvmptd3	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)=\left({{\mathrm{Base}}_S}^I\right)\times \left\{F\left(b\right)\right\}$$
33	25 32	eqtr4d	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(x\in R⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)=\left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)$$
34	33	oveq1d	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(x\in R⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)=\left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)$$
35	34	mpteq2dva	$$⊢\phi \to \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(x\in R⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)=\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
36	35	oveq2d	$$⊢\phi \to \underset{b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)}}\left(\left(x\in R⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)=\underset{b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)}}\left(\left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
37		eqid	$$⊢S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)=S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)$$
38		eqid	$$⊢{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}={\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
39		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}={\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}$$
40		eqid	$$⊢{\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}={\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
41		eqid	$$⊢\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)=\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)$$
42	1 3 5 14 27 4 37 38 39 40 10 41 6 7 8 9	evlsvval	$$⊢\phi \to Q\left(F\right)=\underset{b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)}}\left(\left(x\in R⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
43	2 27	evlval	$$⊢O=\left(I\mathrm{evalSub}S\right)\left({\mathrm{Base}}_S\right)$$
44	43	fveq1i	$$⊢O\left(F\right)=\left(I\mathrm{evalSub}S\right)\left({\mathrm{Base}}_S\right)\left(F\right)$$
45		eqid	$$⊢\left(I\mathrm{evalSub}S\right)\left({\mathrm{Base}}_S\right)=\left(I\mathrm{evalSub}S\right)\left({\mathrm{Base}}_S\right)$$
46		eqid	$$⊢I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S\right)=I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S\right)$$
47		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S\right)\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S\right)\right)}$$
48		eqid	$$⊢S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S=S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S$$
49	7	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
50	27	subrgid	$$⊢S\in \mathrm{Ring}\to {\mathrm{Base}}_S\in \mathrm{SubRing}\left(S\right)$$
51	49 50	syl	$$⊢\phi \to {\mathrm{Base}}_S\in \mathrm{SubRing}\left(S\right)$$
52		eqid	$$⊢I\mathrm{mPoly}S=I\mathrm{mPoly}S$$
53		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
54	3 4 5 52 53 6 8 9	mplsubrgcl	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
55	27	ressid	$$⊢S\in \mathrm{CRing}\to S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S=S$$
56	7 55	syl	$$⊢\phi \to S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S=S$$
57	56	oveq2d	$$⊢\phi \to I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S\right)=I\mathrm{mPoly}S$$
58	57	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S\right)\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
59	54 58	eleqtrrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}{\mathrm{Base}}_S\right)\right)}$$
60	45 46 47 14 27 48 37 38 39 40 26 41 6 7 51 59	evlsvval	$$⊢\phi \to \left(I\mathrm{evalSub}S\right)\left({\mathrm{Base}}_S\right)\left(F\right)=\underset{b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)}}\left(\left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
61	44 60	eqtrid	$$⊢\phi \to O\left(F\right)=\underset{b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)}}\left(\left(x\in {\mathrm{Base}}_S⟼\left({{\mathrm{Base}}_S}^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left({{\mathrm{Base}}_S}^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
62	36 42 61	3eqtr4d	$$⊢\phi \to Q\left(F\right)=O\left(F\right)$$