Metamath Proof Explorer

Theorem evls1maprhm

Description: The function F mapping polynomials p to their subring evaluation at a given point X is a ring homomorphism. (Contributed by Thierry Arnoux, 8-Feb-2025)

Ref Expression
Hypotheses evls1maprhm.q 
|- O = ( R evalSub1 S )
evls1maprhm.p 
|- P = ( Poly1 ` ( R |`s S ) )
evls1maprhm.b 
|- B = ( Base ` R )
evls1maprhm.u 
|- U = ( Base ` P )
evls1maprhm.r 
|- ( ph -> R e. CRing )
evls1maprhm.s 
|- ( ph -> S e. ( SubRing ` R ) )
evls1maprhm.y 
|- ( ph -> X e. B )
evls1maprhm.f 
|- F = ( p e. U |-> ( ( O ` p ) ` X ) )
Assertion evls1maprhm 
|- ( ph -> F e. ( P RingHom R ) )

Proof

Step Hyp Ref Expression
1 evls1maprhm.q 
 |-  O = ( R evalSub1 S )
2 evls1maprhm.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
3 evls1maprhm.b 
 |-  B = ( Base ` R )
4 evls1maprhm.u 
 |-  U = ( Base ` P )
5 evls1maprhm.r 
 |-  ( ph -> R e. CRing )
6 evls1maprhm.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
7 evls1maprhm.y 
 |-  ( ph -> X e. B )
8 evls1maprhm.f 
 |-  F = ( p e. U |-> ( ( O ` p ) ` X ) )
9 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
10 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
11 eqid 
 |-  ( .r ` P ) = ( .r ` P )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 eqid 
 |-  ( R |`s S ) = ( R |`s S )
14 13 subrgcrng 
 |-  ( ( R e. CRing /\ S e. ( SubRing ` R ) ) -> ( R |`s S ) e. CRing )
15 5 6 14 syl2anc 
 |-  ( ph -> ( R |`s S ) e. CRing )
16 2 ply1crng 
 |-  ( ( R |`s S ) e. CRing -> P e. CRing )
17 15 16 syl 
 |-  ( ph -> P e. CRing )
18 17 crngringd 
 |-  ( ph -> P e. Ring )
19 5 crngringd 
 |-  ( ph -> R e. Ring )
20 fveq2 
 |-  ( p = ( 1r ` P ) -> ( O ` p ) = ( O ` ( 1r ` P ) ) )
21 20 fveq1d 
 |-  ( p = ( 1r ` P ) -> ( ( O ` p ) ` X ) = ( ( O ` ( 1r ` P ) ) ` X ) )
22 4 9 ringidcl 
 |-  ( P e. Ring -> ( 1r ` P ) e. U )
23 18 22 syl 
 |-  ( ph -> ( 1r ` P ) e. U )
24 fvexd 
 |-  ( ph -> ( ( O ` ( 1r ` P ) ) ` X ) e. _V )
25 8 21 23 24 fvmptd3 
 |-  ( ph -> ( F ` ( 1r ` P ) ) = ( ( O ` ( 1r ` P ) ) ` X ) )
26 13 10 subrg1 
 |-  ( S e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` ( R |`s S ) ) )
27 6 26 syl 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( R |`s S ) ) )
28 27 fveq2d 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( algSc ` P ) ` ( 1r ` ( R |`s S ) ) ) )
29 15 crngringd 
 |-  ( ph -> ( R |`s S ) e. Ring )
30 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
31 eqid 
 |-  ( 1r ` ( R |`s S ) ) = ( 1r ` ( R |`s S ) )
32 2 30 31 9 ply1scl1 
 |-  ( ( R |`s S ) e. Ring -> ( ( algSc ` P ) ` ( 1r ` ( R |`s S ) ) ) = ( 1r ` P ) )
33 29 32 syl 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` ( R |`s S ) ) ) = ( 1r ` P ) )
34 28 33 eqtr2d 
 |-  ( ph -> ( 1r ` P ) = ( ( algSc ` P ) ` ( 1r ` R ) ) )
35 34 fveq2d 
 |-  ( ph -> ( O ` ( 1r ` P ) ) = ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) )
36 35 fveq1d 
 |-  ( ph -> ( ( O ` ( 1r ` P ) ) ` X ) = ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` X ) )
37 10 subrg1cl 
 |-  ( S e. ( SubRing ` R ) -> ( 1r ` R ) e. S )
38 6 37 syl 
 |-  ( ph -> ( 1r ` R ) e. S )
39 1 2 13 3 30 5 6 38 7 evls1scafv 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` X ) = ( 1r ` R ) )
40 25 36 39 3eqtrd 
 |-  ( ph -> ( F ` ( 1r ` P ) ) = ( 1r ` R ) )
41 5 adantr 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> R e. CRing )
42 6 adantr 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> S e. ( SubRing ` R ) )
43 simprl 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> q e. U )
44 simprr 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> r e. U )
45 7 adantr 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> X e. B )
46 1 3 2 13 4 11 12 41 42 43 44 45 evls1muld 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( ( O ` ( q ( .r ` P ) r ) ) ` X ) = ( ( ( O ` q ) ` X ) ( .r ` R ) ( ( O ` r ) ` X ) ) )
47 fveq2 
 |-  ( p = ( q ( .r ` P ) r ) -> ( O ` p ) = ( O ` ( q ( .r ` P ) r ) ) )
48 47 fveq1d 
 |-  ( p = ( q ( .r ` P ) r ) -> ( ( O ` p ) ` X ) = ( ( O ` ( q ( .r ` P ) r ) ) ` X ) )
49 18 adantr 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> P e. Ring )
50 4 11 49 43 44 ringcld 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( q ( .r ` P ) r ) e. U )
51 fvexd 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( ( O ` ( q ( .r ` P ) r ) ) ` X ) e. _V )
52 8 48 50 51 fvmptd3 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( F ` ( q ( .r ` P ) r ) ) = ( ( O ` ( q ( .r ` P ) r ) ) ` X ) )
53 fveq2 
 |-  ( p = q -> ( O ` p ) = ( O ` q ) )
54 53 fveq1d 
 |-  ( p = q -> ( ( O ` p ) ` X ) = ( ( O ` q ) ` X ) )
55 fvexd 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( ( O ` q ) ` X ) e. _V )
56 8 54 43 55 fvmptd3 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( F ` q ) = ( ( O ` q ) ` X ) )
57 fveq2 
 |-  ( p = r -> ( O ` p ) = ( O ` r ) )
58 57 fveq1d 
 |-  ( p = r -> ( ( O ` p ) ` X ) = ( ( O ` r ) ` X ) )
59 fvexd 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( ( O ` r ) ` X ) e. _V )
60 8 58 44 59 fvmptd3 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( F ` r ) = ( ( O ` r ) ` X ) )
61 56 60 oveq12d 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( ( F ` q ) ( .r ` R ) ( F ` r ) ) = ( ( ( O ` q ) ` X ) ( .r ` R ) ( ( O ` r ) ` X ) ) )
62 46 52 61 3eqtr4d 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( F ` ( q ( .r ` P ) r ) ) = ( ( F ` q ) ( .r ` R ) ( F ` r ) ) )
63 eqid 
 |-  ( +g ` P ) = ( +g ` P )
64 eqid 
 |-  ( +g ` R ) = ( +g ` R )
65 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
66 1 3 2 13 4 65 5 6 ressply1evl 
 |-  ( ph -> O = ( ( eval1 ` R ) |` U ) )
67 66 adantr 
 |-  ( ( ph /\ p e. U ) -> O = ( ( eval1 ` R ) |` U ) )
68 67 fveq1d 
 |-  ( ( ph /\ p e. U ) -> ( O ` p ) = ( ( ( eval1 ` R ) |` U ) ` p ) )
69 simpr 
 |-  ( ( ph /\ p e. U ) -> p e. U )
70 69 fvresd 
 |-  ( ( ph /\ p e. U ) -> ( ( ( eval1 ` R ) |` U ) ` p ) = ( ( eval1 ` R ) ` p ) )
71 68 70 eqtrd 
 |-  ( ( ph /\ p e. U ) -> ( O ` p ) = ( ( eval1 ` R ) ` p ) )
72 71 fveq1d 
 |-  ( ( ph /\ p e. U ) -> ( ( O ` p ) ` X ) = ( ( ( eval1 ` R ) ` p ) ` X ) )
73 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
74 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
75 5 adantr 
 |-  ( ( ph /\ p e. U ) -> R e. CRing )
76 7 adantr 
 |-  ( ( ph /\ p e. U ) -> X e. B )
77 eqid 
 |-  ( PwSer1 ` ( R |`s S ) ) = ( PwSer1 ` ( R |`s S ) )
78 eqid 
 |-  ( Base ` ( PwSer1 ` ( R |`s S ) ) ) = ( Base ` ( PwSer1 ` ( R |`s S ) ) )
79 73 13 2 4 6 77 78 74 ressply1bas2 
 |-  ( ph -> U = ( ( Base ` ( PwSer1 ` ( R |`s S ) ) ) i^i ( Base ` ( Poly1 ` R ) ) ) )
80 inss2 
 |-  ( ( Base ` ( PwSer1 ` ( R |`s S ) ) ) i^i ( Base ` ( Poly1 ` R ) ) ) C_ ( Base ` ( Poly1 ` R ) )
81 79 80 eqsstrdi 
 |-  ( ph -> U C_ ( Base ` ( Poly1 ` R ) ) )
82 81 sselda 
 |-  ( ( ph /\ p e. U ) -> p e. ( Base ` ( Poly1 ` R ) ) )
83 65 73 3 74 75 76 82 fveval1fvcl 
 |-  ( ( ph /\ p e. U ) -> ( ( ( eval1 ` R ) ` p ) ` X ) e. B )
84 72 83 eqeltrd 
 |-  ( ( ph /\ p e. U ) -> ( ( O ` p ) ` X ) e. B )
85 84 8 fmptd 
 |-  ( ph -> F : U --> B )
86 1 3 2 13 4 63 64 41 42 43 44 45 evls1addd 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( ( O ` ( q ( +g ` P ) r ) ) ` X ) = ( ( ( O ` q ) ` X ) ( +g ` R ) ( ( O ` r ) ` X ) ) )
87 fveq2 
 |-  ( p = ( q ( +g ` P ) r ) -> ( O ` p ) = ( O ` ( q ( +g ` P ) r ) ) )
88 87 fveq1d 
 |-  ( p = ( q ( +g ` P ) r ) -> ( ( O ` p ) ` X ) = ( ( O ` ( q ( +g ` P ) r ) ) ` X ) )
89 49 ringgrpd 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> P e. Grp )
90 4 63 89 43 44 grpcld 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( q ( +g ` P ) r ) e. U )
91 fvexd 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( ( O ` ( q ( +g ` P ) r ) ) ` X ) e. _V )
92 8 88 90 91 fvmptd3 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( F ` ( q ( +g ` P ) r ) ) = ( ( O ` ( q ( +g ` P ) r ) ) ` X ) )
93 56 60 oveq12d 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( ( F ` q ) ( +g ` R ) ( F ` r ) ) = ( ( ( O ` q ) ` X ) ( +g ` R ) ( ( O ` r ) ` X ) ) )
94 86 92 93 3eqtr4d 
 |-  ( ( ph /\ ( q e. U /\ r e. U ) ) -> ( F ` ( q ( +g ` P ) r ) ) = ( ( F ` q ) ( +g ` R ) ( F ` r ) ) )
95 4 9 10 11 12 18 19 40 62 3 63 64 85 94 isrhmd 
 |-  ( ph -> F e. ( P RingHom R ) )