Theorem evlsca

Description: Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019)

	Ref	Expression
Hypotheses	evlsca.q	$$⊢Q=I\mathrm{eval}S$$
	evlsca.w	$$⊢W=I\mathrm{mPoly}S$$
	evlsca.b	$$⊢B={\mathrm{Base}}_S$$
	evlsca.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	evlsca.i	$$⊢\phi \to I\in V$$
	evlsca.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsca.x	$$⊢\phi \to X\in B$$
Assertion	evlsca	$$⊢\phi \to Q\left(A\left(X\right)\right)=\left(B^I\right)\times \left\{X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		evlsca.q	$$⊢Q=I\mathrm{eval}S$$
2		evlsca.w	$$⊢W=I\mathrm{mPoly}S$$
3		evlsca.b	$$⊢B={\mathrm{Base}}_S$$
4		evlsca.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
5		evlsca.i	$$⊢\phi \to I\in V$$
6		evlsca.s	$$⊢\phi \to S\in \mathrm{CRing}$$
7		evlsca.x	$$⊢\phi \to X\in B$$
8		eqid	$$⊢\left(I\mathrm{evalSub}S\right)\left(B\right)=\left(I\mathrm{evalSub}S\right)\left(B\right)$$
9		eqid	$$⊢I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}B\right)=I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}B\right)$$
10		eqid	$$⊢S{\upharpoonright }_{𝑠}B=S{\upharpoonright }_{𝑠}B$$
11		eqid	$$⊢\mathrm{algSc}\left(I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}B\right)\right)=\mathrm{algSc}\left(I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}B\right)\right)$$
12		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
13	3	subrgid	$$⊢S\in \mathrm{Ring}\to B\in \mathrm{SubRing}\left(S\right)$$
14	6 12 13	3syl	$$⊢\phi \to B\in \mathrm{SubRing}\left(S\right)$$
15	8 1 9 10 2 3 11 4 5 6 14 7	evlsscasrng	$$⊢\phi \to \left(I\mathrm{evalSub}S\right)\left(B\right)\left(\mathrm{algSc}\left(I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}B\right)\right)\left(X\right)\right)=Q\left(A\left(X\right)\right)$$
16	8 9 10 3 11 5 6 14 7	evlssca	$$⊢\phi \to \left(I\mathrm{evalSub}S\right)\left(B\right)\left(\mathrm{algSc}\left(I\mathrm{mPoly}\left(S{\upharpoonright }_{𝑠}B\right)\right)\left(X\right)\right)=\left(B^I\right)\times \left\{X\right\}$$
17	15 16	eqtr3d	$$⊢\phi \to Q\left(A\left(X\right)\right)=\left(B^I\right)\times \left\{X\right\}$$