Theorem ressply1evl

Description: Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025)

	Ref	Expression
Hypotheses	ressply1evl2.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	ressply1evl2.k	$$⊢K={\mathrm{Base}}_S$$
	ressply1evl2.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	ressply1evl2.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	ressply1evl2.b	$$⊢B={\mathrm{Base}}_W$$
	ressply1evl.e	$$⊢E={\mathrm{eval}}_1\left(S\right)$$
	ressply1evl.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	ressply1evl.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
Assertion	ressply1evl	$$⊢\phi \to Q={E\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		ressply1evl2.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		ressply1evl2.k	$$⊢K={\mathrm{Base}}_S$$
3		ressply1evl2.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		ressply1evl2.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		ressply1evl2.b	$$⊢B={\mathrm{Base}}_W$$
6		ressply1evl.e	$$⊢E={\mathrm{eval}}_1\left(S\right)$$
7		ressply1evl.s	$$⊢\phi \to S\in \mathrm{CRing}$$
8		ressply1evl.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
9	6 2	evl1fval1	$$⊢E=S{\mathrm{evalSub}}_{1}K$$
10		eqid	$$⊢{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}K\right)={\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}K\right)$$
11		eqid	$$⊢S{\upharpoonright }_{𝑠}K=S{\upharpoonright }_{𝑠}K$$
12		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}K\right)}$$
13	7	adantr	$$⊢\left(\phi \wedge m\in B\right)\to S\in \mathrm{CRing}$$
14	7	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
15	2	subrgid	$$⊢S\in \mathrm{Ring}\to K\in \mathrm{SubRing}\left(S\right)$$
16	14 15	syl	$$⊢\phi \to K\in \mathrm{SubRing}\left(S\right)$$
17	16	adantr	$$⊢\left(\phi \wedge m\in B\right)\to K\in \mathrm{SubRing}\left(S\right)$$
18		eqid	$$⊢{\mathrm{Poly}}_1\left(S\right)={\mathrm{Poly}}_1\left(S\right)$$
19		eqid	$$⊢{\mathrm{PwSer}}_1\left(U\right)={\mathrm{PwSer}}_1\left(U\right)$$
20		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}$$
21		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
22	18 4 3 5 8 19 20 21	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
23		inss2	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
24	22 23	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
25	2	ressid	$$⊢S\in \mathrm{CRing}\to S{\upharpoonright }_{𝑠}K=S$$
26	7 25	syl	$$⊢\phi \to S{\upharpoonright }_{𝑠}K=S$$
27	26	fveq2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}K\right)={\mathrm{Poly}}_1\left(S\right)$$
28	27	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
29	24 28	sseqtrrd	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}K\right)}$$
30	29	sselda	$$⊢\left(\phi \wedge m\in B\right)\to m\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S{\upharpoonright }_{𝑠}K\right)}$$
31		eqid	$$⊢{\cdot }_S={\cdot }_S$$
32		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_S}={\cdot }_{{\mathrm{mulGrp}}_S}$$
33		eqid	$$⊢{\mathrm{coe}}_1\left(m\right)={\mathrm{coe}}_1\left(m\right)$$
34	9 2 10 11 12 13 17 30 31 32 33	evls1fpws	$$⊢\left(\phi \wedge m\in B\right)\to E\left(m\right)=\left(x\in K⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_S}\left({\mathrm{coe}}_1\left(m\right)\left(k\right){\cdot }_S\left(k{\cdot }_{{\mathrm{mulGrp}}_S}x\right)\right)\right)$$
35	8	adantr	$$⊢\left(\phi \wedge m\in B\right)\to R\in \mathrm{SubRing}\left(S\right)$$
36		simpr	$$⊢\left(\phi \wedge m\in B\right)\to m\in B$$
37	1 2 3 4 5 13 35 36 31 32 33	evls1fpws	$$⊢\left(\phi \wedge m\in B\right)\to Q\left(m\right)=\left(x\in K⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_S}\left({\mathrm{coe}}_1\left(m\right)\left(k\right){\cdot }_S\left(k{\cdot }_{{\mathrm{mulGrp}}_S}x\right)\right)\right)$$
38	34 37	eqtr4d	$$⊢\left(\phi \wedge m\in B\right)\to E\left(m\right)=Q\left(m\right)$$
39	38	ralrimiva	$$⊢\phi \to \forall m\in BE\left(m\right)=Q\left(m\right)$$
40		eqid	$$⊢S{\uparrow }_{𝑠}K=S{\uparrow }_{𝑠}K$$
41	6 18 40 2	evl1rhm	$$⊢S\in \mathrm{CRing}\to E\in \left({\mathrm{Poly}}_1\left(S\right)\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)$$
42		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
43	21 42	rhmf	$$⊢E\in \left({\mathrm{Poly}}_1\left(S\right)\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)\to E:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
44	7 41 43	3syl	$$⊢\phi \to E:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
45	44	ffnd	$$⊢\phi \to EFn{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
46	1 2 40 4 3	evls1rhm	$$⊢\left(S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)$$
47	7 8 46	syl2anc	$$⊢\phi \to Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)$$
48	5 42	rhmf	$$⊢Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)\to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
49	47 48	syl	$$⊢\phi \to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
50	49	ffnd	$$⊢\phi \to QFnB$$
51		fvreseq1	$$⊢\left(\left(EFn{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}\wedge QFnB\right)\wedge B\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}\right)\to \left({E\upharpoonright }_B=Q\leftrightarrow \forall m\in BE\left(m\right)=Q\left(m\right)\right)$$
52	45 50 24 51	syl21anc	$$⊢\phi \to \left({E\upharpoonright }_B=Q\leftrightarrow \forall m\in BE\left(m\right)=Q\left(m\right)\right)$$
53	39 52	mpbird	$$⊢\phi \to {E\upharpoonright }_B=Q$$
54	53	eqcomd	$$⊢\phi \to Q={E\upharpoonright }_B$$