Metamath Proof Explorer

Theorem evlsmaprhm

Description: The function F mapping polynomials p to their subring evaluation at a given point X is a ring homomorphism. Compare evls1maprhm . (Contributed by SN, 12-Mar-2025)

Ref Expression
Hypotheses evlsmaprhm.q 
|- Q = ( ( I evalSub R ) ` S )
evlsmaprhm.p 
|- P = ( I mPoly U )
evlsmaprhm.u 
|- U = ( R |`s S )
evlsmaprhm.b 
|- B = ( Base ` P )
evlsmaprhm.k 
|- K = ( Base ` R )
evlsmaprhm.f 
|- F = ( p e. B |-> ( ( Q ` p ) ` A ) )
evlsmaprhm.i 
|- ( ph -> I e. V )
evlsmaprhm.r 
|- ( ph -> R e. CRing )
evlsmaprhm.s 
|- ( ph -> S e. ( SubRing ` R ) )
evlsmaprhm.a 
|- ( ph -> A e. ( K ^m I ) )
Assertion evlsmaprhm 
|- ( ph -> F e. ( P RingHom R ) )

Proof

Step Hyp Ref Expression
1 evlsmaprhm.q 
 |-  Q = ( ( I evalSub R ) ` S )
2 evlsmaprhm.p 
 |-  P = ( I mPoly U )
3 evlsmaprhm.u 
 |-  U = ( R |`s S )
4 evlsmaprhm.b 
 |-  B = ( Base ` P )
5 evlsmaprhm.k 
 |-  K = ( Base ` R )
6 evlsmaprhm.f 
 |-  F = ( p e. B |-> ( ( Q ` p ) ` A ) )
7 evlsmaprhm.i 
 |-  ( ph -> I e. V )
8 evlsmaprhm.r 
 |-  ( ph -> R e. CRing )
9 evlsmaprhm.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
10 evlsmaprhm.a 
 |-  ( ph -> A e. ( K ^m I ) )
11 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
12 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
13 eqid 
 |-  ( .r ` P ) = ( .r ` P )
14 eqid 
 |-  ( .r ` R ) = ( .r ` R )
15 3 subrgring 
 |-  ( S e. ( SubRing ` R ) -> U e. Ring )
16 9 15 syl 
 |-  ( ph -> U e. Ring )
17 2 7 16 mplringd 
 |-  ( ph -> P e. Ring )
18 8 crngringd 
 |-  ( ph -> R e. Ring )
19 fveq2 
 |-  ( p = ( 1r ` P ) -> ( Q ` p ) = ( Q ` ( 1r ` P ) ) )
20 19 fveq1d 
 |-  ( p = ( 1r ` P ) -> ( ( Q ` p ) ` A ) = ( ( Q ` ( 1r ` P ) ) ` A ) )
21 4 11 ringidcl 
 |-  ( P e. Ring -> ( 1r ` P ) e. B )
22 17 21 syl 
 |-  ( ph -> ( 1r ` P ) e. B )
23 fvexd 
 |-  ( ph -> ( ( Q ` ( 1r ` P ) ) ` A ) e. _V )
24 6 20 22 23 fvmptd3 
 |-  ( ph -> ( F ` ( 1r ` P ) ) = ( ( Q ` ( 1r ` P ) ) ` A ) )
25 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
26 eqid 
 |-  ( 1r ` U ) = ( 1r ` U )
27 2 25 26 11 7 16 mplascl1 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` U ) ) = ( 1r ` P ) )
28 27 eqcomd 
 |-  ( ph -> ( 1r ` P ) = ( ( algSc ` P ) ` ( 1r ` U ) ) )
29 28 fveq2d 
 |-  ( ph -> ( Q ` ( 1r ` P ) ) = ( Q ` ( ( algSc ` P ) ` ( 1r ` U ) ) ) )
30 29 fveq1d 
 |-  ( ph -> ( ( Q ` ( 1r ` P ) ) ` A ) = ( ( Q ` ( ( algSc ` P ) ` ( 1r ` U ) ) ) ` A ) )
31 3 12 subrg1 
 |-  ( S e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` U ) )
32 9 31 syl 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` U ) )
33 12 subrg1cl 
 |-  ( S e. ( SubRing ` R ) -> ( 1r ` R ) e. S )
34 9 33 syl 
 |-  ( ph -> ( 1r ` R ) e. S )
35 32 34 eqeltrrd 
 |-  ( ph -> ( 1r ` U ) e. S )
36 1 2 3 5 4 25 7 8 9 35 10 evlsscaval 
 |-  ( ph -> ( ( ( algSc ` P ) ` ( 1r ` U ) ) e. B /\ ( ( Q ` ( ( algSc ` P ) ` ( 1r ` U ) ) ) ` A ) = ( 1r ` U ) ) )
37 36 simprd 
 |-  ( ph -> ( ( Q ` ( ( algSc ` P ) ` ( 1r ` U ) ) ) ` A ) = ( 1r ` U ) )
38 37 32 eqtr4d 
 |-  ( ph -> ( ( Q ` ( ( algSc ` P ) ` ( 1r ` U ) ) ) ` A ) = ( 1r ` R ) )
39 24 30 38 3eqtrd 
 |-  ( ph -> ( F ` ( 1r ` P ) ) = ( 1r ` R ) )
40 7 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> I e. V )
41 8 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> R e. CRing )
42 9 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> S e. ( SubRing ` R ) )
43 10 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> A e. ( K ^m I ) )
44 simprl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> q e. B )
45 eqidd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( Q ` q ) ` A ) = ( ( Q ` q ) ` A ) )
46 44 45 jca 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( q e. B /\ ( ( Q ` q ) ` A ) = ( ( Q ` q ) ` A ) ) )
47 simprr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> r e. B )
48 eqidd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( Q ` r ) ` A ) = ( ( Q ` r ) ` A ) )
49 47 48 jca 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( r e. B /\ ( ( Q ` r ) ` A ) = ( ( Q ` r ) ` A ) ) )
50 1 2 3 5 4 40 41 42 43 46 49 13 14 evlsmulval 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( q ( .r ` P ) r ) e. B /\ ( ( Q ` ( q ( .r ` P ) r ) ) ` A ) = ( ( ( Q ` q ) ` A ) ( .r ` R ) ( ( Q ` r ) ` A ) ) ) )
51 50 simprd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( Q ` ( q ( .r ` P ) r ) ) ` A ) = ( ( ( Q ` q ) ` A ) ( .r ` R ) ( ( Q ` r ) ` A ) ) )
52 fveq2 
 |-  ( p = ( q ( .r ` P ) r ) -> ( Q ` p ) = ( Q ` ( q ( .r ` P ) r ) ) )
53 52 fveq1d 
 |-  ( p = ( q ( .r ` P ) r ) -> ( ( Q ` p ) ` A ) = ( ( Q ` ( q ( .r ` P ) r ) ) ` A ) )
54 17 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> P e. Ring )
55 4 13 54 44 47 ringcld 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( q ( .r ` P ) r ) e. B )
56 fvexd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( Q ` ( q ( .r ` P ) r ) ) ` A ) e. _V )
57 6 53 55 56 fvmptd3 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( F ` ( q ( .r ` P ) r ) ) = ( ( Q ` ( q ( .r ` P ) r ) ) ` A ) )
58 fveq2 
 |-  ( p = q -> ( Q ` p ) = ( Q ` q ) )
59 58 fveq1d 
 |-  ( p = q -> ( ( Q ` p ) ` A ) = ( ( Q ` q ) ` A ) )
60 fvexd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( Q ` q ) ` A ) e. _V )
61 6 59 44 60 fvmptd3 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( F ` q ) = ( ( Q ` q ) ` A ) )
62 fveq2 
 |-  ( p = r -> ( Q ` p ) = ( Q ` r ) )
63 62 fveq1d 
 |-  ( p = r -> ( ( Q ` p ) ` A ) = ( ( Q ` r ) ` A ) )
64 fvexd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( Q ` r ) ` A ) e. _V )
65 6 63 47 64 fvmptd3 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( F ` r ) = ( ( Q ` r ) ` A ) )
66 61 65 oveq12d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( F ` q ) ( .r ` R ) ( F ` r ) ) = ( ( ( Q ` q ) ` A ) ( .r ` R ) ( ( Q ` r ) ` A ) ) )
67 51 57 66 3eqtr4d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( F ` ( q ( .r ` P ) r ) ) = ( ( F ` q ) ( .r ` R ) ( F ` r ) ) )
68 eqid 
 |-  ( +g ` P ) = ( +g ` P )
69 eqid 
 |-  ( +g ` R ) = ( +g ` R )
70 7 adantr 
 |-  ( ( ph /\ p e. B ) -> I e. V )
71 8 adantr 
 |-  ( ( ph /\ p e. B ) -> R e. CRing )
72 9 adantr 
 |-  ( ( ph /\ p e. B ) -> S e. ( SubRing ` R ) )
73 simpr 
 |-  ( ( ph /\ p e. B ) -> p e. B )
74 10 adantr 
 |-  ( ( ph /\ p e. B ) -> A e. ( K ^m I ) )
75 1 2 3 4 5 70 71 72 73 74 evlscl 
 |-  ( ( ph /\ p e. B ) -> ( ( Q ` p ) ` A ) e. K )
76 75 6 fmptd 
 |-  ( ph -> F : B --> K )
77 1 2 3 5 4 40 41 42 43 46 49 68 69 evlsaddval 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( q ( +g ` P ) r ) e. B /\ ( ( Q ` ( q ( +g ` P ) r ) ) ` A ) = ( ( ( Q ` q ) ` A ) ( +g ` R ) ( ( Q ` r ) ` A ) ) ) )
78 77 simprd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( Q ` ( q ( +g ` P ) r ) ) ` A ) = ( ( ( Q ` q ) ` A ) ( +g ` R ) ( ( Q ` r ) ` A ) ) )
79 fveq2 
 |-  ( p = ( q ( +g ` P ) r ) -> ( Q ` p ) = ( Q ` ( q ( +g ` P ) r ) ) )
80 79 fveq1d 
 |-  ( p = ( q ( +g ` P ) r ) -> ( ( Q ` p ) ` A ) = ( ( Q ` ( q ( +g ` P ) r ) ) ` A ) )
81 17 ringgrpd 
 |-  ( ph -> P e. Grp )
82 81 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> P e. Grp )
83 4 68 82 44 47 grpcld 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( q ( +g ` P ) r ) e. B )
84 fvexd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( Q ` ( q ( +g ` P ) r ) ) ` A ) e. _V )
85 6 80 83 84 fvmptd3 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( F ` ( q ( +g ` P ) r ) ) = ( ( Q ` ( q ( +g ` P ) r ) ) ` A ) )
86 61 65 oveq12d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( F ` q ) ( +g ` R ) ( F ` r ) ) = ( ( ( Q ` q ) ` A ) ( +g ` R ) ( ( Q ` r ) ` A ) ) )
87 78 85 86 3eqtr4d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( F ` ( q ( +g ` P ) r ) ) = ( ( F ` q ) ( +g ` R ) ( F ` r ) ) )
88 4 11 12 13 14 17 18 39 67 5 68 69 76 87 isrhmd 
 |-  ( ph -> F e. ( P RingHom R ) )