Metamath Proof Explorer

Theorem evl1maprhm

Description: The function F mapping polynomials p to their evaluation at a given point X is a ring homomorphism. (Contributed by metakunt, 19-May-2025)

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

Proof

Step Hyp Ref Expression
1 evl1maprhm.q 
 |-  O = ( eval1 ` R )
2 evl1maprhm.p 
 |-  P = ( Poly1 ` R )
3 evl1maprhm.b 
 |-  B = ( Base ` R )
4 evl1maprhm.u 
 |-  U = ( Base ` P )
5 evl1maprhm.r 
 |-  ( ph -> R e. CRing )
6 evl1maprhm.y 
 |-  ( ph -> X e. B )
7 evl1maprhm.f 
 |-  F = ( p e. U |-> ( ( O ` p ) ` X ) )
8 7 a1i 
 |-  ( ph -> F = ( p e. U |-> ( ( O ` p ) ` X ) ) )
9 ssidd 
 |-  ( ph -> ( Base ` R ) C_ ( Base ` R ) )
10 5 elexd 
 |-  ( ph -> R e. _V )
11 5 crngringd 
 |-  ( ph -> R e. Ring )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 12 subrgid 
 |-  ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
14 11 13 syl 
 |-  ( ph -> ( Base ` R ) e. ( SubRing ` R ) )
15 14 elexd 
 |-  ( ph -> ( Base ` R ) e. _V )
16 eqid 
 |-  ( R |`s ( Base ` R ) ) = ( R |`s ( Base ` R ) )
17 16 12 ressid2 
 |-  ( ( ( Base ` R ) C_ ( Base ` R ) /\ R e. _V /\ ( Base ` R ) e. _V ) -> ( R |`s ( Base ` R ) ) = R )
18 9 10 15 17 syl3anc 
 |-  ( ph -> ( R |`s ( Base ` R ) ) = R )
19 eqcom 
 |-  ( ( R |`s ( Base ` R ) ) = R <-> R = ( R |`s ( Base ` R ) ) )
20 19 imbi2i 
 |-  ( ( ph -> ( R |`s ( Base ` R ) ) = R ) <-> ( ph -> R = ( R |`s ( Base ` R ) ) ) )
21 18 20 mpbi 
 |-  ( ph -> R = ( R |`s ( Base ` R ) ) )
22 21 fveq2d 
 |-  ( ph -> ( Poly1 ` R ) = ( Poly1 ` ( R |`s ( Base ` R ) ) ) )
23 2 22 eqtrid 
 |-  ( ph -> P = ( Poly1 ` ( R |`s ( Base ` R ) ) ) )
24 23 fveq2d 
 |-  ( ph -> ( Base ` P ) = ( Base ` ( Poly1 ` ( R |`s ( Base ` R ) ) ) ) )
25 4 24 eqtrid 
 |-  ( ph -> U = ( Base ` ( Poly1 ` ( R |`s ( Base ` R ) ) ) ) )
26 1 12 evl1fval1 
 |-  O = ( R evalSub1 ( Base ` R ) )
27 26 a1i 
 |-  ( ph -> O = ( R evalSub1 ( Base ` R ) ) )
28 27 fveq1d 
 |-  ( ph -> ( O ` p ) = ( ( R evalSub1 ( Base ` R ) ) ` p ) )
29 28 fveq1d 
 |-  ( ph -> ( ( O ` p ) ` X ) = ( ( ( R evalSub1 ( Base ` R ) ) ` p ) ` X ) )
30 25 29 mpteq12dv 
 |-  ( ph -> ( p e. U |-> ( ( O ` p ) ` X ) ) = ( p e. ( Base ` ( Poly1 ` ( R |`s ( Base ` R ) ) ) ) |-> ( ( ( R evalSub1 ( Base ` R ) ) ` p ) ` X ) ) )
31 eqid 
 |-  ( R evalSub1 ( Base ` R ) ) = ( R evalSub1 ( Base ` R ) )
32 eqid 
 |-  ( Poly1 ` ( R |`s ( Base ` R ) ) ) = ( Poly1 ` ( R |`s ( Base ` R ) ) )
33 eqid 
 |-  ( Base ` ( Poly1 ` ( R |`s ( Base ` R ) ) ) ) = ( Base ` ( Poly1 ` ( R |`s ( Base ` R ) ) ) )
34 6 3 eleqtrdi 
 |-  ( ph -> X e. ( Base ` R ) )
35 eqid 
 |-  ( p e. ( Base ` ( Poly1 ` ( R |`s ( Base ` R ) ) ) ) |-> ( ( ( R evalSub1 ( Base ` R ) ) ` p ) ` X ) ) = ( p e. ( Base ` ( Poly1 ` ( R |`s ( Base ` R ) ) ) ) |-> ( ( ( R evalSub1 ( Base ` R ) ) ` p ) ` X ) )
36 31 32 12 33 5 14 34 35 evls1maprhm 
 |-  ( ph -> ( p e. ( Base ` ( Poly1 ` ( R |`s ( Base ` R ) ) ) ) |-> ( ( ( R evalSub1 ( Base ` R ) ) ` p ) ` X ) ) e. ( ( Poly1 ` ( R |`s ( Base ` R ) ) ) RingHom R ) )
37 30 36 eqeltrd 
 |-  ( ph -> ( p e. U |-> ( ( O ` p ) ` X ) ) e. ( ( Poly1 ` ( R |`s ( Base ` R ) ) ) RingHom R ) )
38 2 a1i 
 |-  ( ph -> P = ( Poly1 ` R ) )
39 18 eqcomd 
 |-  ( ph -> R = ( R |`s ( Base ` R ) ) )
40 39 fveq2d 
 |-  ( ph -> ( Poly1 ` R ) = ( Poly1 ` ( R |`s ( Base ` R ) ) ) )
41 38 40 eqtr2d 
 |-  ( ph -> ( Poly1 ` ( R |`s ( Base ` R ) ) ) = P )
42 41 oveq1d 
 |-  ( ph -> ( ( Poly1 ` ( R |`s ( Base ` R ) ) ) RingHom R ) = ( P RingHom R ) )
43 37 42 eleqtrd 
 |-  ( ph -> ( p e. U |-> ( ( O ` p ) ` X ) ) e. ( P RingHom R ) )
44 8 43 eqeltrd 
 |-  ( ph -> F e. ( P RingHom R ) )