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 
|- G = ( E |`s R )
ressply1evls1.2 
|- O = ( E evalSub1 S )
ressply1evls1.3 
|- Q = ( G evalSub1 S )
ressply1evls1.4 
|- P = ( Poly1 ` K )
ressply1evls1.5 
|- K = ( E |`s S )
ressply1evls1.6 
|- B = ( Base ` P )
ressply1evls1.7 
|- ( ph -> E e. CRing )
ressply1evls1.8 
|- ( ph -> R e. ( SubRing ` E ) )
ressply1evls1.9 
|- ( ph -> S e. ( SubRing ` G ) )
ressply1evls1.10 
|- ( ph -> F e. B )
Assertion ressply1evls1 
|- ( ph -> ( Q ` F ) = ( ( O ` F ) |` R ) )

Proof

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