Theorem ressply1evls1

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

	Ref	Expression
Hypotheses	ressply1evls1.1	$$⊢G=E{\upharpoonright }_{𝑠}R$$
	ressply1evls1.2	$$⊢O=E{\mathrm{evalSub}}_{1}S$$
	ressply1evls1.3	$$⊢Q=G{\mathrm{evalSub}}_{1}S$$
	ressply1evls1.4	$$⊢P={\mathrm{Poly}}_1\left(K\right)$$
	ressply1evls1.5	$$⊢K=E{\upharpoonright }_{𝑠}S$$
	ressply1evls1.6	$$⊢B={\mathrm{Base}}_P$$
	ressply1evls1.7	$$⊢\phi \to E\in \mathrm{CRing}$$
	ressply1evls1.8	$$⊢\phi \to R\in \mathrm{SubRing}\left(E\right)$$
	ressply1evls1.9	$$⊢\phi \to S\in \mathrm{SubRing}\left(G\right)$$
	ressply1evls1.10	$$⊢\phi \to F\in B$$
Assertion	ressply1evls1	$$⊢\phi \to Q\left(F\right)={O\left(F\right)\upharpoonright }_R$$

Proof

Step	Hyp	Ref	Expression
1		ressply1evls1.1	$$⊢G=E{\upharpoonright }_{𝑠}R$$
2		ressply1evls1.2	$$⊢O=E{\mathrm{evalSub}}_{1}S$$
3		ressply1evls1.3	$$⊢Q=G{\mathrm{evalSub}}_{1}S$$
4		ressply1evls1.4	$$⊢P={\mathrm{Poly}}_1\left(K\right)$$
5		ressply1evls1.5	$$⊢K=E{\upharpoonright }_{𝑠}S$$
6		ressply1evls1.6	$$⊢B={\mathrm{Base}}_P$$
7		ressply1evls1.7	$$⊢\phi \to E\in \mathrm{CRing}$$
8		ressply1evls1.8	$$⊢\phi \to R\in \mathrm{SubRing}\left(E\right)$$
9		ressply1evls1.9	$$⊢\phi \to S\in \mathrm{SubRing}\left(G\right)$$
10		ressply1evls1.10	$$⊢\phi \to F\in B$$
11		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
12	11	subrgss	$$⊢R\in \mathrm{SubRing}\left(E\right)\to R\subseteq {\mathrm{Base}}_E$$
13	1 11	ressbas2	$$⊢R\subseteq {\mathrm{Base}}_E\to R={\mathrm{Base}}_G$$
14	8 12 13	3syl	$$⊢\phi \to R={\mathrm{Base}}_G$$
15	8 12	syl	$$⊢\phi \to R\subseteq {\mathrm{Base}}_E$$
16	14 15	eqsstrrd	$$⊢\phi \to {\mathrm{Base}}_G\subseteq {\mathrm{Base}}_E$$
17	16	resmptd	$$⊢\phi \to {\left(x\in {\mathrm{Base}}_E⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_E}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)\right)\upharpoonright }_{{\mathrm{Base}}_G}=\left(x\in {\mathrm{Base}}_G⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_E}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)\right)$$
18	1	subsubrg	$$⊢R\in \mathrm{SubRing}\left(E\right)\to \left(S\in \mathrm{SubRing}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubRing}\left(E\right)\wedge S\subseteq R\right)\right)$$
19	18	biimpa	$$⊢\left(R\in \mathrm{SubRing}\left(E\right)\wedge S\in \mathrm{SubRing}\left(G\right)\right)\to \left(S\in \mathrm{SubRing}\left(E\right)\wedge S\subseteq R\right)$$
20	8 9 19	syl2anc	$$⊢\phi \to \left(S\in \mathrm{SubRing}\left(E\right)\wedge S\subseteq R\right)$$
21	20	simpld	$$⊢\phi \to S\in \mathrm{SubRing}\left(E\right)$$
22		eqid	$$⊢{\cdot }_E={\cdot }_E$$
23		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_E}={\cdot }_{{\mathrm{mulGrp}}_E}$$
24		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
25	2 11 4 5 6 7 21 10 22 23 24	evls1fpws	$$⊢\phi \to O\left(F\right)=\left(x\in {\mathrm{Base}}_E⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_E}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)\right)$$
26	25 14	reseq12d	$$⊢\phi \to {O\left(F\right)\upharpoonright }_R={\left(x\in {\mathrm{Base}}_E⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_E}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)\right)\upharpoonright }_{{\mathrm{Base}}_G}$$
27		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
28		eqid	$$⊢{\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)={\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)$$
29		eqid	$$⊢G{\upharpoonright }_{𝑠}S=G{\upharpoonright }_{𝑠}S$$
30		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)}$$
31	1	subrgcrng	$$⊢\left(E\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(E\right)\right)\to G\in \mathrm{CRing}$$
32	7 8 31	syl2anc	$$⊢\phi \to G\in \mathrm{CRing}$$
33	20	simprd	$$⊢\phi \to S\subseteq R$$
34		ressabs	$$⊢\left(R\in \mathrm{SubRing}\left(E\right)\wedge S\subseteq R\right)\to \left(E{\upharpoonright }_{𝑠}R\right){\upharpoonright }_{𝑠}S=E{\upharpoonright }_{𝑠}S$$
35	8 33 34	syl2anc	$$⊢\phi \to \left(E{\upharpoonright }_{𝑠}R\right){\upharpoonright }_{𝑠}S=E{\upharpoonright }_{𝑠}S$$
36	1	oveq1i	$$⊢G{\upharpoonright }_{𝑠}S=\left(E{\upharpoonright }_{𝑠}R\right){\upharpoonright }_{𝑠}S$$
37	35 36 5	3eqtr4g	$$⊢\phi \to G{\upharpoonright }_{𝑠}S=K$$
38	37	fveq2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)={\mathrm{Poly}}_1\left(K\right)$$
39	38 4	eqtr4di	$$⊢\phi \to {\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)=P$$
40	39	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_P$$
41	40 6	eqtr4di	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)}=B$$
42	10 41	eleqtrrd	$$⊢\phi \to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(G{\upharpoonright }_{𝑠}S\right)}$$
43		eqid	$$⊢{\cdot }_G={\cdot }_G$$
44		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_G}={\cdot }_{{\mathrm{mulGrp}}_G}$$
45	3 27 28 29 30 32 9 42 43 44 24	evls1fpws	$$⊢\phi \to Q\left(F\right)=\left(x\in {\mathrm{Base}}_G⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_G}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_G\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)\right)\right)$$
46		eqid	$$⊢{+}_E={+}_E$$
47	7	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to E\in \mathrm{CRing}$$
48		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
49	48	a1i	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
50	15	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to R\subseteq {\mathrm{Base}}_E$$
51	8	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to R\in \mathrm{SubRing}\left(E\right)$$
52	33 15	sstrd	$$⊢\phi \to S\subseteq {\mathrm{Base}}_E$$
53	5 11	ressbas2	$$⊢S\subseteq {\mathrm{Base}}_E\to S={\mathrm{Base}}_K$$
54	52 53	syl	$$⊢\phi \to S={\mathrm{Base}}_K$$
55	54 33	eqsstrrd	$$⊢\phi \to {\mathrm{Base}}_K\subseteq R$$
56	55	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{Base}}_K\subseteq R$$
57	10	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to F\in B$$
58		simpr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to k\in {\mathbb{N}}_0$$
59		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
60	24 6 4 59	coe1fvalcl	$$⊢\left(F\in B\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(k\right)\in {\mathrm{Base}}_K$$
61	57 58 60	syl2anc	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(k\right)\in {\mathrm{Base}}_K$$
62	56 61	sseldd	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(k\right)\in R$$
63		eqid	$$⊢{\mathrm{mulGrp}}_E={\mathrm{mulGrp}}_E$$
64	1 63	mgpress	$$⊢\left(E\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(E\right)\right)\to {\mathrm{mulGrp}}_E{\upharpoonright }_{𝑠}R={\mathrm{mulGrp}}_G$$
65	47 51 64	syl2an2r	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{mulGrp}}_E{\upharpoonright }_{𝑠}R={\mathrm{mulGrp}}_G$$
66	7	crngringd	$$⊢\phi \to E\in \mathrm{Ring}$$
67		eqid	$$⊢1_E=1_E$$
68	67	subrg1cl	$$⊢R\in \mathrm{SubRing}\left(E\right)\to 1_E\in R$$
69	8 68	syl	$$⊢\phi \to 1_E\in R$$
70	1 11 67	ress1r	$$⊢\left(E\in \mathrm{Ring}\wedge 1_E\in R\wedge R\subseteq {\mathrm{Base}}_E\right)\to 1_E=1_G$$
71	66 69 15 70	syl3anc	$$⊢\phi \to 1_E=1_G$$
72	71	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to 1_E=1_G$$
73	63 67	ringidval	$$⊢1_E=0_{{\mathrm{mulGrp}}_E}$$
74		eqid	$$⊢{\mathrm{mulGrp}}_G={\mathrm{mulGrp}}_G$$
75		eqid	$$⊢1_G=1_G$$
76	74 75	ringidval	$$⊢1_G=0_{{\mathrm{mulGrp}}_G}$$
77	72 73 76	3eqtr3g	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to 0_{{\mathrm{mulGrp}}_E}=0_{{\mathrm{mulGrp}}_G}$$
78	63 11	mgpbas	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_{{\mathrm{mulGrp}}_E}$$
79	15 78	sseqtrdi	$$⊢\phi \to R\subseteq {\mathrm{Base}}_{{\mathrm{mulGrp}}_E}$$
80	79	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to R\subseteq {\mathrm{Base}}_{{\mathrm{mulGrp}}_E}$$
81	14	eleq2d	$$⊢\phi \to \left(x\in R\leftrightarrow x\in {\mathrm{Base}}_G\right)$$
82	81	biimpar	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to x\in R$$
83	82	adantr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to x\in R$$
84	65 77 80 58 83	ressmulgnn0d	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to k{\cdot }_{{\mathrm{mulGrp}}_G}x=k{\cdot }_{{\mathrm{mulGrp}}_E}x$$
85	74 27	mgpbas	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_{{\mathrm{mulGrp}}_G}$$
86	1	subrgring	$$⊢R\in \mathrm{SubRing}\left(E\right)\to G\in \mathrm{Ring}$$
87	74	ringmgp	$$⊢G\in \mathrm{Ring}\to {\mathrm{mulGrp}}_G\in \mathrm{Mnd}$$
88	8 86 87	3syl	$$⊢\phi \to {\mathrm{mulGrp}}_G\in \mathrm{Mnd}$$
89	88	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{mulGrp}}_G\in \mathrm{Mnd}$$
90		simplr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to x\in {\mathrm{Base}}_G$$
91	85 44 89 58 90	mulgnn0cld	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to k{\cdot }_{{\mathrm{mulGrp}}_G}x\in {\mathrm{Base}}_G$$
92	84 91	eqeltrrd	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to k{\cdot }_{{\mathrm{mulGrp}}_E}x\in {\mathrm{Base}}_G$$
93	51 12 13	3syl	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to R={\mathrm{Base}}_G$$
94	92 93	eleqtrrd	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to k{\cdot }_{{\mathrm{mulGrp}}_E}x\in R$$
95	22 51 62 94	subrgmcld	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\in R$$
96	95	fmpttd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to \left(k\in {\mathbb{N}}_0⟼{\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right):{\mathbb{N}}_0⟶R$$
97		subrgsubg	$$⊢R\in \mathrm{SubRing}\left(E\right)\to R\in \mathrm{SubGrp}\left(E\right)$$
98		eqid	$$⊢0_E=0_E$$
99	98	subg0cl	$$⊢R\in \mathrm{SubGrp}\left(E\right)\to 0_E\in R$$
100	8 97 99	3syl	$$⊢\phi \to 0_E\in R$$
101	100	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to 0_E\in R$$
102	7	crnggrpd	$$⊢\phi \to E\in \mathrm{Grp}$$
103	102	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge y\in {\mathrm{Base}}_E\right)\to E\in \mathrm{Grp}$$
104		simpr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge y\in {\mathrm{Base}}_E\right)\to y\in {\mathrm{Base}}_E$$
105	11 46 98 103 104	grplidd	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge y\in {\mathrm{Base}}_E\right)\to 0_E{+}_{E}y=y$$
106	11 46 98 103 104	grpridd	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge y\in {\mathrm{Base}}_E\right)\to y{+}_E{0}_E=y$$
107	105 106	jca	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge y\in {\mathrm{Base}}_E\right)\to \left(0_E{+}_{E}y=y\wedge y{+}_E{0}_E=y\right)$$
108	11 46 1 47 49 50 96 101 107	gsumress	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_E}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)=\underset{k\in {\mathbb{N}}_0}{{\sum }_G}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)$$
109	1 22	ressmulr	$$⊢R\in \mathrm{SubRing}\left(E\right)\to {\cdot }_E={\cdot }_G$$
110	8 109	syl	$$⊢\phi \to {\cdot }_E={\cdot }_G$$
111	110	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\cdot }_E={\cdot }_G$$
112	111	oveqd	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)={\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_G\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)$$
113	84	oveq2d	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)={\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)$$
114	112 113	eqtr3d	$$⊢\left(\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_G\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)={\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)$$
115	114	mpteq2dva	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to \left(k\in {\mathbb{N}}_0⟼{\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_G\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)\right)=\left(k\in {\mathbb{N}}_0⟼{\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)$$
116	115	oveq2d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_G}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_G\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)\right)=\underset{k\in {\mathbb{N}}_0}{{\sum }_G}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)$$
117	108 116	eqtr4d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_E}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)=\underset{k\in {\mathbb{N}}_0}{{\sum }_G}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_G\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)\right)$$
118	117	mpteq2dva	$$⊢\phi \to \left(x\in {\mathrm{Base}}_G⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_E}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)\right)=\left(x\in {\mathrm{Base}}_G⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_G}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_G\left(k{\cdot }_{{\mathrm{mulGrp}}_G}x\right)\right)\right)$$
119	45 118	eqtr4d	$$⊢\phi \to Q\left(F\right)=\left(x\in {\mathrm{Base}}_G⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_E}\left({\mathrm{coe}}_1\left(F\right)\left(k\right){\cdot }_E\left(k{\cdot }_{{\mathrm{mulGrp}}_E}x\right)\right)\right)$$
120	17 26 119	3eqtr4rd	$$⊢\phi \to Q\left(F\right)={O\left(F\right)\upharpoonright }_R$$