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	8 2	syl6reqr	$$⊢\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	syl5eq	$$⊢\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		eqid	$$⊢{\mathrm{PwSer}}_1\left(S{\upharpoonright }_{𝑠}R\right)={\mathrm{PwSer}}_1\left(S{\upharpoonright }_{𝑠}R\right)$$
31	3	fveq2i	$$⊢{\mathrm{Poly}}_1\left(U\right)={\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}R\right)$$
32	31	fveq2i	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}R\right)}$$
33	29 30 32	ply1bas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}$$
34	33	eqcomi	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
35	7 6 3 28 34	subrgvr1cl	$$⊢\phi \to {\mathrm{var}}_1\left(S\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)\right)}$$
36		eqid	$$⊢1_{𝑜}\mathrm{evalSub}S=1_{𝑜}\mathrm{evalSub}S$$
37		eqid	$$⊢1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)=1_{𝑜}\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}R\right)$$
38		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)}$$
39	1 36 4 37 38	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)$$
40	5 6 35 39	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)$$
41		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
42		eqid	$$⊢{\mathrm{Poly}}_1\left(S\right)={\mathrm{Poly}}_1\left(S\right)$$
43		eqid	$$⊢{\mathrm{PwSer}}_1\left(S\right)={\mathrm{PwSer}}_1\left(S\right)$$
44		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
45	42 43 44	ply1bas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
46	45	eqcomi	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
47	7 42 46	vr1cl	$$⊢S\in \mathrm{Ring}\to {\mathrm{var}}_1\left(S\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
48	5 41 47	3syl	$$⊢\phi \to {\mathrm{var}}_1\left(S\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
49		eqid	$$⊢{\mathrm{eval}}_1\left(S\right)={\mathrm{eval}}_1\left(S\right)$$
50		eqid	$$⊢1_{𝑜}\mathrm{mPoly}S=1_{𝑜}\mathrm{mPoly}S$$
51		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
52	49 12 4 50 51	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)$$
53	5 48 52	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)$$
54	27 40 53	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)$$
55	49 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$$
56	5 55	syl	$$⊢\phi \to {\mathrm{eval}}_1\left(S\right)\left({\mathrm{var}}_1\left(S\right)\right)={\mathrm{I}\upharpoonright }_B$$
57	10 54 56	3eqtrd	$$⊢\phi \to Q\left(X\right)={\mathrm{I}\upharpoonright }_B$$