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	⊢ 𝐺 = ( 𝐸 ↾s 𝑅 )
	ressply1evls1.2	⊢ 𝑂 = ( 𝐸 evalSub1 𝑆 )
	ressply1evls1.3	⊢ 𝑄 = ( 𝐺 evalSub1 𝑆 )
	ressply1evls1.4	⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
	ressply1evls1.5	⊢ 𝐾 = ( 𝐸 ↾s 𝑆 )
	ressply1evls1.6	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ressply1evls1.7	⊢ ( 𝜑 → 𝐸 ∈ CRing )
	ressply1evls1.8	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝐸 ) )
	ressply1evls1.9	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝐺 ) )
	ressply1evls1.10	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	ressply1evls1	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( ( 𝑂 ‘ 𝐹 ) ↾ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ressply1evls1.1	⊢ 𝐺 = ( 𝐸 ↾s 𝑅 )
2		ressply1evls1.2	⊢ 𝑂 = ( 𝐸 evalSub1 𝑆 )
3		ressply1evls1.3	⊢ 𝑄 = ( 𝐺 evalSub1 𝑆 )
4		ressply1evls1.4	⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
5		ressply1evls1.5	⊢ 𝐾 = ( 𝐸 ↾s 𝑆 )
6		ressply1evls1.6	⊢ 𝐵 = ( Base ‘ 𝑃 )
7		ressply1evls1.7	⊢ ( 𝜑 → 𝐸 ∈ CRing )
8		ressply1evls1.8	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝐸 ) )
9		ressply1evls1.9	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝐺 ) )
10		ressply1evls1.10	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
11		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
12	11	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝐸 ) → 𝑅 ⊆ ( Base ‘ 𝐸 ) )
13	1 11	ressbas2	⊢ ( 𝑅 ⊆ ( Base ‘ 𝐸 ) → 𝑅 = ( Base ‘ 𝐺 ) )
14	8 12 13	3syl	⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝐺 ) )
15	8 12	syl	⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ 𝐸 ) )
16	14 15	eqsstrrd	⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝐸 ) )
17	16	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐸 ) ↦ ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) ) ↾ ( Base ‘ 𝐺 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) ) )
18	1	subsubrg	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝐸 ) → ( 𝑆 ∈ ( SubRing ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑆 ⊆ 𝑅 ) ) )
19	18	biimpa	⊢ ( ( 𝑅 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑆 ∈ ( SubRing ‘ 𝐺 ) ) → ( 𝑆 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑆 ⊆ 𝑅 ) )
20	8 9 19	syl2anc	⊢ ( 𝜑 → ( 𝑆 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑆 ⊆ 𝑅 ) )
21	20	simpld	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝐸 ) )
22		eqid	⊢ ( .r ‘ 𝐸 ) = ( .r ‘ 𝐸 )
23		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝐸 ) ) = ( .g ‘ ( mulGrp ‘ 𝐸 ) )
24		eqid	⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
25	2 11 4 5 6 7 21 10 22 23 24	evls1fpws	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐸 ) ↦ ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) ) )
26	25 14	reseq12d	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐹 ) ↾ 𝑅 ) = ( ( 𝑥 ∈ ( Base ‘ 𝐸 ) ↦ ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) ) ↾ ( Base ‘ 𝐺 ) ) )
27		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
28		eqid	⊢ ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) )
29		eqid	⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 )
30		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) ) ) = ( Base ‘ ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) ) )
31	1	subrgcrng	⊢ ( ( 𝐸 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐺 ∈ CRing )
32	7 8 31	syl2anc	⊢ ( 𝜑 → 𝐺 ∈ CRing )
33	20	simprd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑅 )
34		ressabs	⊢ ( ( 𝑅 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑆 ⊆ 𝑅 ) → ( ( 𝐸 ↾s 𝑅 ) ↾s 𝑆 ) = ( 𝐸 ↾s 𝑆 ) )
35	8 33 34	syl2anc	⊢ ( 𝜑 → ( ( 𝐸 ↾s 𝑅 ) ↾s 𝑆 ) = ( 𝐸 ↾s 𝑆 ) )
36	1	oveq1i	⊢ ( 𝐺 ↾s 𝑆 ) = ( ( 𝐸 ↾s 𝑅 ) ↾s 𝑆 )
37	35 36 5	3eqtr4g	⊢ ( 𝜑 → ( 𝐺 ↾s 𝑆 ) = 𝐾 )
38	37	fveq2d	⊢ ( 𝜑 → ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Poly1 ‘ 𝐾 ) )
39	38 4	eqtr4di	⊢ ( 𝜑 → ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) ) = 𝑃 )
40	39	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) ) ) = ( Base ‘ 𝑃 ) )
41	40 6	eqtr4di	⊢ ( 𝜑 → ( Base ‘ ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) ) ) = 𝐵 )
42	10 41	eleqtrrd	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ ( 𝐺 ↾s 𝑆 ) ) ) )
43		eqid	⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝐺 )
44		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝐺 ) ) = ( .g ‘ ( mulGrp ‘ 𝐺 ) )
45	3 27 28 29 30 32 9 42 43 44 24	evls1fpws	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐺 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) ) ) ) )
46		eqid	⊢ ( +g ‘ 𝐸 ) = ( +g ‘ 𝐸 )
47	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝐸 ∈ CRing )
48		nn0ex	⊢ ℕ0 ∈ V
49	48	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ℕ0 ∈ V )
50	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑅 ⊆ ( Base ‘ 𝐸 ) )
51	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ ( SubRing ‘ 𝐸 ) )
52	33 15	sstrd	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐸 ) )
53	5 11	ressbas2	⊢ ( 𝑆 ⊆ ( Base ‘ 𝐸 ) → 𝑆 = ( Base ‘ 𝐾 ) )
54	52 53	syl	⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐾 ) )
55	54 33	eqsstrrd	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) ⊆ 𝑅 )
56	55	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( Base ‘ 𝐾 ) ⊆ 𝑅 )
57	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐹 ∈ 𝐵 )
58		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
59		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
60	24 6 4 59	coe1fvalcl	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐾 ) )
61	57 58 60	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐾 ) )
62	56 61	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑅 )
63		eqid	⊢ ( mulGrp ‘ 𝐸 ) = ( mulGrp ‘ 𝐸 )
64	1 63	mgpress	⊢ ( ( 𝐸 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝐸 ) ) → ( ( mulGrp ‘ 𝐸 ) ↾s 𝑅 ) = ( mulGrp ‘ 𝐺 ) )
65	47 51 64	syl2an2r	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( mulGrp ‘ 𝐸 ) ↾s 𝑅 ) = ( mulGrp ‘ 𝐺 ) )
66	7	crngringd	⊢ ( 𝜑 → 𝐸 ∈ Ring )
67		eqid	⊢ ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐸 )
68	67	subrg1cl	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝐸 ) → ( 1r ‘ 𝐸 ) ∈ 𝑅 )
69	8 68	syl	⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) ∈ 𝑅 )
70	1 11 67	ress1r	⊢ ( ( 𝐸 ∈ Ring ∧ ( 1r ‘ 𝐸 ) ∈ 𝑅 ∧ 𝑅 ⊆ ( Base ‘ 𝐸 ) ) → ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐺 ) )
71	66 69 15 70	syl3anc	⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐺 ) )
72	71	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐺 ) )
73	63 67	ringidval	⊢ ( 1r ‘ 𝐸 ) = ( 0g ‘ ( mulGrp ‘ 𝐸 ) )
74		eqid	⊢ ( mulGrp ‘ 𝐺 ) = ( mulGrp ‘ 𝐺 )
75		eqid	⊢ ( 1r ‘ 𝐺 ) = ( 1r ‘ 𝐺 )
76	74 75	ringidval	⊢ ( 1r ‘ 𝐺 ) = ( 0g ‘ ( mulGrp ‘ 𝐺 ) )
77	72 73 76	3eqtr3g	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 0g ‘ ( mulGrp ‘ 𝐸 ) ) = ( 0g ‘ ( mulGrp ‘ 𝐺 ) ) )
78	63 11	mgpbas	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ ( mulGrp ‘ 𝐸 ) )
79	15 78	sseqtrdi	⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ ( mulGrp ‘ 𝐸 ) ) )
80	79	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ⊆ ( Base ‘ ( mulGrp ‘ 𝐸 ) ) )
81	14	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 ↔ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
82	81	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ 𝑅 )
83	82	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑥 ∈ 𝑅 )
84	65 77 80 58 83	ressmulgnn0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) )
85	74 27	mgpbas	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ ( mulGrp ‘ 𝐺 ) )
86	1	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝐸 ) → 𝐺 ∈ Ring )
87	74	ringmgp	⊢ ( 𝐺 ∈ Ring → ( mulGrp ‘ 𝐺 ) ∈ Mnd )
88	8 86 87	3syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝐺 ) ∈ Mnd )
89	88	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝐺 ) ∈ Mnd )
90		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
91	85 44 89 58 90	mulgnn0cld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
92	84 91	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
93	51 12 13	3syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 = ( Base ‘ 𝐺 ) )
94	92 93	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ∈ 𝑅 )
95	22 51 62 94	subrgmcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ∈ 𝑅 )
96	95	fmpttd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) : ℕ0 ⟶ 𝑅 )
97		subrgsubg	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝐸 ) → 𝑅 ∈ ( SubGrp ‘ 𝐸 ) )
98		eqid	⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
99	98	subg0cl	⊢ ( 𝑅 ∈ ( SubGrp ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) ∈ 𝑅 )
100	8 97 99	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ 𝑅 )
101	100	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 0g ‘ 𝐸 ) ∈ 𝑅 )
102	7	crnggrpd	⊢ ( 𝜑 → 𝐸 ∈ Grp )
103	102	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) → 𝐸 ∈ Grp )
104		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) → 𝑦 ∈ ( Base ‘ 𝐸 ) )
105	11 46 98 103 104	grplidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) → ( ( 0g ‘ 𝐸 ) ( +g ‘ 𝐸 ) 𝑦 ) = 𝑦 )
106	11 46 98 103 104	grpridd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑦 ( +g ‘ 𝐸 ) ( 0g ‘ 𝐸 ) ) = 𝑦 )
107	105 106	jca	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) → ( ( ( 0g ‘ 𝐸 ) ( +g ‘ 𝐸 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐸 ) ( 0g ‘ 𝐸 ) ) = 𝑦 ) )
108	11 46 1 47 49 50 96 101 107	gsumress	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) )
109	1 22	ressmulr	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝐸 ) → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐺 ) )
110	8 109	syl	⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐺 ) )
111	110	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐺 ) )
112	111	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐺 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) )
113	84	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) )
114	112 113	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐺 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) )
115	114	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐺 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) )
116	115	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐺 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) )
117	108 116	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐺 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) ) ) )
118	117	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐺 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐺 ) ) 𝑥 ) ) ) ) ) )
119	45 118	eqtr4d	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) ) )
120	17 26 119	3eqtr4rd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( ( 𝑂 ‘ 𝐹 ) ↾ 𝑅 ) )