Theorem evls1var

Description: Univariate polynomial evaluation for subrings maps the variable to the identity function. (Contributed by AV, 13-Sep-2019)

	Ref	Expression
Hypotheses	evls1var.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	evls1var.x	$$⊢X={\mathrm{var}}_1\left(U\right)$$
	evls1var.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evls1var.b	$$⊢B={\mathrm{Base}}_S$$
	evls1var.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1var.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
Assertion	evls1var	$$⊢\phi \to Q\left(X\right)={\mathrm{I}\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		evls1var.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1var.x	$$⊢X={\mathrm{var}}_1\left(U\right)$$
3		evls1var.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		evls1var.b	$$⊢B={\mathrm{Base}}_S$$
5		evls1var.s	$$⊢\phi \to S\in \mathrm{CRing}$$
6		evls1var.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
7		eqid	$$⊢{\mathrm{var}}_1\left(S\right)={\mathrm{var}}_1\left(S\right)$$
8	7 6 3	subrgvr1	$$⊢\phi \to {\mathrm{var}}_1\left(S\right)={\mathrm{var}}_1\left(U\right)$$
9	2 8	eqtr4id	$$⊢\phi \to X={\mathrm{var}}_1\left(S\right)$$
10	9	fveq2d	$$⊢\phi \to Q\left(X\right)=Q\left({\mathrm{var}}_1\left(S\right)\right)$$
11		eqid	$$⊢\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)=\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)$$
12		eqid	$$⊢1_{𝑜}\mathrm{eval}S=1_{𝑜}\mathrm{eval}S$$
13		eqid	$$⊢1_{𝑜}\mathrm{mVar}U=1_{𝑜}\mathrm{mVar}U$$
14		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
15	14	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
16		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
17	16	a1i	$$⊢\phi \to \varnothing \in 1_{𝑜}$$
18	11 12 13 3 4 15 5 6 17	evlsvarsrng	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(\left(1_{𝑜}\mathrm{mVar}U\right)\left(\varnothing \right)\right)=\left(1_{𝑜}\mathrm{eval}S\right)\left(\left(1_{𝑜}\mathrm{mVar}U\right)\left(\varnothing \right)\right)$$
19	7	vr1val	$$⊢{\mathrm{var}}_1\left(S\right)=\left(1_{𝑜}\mathrm{mVar}S\right)\left(\varnothing \right)$$
20		eqid	$$⊢1_{𝑜}\mathrm{mVar}S=1_{𝑜}\mathrm{mVar}S$$
21	20 15 6 3	subrgmvr	$$⊢\phi \to 1_{𝑜}\mathrm{mVar}S=1_{𝑜}\mathrm{mVar}U$$
22	21	fveq1d	$$⊢\phi \to \left(1_{𝑜}\mathrm{mVar}S\right)\left(\varnothing \right)=\left(1_{𝑜}\mathrm{mVar}U\right)\left(\varnothing \right)$$
23	19 22	eqtrid	$$⊢\phi \to {\mathrm{var}}_1\left(S\right)=\left(1_{𝑜}\mathrm{mVar}U\right)\left(\varnothing \right)$$
24	23	fveq2d	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left({\mathrm{var}}_1\left(S\right)\right)=\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(\left(1_{𝑜}\mathrm{mVar}U\right)\left(\varnothing \right)\right)$$
25	23	fveq2d	$$⊢\phi \to \left(1_{𝑜}\mathrm{eval}S\right)\left({\mathrm{var}}_1\left(S\right)\right)=\left(1_{𝑜}\mathrm{eval}S\right)\left(\left(1_{𝑜}\mathrm{mVar}U\right)\left(\varnothing \right)\right)$$
26	18 24 25	3eqtr4d	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left({\mathrm{var}}_1\left(S\right)\right)=\left(1_{𝑜}\mathrm{eval}S\right)\left({\mathrm{var}}_1\left(S\right)\right)$$
27	26	coeq1d	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left({\mathrm{var}}_1\left(S\right)\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)=\left(1_{𝑜}\mathrm{eval}S\right)\left({\mathrm{var}}_1\left(S\right)\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
28		eqid	$$⊢{\mathrm{Poly}}_1\left(U\right)={\mathrm{Poly}}_1\left(U\right)$$
29		eqid	$$⊢{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}R\right)={\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}R\right)$$
30	3	fveq2i	$$⊢{\mathrm{Poly}}_1\left(U\right)={\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}R\right)$$
31	30	fveq2i	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}R\right)}$$
32	29 31	ply1bas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}$$
33	32	eqcomi	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
34	7 6 3 28 33	subrgvr1cl	$$⊢\phi \to {\mathrm{var}}_1\left(S\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}$$
35		eqid	$$⊢1_{𝑜}\mathrm{evalSub}S=1_{𝑜}\mathrm{evalSub}S$$
36		eqid	$$⊢1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)=1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)$$
37		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}$$
38	1 35 4 36 37	evls1val	$$⊢\left(S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\wedge {\mathrm{var}}_1\left(S\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}\right)\to Q\left({\mathrm{var}}_1\left(S\right)\right)=\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left({\mathrm{var}}_1\left(S\right)\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
39	5 6 34 38	syl3anc	$$⊢\phi \to Q\left({\mathrm{var}}_1\left(S\right)\right)=\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left({\mathrm{var}}_1\left(S\right)\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
40		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
41		eqid	$$⊢{\mathrm{Poly}}_1\left(S\right)={\mathrm{Poly}}_1\left(S\right)$$
42		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
43	41 42	ply1bas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
44	43	eqcomi	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
45	7 41 44	vr1cl	$$⊢S\in \mathrm{Ring}\to {\mathrm{var}}_1\left(S\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
46	5 40 45	3syl	$$⊢\phi \to {\mathrm{var}}_1\left(S\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
47		eqid	$$⊢{\mathrm{eval}}_1\left(S\right)={\mathrm{eval}}_1\left(S\right)$$
48		eqid	$$⊢1_{𝑜}\mathrm{mPoly}S=1_{𝑜}\mathrm{mPoly}S$$
49		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
50	47 12 4 48 49	evl1val	$$⊢\left(S\in \mathrm{CRing}\wedge {\mathrm{var}}_1\left(S\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}\right)\to {\mathrm{eval}}_1\left(S\right)\left({\mathrm{var}}_1\left(S\right)\right)=\left(1_{𝑜}\mathrm{eval}S\right)\left({\mathrm{var}}_1\left(S\right)\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
51	5 46 50	syl2anc	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left({\mathrm{var}}_1\left(S\right)\right)=\left(1_{𝑜}\mathrm{eval}S\right)\left({\mathrm{var}}_1\left(S\right)\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
52	27 39 51	3eqtr4d	$$⊢\phi \to Q\left({\mathrm{var}}_1\left(S\right)\right)={\mathrm{eval}}_1\left(S\right)\left({\mathrm{var}}_1\left(S\right)\right)$$
53	47 7 4	evl1var	$$⊢S\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(S\right)\left({\mathrm{var}}_1\left(S\right)\right)={\mathrm{I}\upharpoonright }_B$$
54	5 53	syl	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left({\mathrm{var}}_1\left(S\right)\right)={\mathrm{I}\upharpoonright }_B$$
55	10 52 54	3eqtrd	$$⊢\phi \to Q\left(X\right)={\mathrm{I}\upharpoonright }_B$$