Theorem evls1scasrng

Description: The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 13-Sep-2019)

	Ref	Expression
Hypotheses	evls1scasrng.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	evls1scasrng.o	$$⊢O={\mathrm{eval}}_1\left(S\right)$$
	evls1scasrng.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	evls1scasrng.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evls1scasrng.p	$$⊢P={\mathrm{Poly}}_1\left(S\right)$$
	evls1scasrng.b	$$⊢B={\mathrm{Base}}_S$$
	evls1scasrng.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	evls1scasrng.c	$$⊢C=\mathrm{algSc}\left(P\right)$$
	evls1scasrng.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1scasrng.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1scasrng.x	$$⊢\phi \to X\in R$$
Assertion	evls1scasrng	$$⊢\phi \to Q\left(A\left(X\right)\right)=O\left(C\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evls1scasrng.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1scasrng.o	$$⊢O={\mathrm{eval}}_1\left(S\right)$$
3		evls1scasrng.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		evls1scasrng.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		evls1scasrng.p	$$⊢P={\mathrm{Poly}}_1\left(S\right)$$
6		evls1scasrng.b	$$⊢B={\mathrm{Base}}_S$$
7		evls1scasrng.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
8		evls1scasrng.c	$$⊢C=\mathrm{algSc}\left(P\right)$$
9		evls1scasrng.s	$$⊢\phi \to S\in \mathrm{CRing}$$
10		evls1scasrng.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
11		evls1scasrng.x	$$⊢\phi \to X\in R$$
12	6	ressid	$$⊢S\in \mathrm{CRing}\to S{\upharpoonright }_{𝑠}B=S$$
13	12	eqcomd	$$⊢S\in \mathrm{CRing}\to S=S{\upharpoonright }_{𝑠}B$$
14	9 13	syl	$$⊢\phi \to S=S{\upharpoonright }_{𝑠}B$$
15	14	fveq2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(S\right)={\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)$$
16	5 15	syl5eq	$$⊢\phi \to P={\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)$$
17	16	fveq2d	$$⊢\phi \to \mathrm{algSc}\left(P\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)$$
18	8 17	syl5eq	$$⊢\phi \to C=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)$$
19	18	fveq1d	$$⊢\phi \to C\left(X\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)\left(X\right)$$
20	19	fveq2d	$$⊢\phi \to \left(S{\mathrm{evalSub}}_{1}B\right)\left(C\left(X\right)\right)=\left(S{\mathrm{evalSub}}_{1}B\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)\left(X\right)\right)$$
21		eqid	$$⊢S{\mathrm{evalSub}}_{1}B=S{\mathrm{evalSub}}_{1}B$$
22		eqid	$$⊢{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)={\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)$$
23		eqid	$$⊢S{\upharpoonright }_{𝑠}B=S{\upharpoonright }_{𝑠}B$$
24		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)$$
25		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
26	6	subrgid	$$⊢S\in \mathrm{Ring}\to B\in \mathrm{SubRing}\left(S\right)$$
27	9 25 26	3syl	$$⊢\phi \to B\in \mathrm{SubRing}\left(S\right)$$
28	6	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq B$$
29	10 28	syl	$$⊢\phi \to R\subseteq B$$
30	29 11	sseldd	$$⊢\phi \to X\in B$$
31	21 22 23 6 24 9 27 30	evls1sca	$$⊢\phi \to \left(S{\mathrm{evalSub}}_{1}B\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}B\right)\right)\left(X\right)\right)=B\times \left\{X\right\}$$
32	20 31	eqtrd	$$⊢\phi \to \left(S{\mathrm{evalSub}}_{1}B\right)\left(C\left(X\right)\right)=B\times \left\{X\right\}$$
33	2 6	evl1fval1	$$⊢O=S{\mathrm{evalSub}}_{1}B$$
34	33	a1i	$$⊢\phi \to O=S{\mathrm{evalSub}}_{1}B$$
35	34	fveq1d	$$⊢\phi \to O\left(C\left(X\right)\right)=\left(S{\mathrm{evalSub}}_{1}B\right)\left(C\left(X\right)\right)$$
36	1 3 4 6 7 9 10 11	evls1sca	$$⊢\phi \to Q\left(A\left(X\right)\right)=B\times \left\{X\right\}$$
37	32 35 36	3eqtr4rd	$$⊢\phi \to Q\left(A\left(X\right)\right)=O\left(C\left(X\right)\right)$$