Theorem evls1varsrng

Description: The evaluation of the variable of univariate polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019)

	Ref	Expression
Hypotheses	evls1varsrng.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	evls1varsrng.o	$$⊢O={\mathrm{eval}}_1\left(S\right)$$
	evls1varsrng.v	$$⊢V={\mathrm{var}}_1\left(U\right)$$
	evls1varsrng.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evls1varsrng.b	$$⊢B={\mathrm{Base}}_S$$
	evls1varsrng.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1varsrng.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
Assertion	evls1varsrng	$$⊢\phi \to Q\left(V\right)=O\left(V\right)$$

Proof

Step	Hyp	Ref	Expression
1		evls1varsrng.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1varsrng.o	$$⊢O={\mathrm{eval}}_1\left(S\right)$$
3		evls1varsrng.v	$$⊢V={\mathrm{var}}_1\left(U\right)$$
4		evls1varsrng.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		evls1varsrng.b	$$⊢B={\mathrm{Base}}_S$$
6		evls1varsrng.s	$$⊢\phi \to S\in \mathrm{CRing}$$
7		evls1varsrng.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
8	1 3 4 5 6 7	evls1var	$$⊢\phi \to Q\left(V\right)={\mathrm{I}\upharpoonright }_B$$
9	2 5	evl1fval1	$$⊢O=S{\mathrm{evalSub}}_{1}B$$
10	9	a1i	$$⊢\phi \to O=S{\mathrm{evalSub}}_{1}B$$
11	10	fveq1d	$$⊢\phi \to O\left(V\right)=\left(S{\mathrm{evalSub}}_{1}B\right)\left(V\right)$$
12	3	a1i	$$⊢\phi \to V={\mathrm{var}}_1\left(U\right)$$
13		eqid	$$⊢{\mathrm{var}}_1\left(S\right)={\mathrm{var}}_1\left(S\right)$$
14	13 7 4	subrgvr1	$$⊢\phi \to {\mathrm{var}}_1\left(S\right)={\mathrm{var}}_1\left(U\right)$$
15	5	ressid	$$⊢S\in \mathrm{CRing}\to S{\upharpoonright }_{𝑠}B=S$$
16	6 15	syl	$$⊢\phi \to S{\upharpoonright }_{𝑠}B=S$$
17	16	eqcomd	$$⊢\phi \to S=S{\upharpoonright }_{𝑠}B$$
18	17	fveq2d	$$⊢\phi \to {\mathrm{var}}_1\left(S\right)={\mathrm{var}}_1\left(S{\upharpoonright }_{𝑠}B\right)$$
19	12 14 18	3eqtr2d	$$⊢\phi \to V={\mathrm{var}}_1\left(S{\upharpoonright }_{𝑠}B\right)$$
20	19	fveq2d	$$⊢\phi \to \left(S{\mathrm{evalSub}}_{1}B\right)\left(V\right)=\left(S{\mathrm{evalSub}}_{1}B\right)\left({\mathrm{var}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)$$
21		eqid	$$⊢S{\mathrm{evalSub}}_{1}B=S{\mathrm{evalSub}}_{1}B$$
22		eqid	$$⊢{\mathrm{var}}_1\left(S{\upharpoonright }_{𝑠}B\right)={\mathrm{var}}_1\left(S{\upharpoonright }_{𝑠}B\right)$$
23		eqid	$$⊢S{\upharpoonright }_{𝑠}B=S{\upharpoonright }_{𝑠}B$$
24		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
25	5	subrgid	$$⊢S\in \mathrm{Ring}\to B\in \mathrm{SubRing}\left(S\right)$$
26	6 24 25	3syl	$$⊢\phi \to B\in \mathrm{SubRing}\left(S\right)$$
27	21 22 23 5 6 26	evls1var	$$⊢\phi \to \left(S{\mathrm{evalSub}}_{1}B\right)\left({\mathrm{var}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)={\mathrm{I}\upharpoonright }_B$$
28	11 20 27	3eqtrrd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_B=O\left(V\right)$$
29	8 28	eqtrd	$$⊢\phi \to Q\left(V\right)=O\left(V\right)$$