Theorem evls1sca

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

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

Proof

Step	Hyp	Ref	Expression
1		evls1sca.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1sca.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
3		evls1sca.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		evls1sca.b	$$⊢B={\mathrm{Base}}_S$$
5		evls1sca.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
6		evls1sca.s	$$⊢\phi \to S\in \mathrm{CRing}$$
7		evls1sca.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
8		evls1sca.x	$$⊢\phi \to X\in R$$
9		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
10		eqid	$$⊢\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)=\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)$$
11		eqid	$$⊢1_{𝑜}\mathrm{mPoly}U=1_{𝑜}\mathrm{mPoly}U$$
12		eqid	$$⊢S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)=S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)$$
13	10 11 3 12 4	evlsrhm	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\in \left(\left(1_{𝑜}\mathrm{mPoly}U\right)\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)\right)$$
14	9 6 7 13	mp3an2i	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\in \left(\left(1_{𝑜}\mathrm{mPoly}U\right)\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)\right)$$
15		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}$$
16		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}$$
17	15 16	rhmf	$$⊢\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\in \left(\left(1_{𝑜}\mathrm{mPoly}U\right)\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)\right)\to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right):{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}$$
18	14 17	syl	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right):{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}$$
19		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
20	3	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
21	7 20	syl	$$⊢\phi \to U\in \mathrm{Ring}$$
22	2	ply1ring	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
23	21 22	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
24	2	ply1lmod	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{LMod}$$
25	21 24	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
26		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
27		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
28	5 19 23 25 26 27	asclf	$$⊢\phi \to A:{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟶{\mathrm{Base}}_W$$
29	4	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq B$$
30	7 29	syl	$$⊢\phi \to R\subseteq B$$
31	3 4	ressbas2	$$⊢R\subseteq B\to R={\mathrm{Base}}_U$$
32	30 31	syl	$$⊢\phi \to R={\mathrm{Base}}_U$$
33	2	ply1sca	$$⊢U\in \mathrm{Ring}\to U=\mathrm{Scalar}\left(W\right)$$
34	21 33	syl	$$⊢\phi \to U=\mathrm{Scalar}\left(W\right)$$
35	34	fveq2d	$$⊢\phi \to {\mathrm{Base}}_U={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
36	32 35	eqtrd	$$⊢\phi \to R={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
37	2 27	ply1bas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}$$
38	37	a1i	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}$$
39	38	eqcomd	$$⊢\phi \to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}={\mathrm{Base}}_W$$
40	36 39	feq23d	$$⊢\phi \to \left(A:R⟶{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}\leftrightarrow A:{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟶{\mathrm{Base}}_W\right)$$
41	28 40	mpbird	$$⊢\phi \to A:R⟶{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}$$
42	41 8	ffvelcdmd	$$⊢\phi \to A\left(X\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}$$
43		fvco3	$$⊢\left(\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right):{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}\wedge A\left(X\right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}U\right)}\right)\to \left(\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\right)\left(A\left(X\right)\right)=\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\left(\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(A\left(X\right)\right)\right)$$
44	18 42 43	syl2anc	$$⊢\phi \to \left(\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\right)\left(A\left(X\right)\right)=\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\left(\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(A\left(X\right)\right)\right)$$
45	5	a1i	$$⊢\phi \to A=\mathrm{algSc}\left(W\right)$$
46		eqid	$$⊢\mathrm{algSc}\left(W\right)=\mathrm{algSc}\left(W\right)$$
47	2 46	ply1ascl	$$⊢\mathrm{algSc}\left(W\right)=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}U\right)$$
48	45 47	eqtrdi	$$⊢\phi \to A=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}U\right)$$
49	48	fveq1d	$$⊢\phi \to A\left(X\right)=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}U\right)\left(X\right)$$
50	49	fveq2d	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(A\left(X\right)\right)=\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}U\right)\left(X\right)\right)$$
51		eqid	$$⊢\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}U\right)=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}U\right)$$
52	9	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
53	10 11 3 4 51 52 6 7 8	evlssca	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}U\right)\left(X\right)\right)=\left(B^{1_{𝑜}}\right)\times \left\{X\right\}$$
54	50 53	eqtrd	$$⊢\phi \to \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(A\left(X\right)\right)=\left(B^{1_{𝑜}}\right)\times \left\{X\right\}$$
55	54	fveq2d	$$⊢\phi \to \left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\left(\left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\left(A\left(X\right)\right)\right)=\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)$$
56		eqidd	$$⊢\phi \to \left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)=\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)$$
57		coeq1	$$⊢x=\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\to x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)=\left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
58	57	adantl	$$⊢\left(\phi \wedge x=\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)\to x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)=\left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
59	30 8	sseldd	$$⊢\phi \to X\in B$$
60		fconst6g	$$⊢X\in B\to \left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right):B^{1_{𝑜}}⟶B$$
61	59 60	syl	$$⊢\phi \to \left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right):B^{1_{𝑜}}⟶B$$
62	4	fvexi	$$⊢B\in \mathrm{V}$$
63	62	a1i	$$⊢\phi \to B\in \mathrm{V}$$
64		ovex	$$⊢B^{1_{𝑜}}\in \mathrm{V}$$
65	64	a1i	$$⊢\phi \to B^{1_{𝑜}}\in \mathrm{V}$$
66	63 65	elmapd	$$⊢\phi \to \left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)\leftrightarrow \left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right):B^{1_{𝑜}}⟶B\right)$$
67	61 66	mpbird	$$⊢\phi \to \left(B^{1_{𝑜}}\right)\times \left\{X\right\}\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)$$
68		snex	$$⊢\left\{X\right\}\in \mathrm{V}$$
69	64 68	xpex	$$⊢\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\in \mathrm{V}$$
70	69	a1i	$$⊢\phi \to \left(B^{1_{𝑜}}\right)\times \left\{X\right\}\in \mathrm{V}$$
71	63	mptexd	$$⊢\phi \to \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\in \mathrm{V}$$
72		coexg	$$⊢\left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\in \mathrm{V}\wedge \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\in \mathrm{V}\right)\to \left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\in \mathrm{V}$$
73	70 71 72	syl2anc	$$⊢\phi \to \left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\in \mathrm{V}$$
74	56 58 67 73	fvmptd	$$⊢\phi \to \left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)=\left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
75		fconst6g	$$⊢y\in B\to \left(1_{𝑜}\times \left\{y\right\}\right):1_{𝑜}⟶B$$
76	75	adantl	$$⊢\left(\phi \wedge y\in B\right)\to \left(1_{𝑜}\times \left\{y\right\}\right):1_{𝑜}⟶B$$
77	62 9	pm3.2i	$$⊢\left(B\in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{On}\right)$$
78	77	a1i	$$⊢\left(\phi \wedge y\in B\right)\to \left(B\in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{On}\right)$$
79		elmapg	$$⊢\left(B\in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{On}\right)\to \left(1_{𝑜}\times \left\{y\right\}\in \left(B^{1_{𝑜}}\right)\leftrightarrow \left(1_{𝑜}\times \left\{y\right\}\right):1_{𝑜}⟶B\right)$$
80	78 79	syl	$$⊢\left(\phi \wedge y\in B\right)\to \left(1_{𝑜}\times \left\{y\right\}\in \left(B^{1_{𝑜}}\right)\leftrightarrow \left(1_{𝑜}\times \left\{y\right\}\right):1_{𝑜}⟶B\right)$$
81	76 80	mpbird	$$⊢\left(\phi \wedge y\in B\right)\to 1_{𝑜}\times \left\{y\right\}\in \left(B^{1_{𝑜}}\right)$$
82		eqidd	$$⊢\phi \to \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)=\left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
83		fconstmpt	$$⊢\left(B^{1_{𝑜}}\right)\times \left\{X\right\}=\left(z\in \left(B^{1_{𝑜}}\right)⟼X\right)$$
84	83	a1i	$$⊢\phi \to \left(B^{1_{𝑜}}\right)\times \left\{X\right\}=\left(z\in \left(B^{1_{𝑜}}\right)⟼X\right)$$
85		eqidd	$$⊢z=1_{𝑜}\times \left\{y\right\}\to X=X$$
86	81 82 84 85	fmptco	$$⊢\phi \to \left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)=\left(y\in B⟼X\right)$$
87	74 86	eqtrd	$$⊢\phi \to \left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\left(\left(B^{1_{𝑜}}\right)\times \left\{X\right\}\right)=\left(y\in B⟼X\right)$$
88	44 55 87	3eqtrd	$$⊢\phi \to \left(\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\right)\left(A\left(X\right)\right)=\left(y\in B⟼X\right)$$
89		elpwg	$$⊢R\in \mathrm{SubRing}\left(S\right)\to \left(R\in 𝒫B\leftrightarrow R\subseteq B\right)$$
90	29 89	mpbird	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\in 𝒫B$$
91	7 90	syl	$$⊢\phi \to R\in 𝒫B$$
92		eqid	$$⊢1_{𝑜}\mathrm{evalSub}S=1_{𝑜}\mathrm{evalSub}S$$
93	1 92 4	evls1fval	$$⊢\left(S\in \mathrm{CRing}\wedge R\in 𝒫B\right)\to Q=\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)$$
94	6 91 93	syl2anc	$$⊢\phi \to Q=\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)$$
95	94	fveq1d	$$⊢\phi \to Q\left(A\left(X\right)\right)=\left(\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{evalSub}S\right)\left(R\right)\right)\left(A\left(X\right)\right)$$
96		fconstmpt	$$⊢B\times \left\{X\right\}=\left(y\in B⟼X\right)$$
97	96	a1i	$$⊢\phi \to B\times \left\{X\right\}=\left(y\in B⟼X\right)$$
98	88 95 97	3eqtr4d	$$⊢\phi \to Q\left(A\left(X\right)\right)=B\times \left\{X\right\}$$