This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( ( 𝑂 ‘ 𝐹 ) ↾ 𝑅 ) )