Metamath Proof Explorer

Theorem rhmply1vsca

Description: Apply a ring homomorphism between two univariate polynomial algebras to a scaled polynomial. (Contributed by SN, 20-May-2025)

Ref Expression
Hypotheses rhmply1vsca.p 
|- P = ( Poly1 ` R )
rhmply1vsca.q 
|- Q = ( Poly1 ` S )
rhmply1vsca.b 
|- B = ( Base ` P )
rhmply1vsca.k 
|- K = ( Base ` R )
rhmply1vsca.f 
|- F = ( p e. B |-> ( H o. p ) )
rhmply1vsca.t 
|- .x. = ( .s ` P )
rhmply1vsca.u 
|- .xb = ( .s ` Q )
rhmply1vsca.h 
|- ( ph -> H e. ( R RingHom S ) )
rhmply1vsca.c 
|- ( ph -> C e. K )
rhmply1vsca.x 
|- ( ph -> X e. B )
Assertion rhmply1vsca 
|- ( ph -> ( F ` ( C .x. X ) ) = ( ( H ` C ) .xb ( F ` X ) ) )

Proof

Step Hyp Ref Expression
1 rhmply1vsca.p 
 |-  P = ( Poly1 ` R )
2 rhmply1vsca.q 
 |-  Q = ( Poly1 ` S )
3 rhmply1vsca.b 
 |-  B = ( Base ` P )
4 rhmply1vsca.k 
 |-  K = ( Base ` R )
5 rhmply1vsca.f 
 |-  F = ( p e. B |-> ( H o. p ) )
6 rhmply1vsca.t 
 |-  .x. = ( .s ` P )
7 rhmply1vsca.u 
 |-  .xb = ( .s ` Q )
8 rhmply1vsca.h 
 |-  ( ph -> H e. ( R RingHom S ) )
9 rhmply1vsca.c 
 |-  ( ph -> C e. K )
10 rhmply1vsca.x 
 |-  ( ph -> X e. B )
11 fconst6g 
 |-  ( C e. K -> ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) : { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } --> K )
12 9 11 syl 
 |-  ( ph -> ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) : { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } --> K )
13 psr1baslem 
 |-  ( NN0 ^m 1o ) = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin }
14 13 feq2i 
 |-  ( ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) : ( NN0 ^m 1o ) --> K <-> ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) : { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } --> K )
15 12 14 sylibr 
 |-  ( ph -> ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) : ( NN0 ^m 1o ) --> K )
16 1 3 4 ply1basf 
 |-  ( X e. B -> X : ( NN0 ^m 1o ) --> K )
17 10 16 syl 
 |-  ( ph -> X : ( NN0 ^m 1o ) --> K )
18 eqid 
 |-  ( Base ` S ) = ( Base ` S )
19 4 18 rhmf 
 |-  ( H e. ( R RingHom S ) -> H : K --> ( Base ` S ) )
20 8 19 syl 
 |-  ( ph -> H : K --> ( Base ` S ) )
21 20 ffnd 
 |-  ( ph -> H Fn K )
22 ovexd 
 |-  ( ph -> ( NN0 ^m 1o ) e. _V )
23 rhmrcl1 
 |-  ( H e. ( R RingHom S ) -> R e. Ring )
24 8 23 syl 
 |-  ( ph -> R e. Ring )
25 eqid 
 |-  ( .r ` R ) = ( .r ` R )
26 4 25 ringcl 
 |-  ( ( R e. Ring /\ a e. K /\ b e. K ) -> ( a ( .r ` R ) b ) e. K )
27 24 26 syl3an1 
 |-  ( ( ph /\ a e. K /\ b e. K ) -> ( a ( .r ` R ) b ) e. K )
28 27 3expb 
 |-  ( ( ph /\ ( a e. K /\ b e. K ) ) -> ( a ( .r ` R ) b ) e. K )
29 eqid 
 |-  ( .r ` S ) = ( .r ` S )
30 4 25 29 rhmmul 
 |-  ( ( H e. ( R RingHom S ) /\ a e. K /\ b e. K ) -> ( H ` ( a ( .r ` R ) b ) ) = ( ( H ` a ) ( .r ` S ) ( H ` b ) ) )
31 8 30 syl3an1 
 |-  ( ( ph /\ a e. K /\ b e. K ) -> ( H ` ( a ( .r ` R ) b ) ) = ( ( H ` a ) ( .r ` S ) ( H ` b ) ) )
32 31 3expb 
 |-  ( ( ph /\ ( a e. K /\ b e. K ) ) -> ( H ` ( a ( .r ` R ) b ) ) = ( ( H ` a ) ( .r ` S ) ( H ` b ) ) )
33 15 17 21 22 28 32 coof 
 |-  ( ph -> ( H o. ( ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) oF ( .r ` R ) X ) ) = ( ( H o. ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) ) oF ( .r ` S ) ( H o. X ) ) )
34 fcoconst 
 |-  ( ( H Fn K /\ C e. K ) -> ( H o. ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) ) = ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { ( H ` C ) } ) )
35 21 9 34 syl2anc 
 |-  ( ph -> ( H o. ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) ) = ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { ( H ` C ) } ) )
36 35 oveq1d 
 |-  ( ph -> ( ( H o. ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) ) oF ( .r ` S ) ( H o. X ) ) = ( ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { ( H ` C ) } ) oF ( .r ` S ) ( H o. X ) ) )
37 33 36 eqtrd 
 |-  ( ph -> ( H o. ( ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) oF ( .r ` R ) X ) ) = ( ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { ( H ` C ) } ) oF ( .r ` S ) ( H o. X ) ) )
38 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
39 eqid 
 |-  ( .s ` ( 1o mPoly R ) ) = ( .s ` ( 1o mPoly R ) )
40 1 3 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
41 eqid 
 |-  { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin }
42 38 39 4 40 25 41 9 10 mplvsca 
 |-  ( ph -> ( C ( .s ` ( 1o mPoly R ) ) X ) = ( ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) oF ( .r ` R ) X ) )
43 42 coeq2d 
 |-  ( ph -> ( H o. ( C ( .s ` ( 1o mPoly R ) ) X ) ) = ( H o. ( ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { C } ) oF ( .r ` R ) X ) ) )
44 eqid 
 |-  ( 1o mPoly S ) = ( 1o mPoly S )
45 eqid 
 |-  ( .s ` ( 1o mPoly S ) ) = ( .s ` ( 1o mPoly S ) )
46 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
47 2 46 ply1bas 
 |-  ( Base ` Q ) = ( Base ` ( 1o mPoly S ) )
48 20 9 ffvelcdmd 
 |-  ( ph -> ( H ` C ) e. ( Base ` S ) )
49 rhmghm 
 |-  ( H e. ( R RingHom S ) -> H e. ( R GrpHom S ) )
50 ghmmhm 
 |-  ( H e. ( R GrpHom S ) -> H e. ( R MndHom S ) )
51 8 49 50 3syl 
 |-  ( ph -> H e. ( R MndHom S ) )
52 1 2 3 46 51 10 mhmcoply1 
 |-  ( ph -> ( H o. X ) e. ( Base ` Q ) )
53 44 45 18 47 29 41 48 52 mplvsca 
 |-  ( ph -> ( ( H ` C ) ( .s ` ( 1o mPoly S ) ) ( H o. X ) ) = ( ( { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } X. { ( H ` C ) } ) oF ( .r ` S ) ( H o. X ) ) )
54 37 43 53 3eqtr4d 
 |-  ( ph -> ( H o. ( C ( .s ` ( 1o mPoly R ) ) X ) ) = ( ( H ` C ) ( .s ` ( 1o mPoly S ) ) ( H o. X ) ) )
55 1 38 6 ply1vsca 
 |-  .x. = ( .s ` ( 1o mPoly R ) )
56 55 oveqi 
 |-  ( C .x. X ) = ( C ( .s ` ( 1o mPoly R ) ) X )
57 56 coeq2i 
 |-  ( H o. ( C .x. X ) ) = ( H o. ( C ( .s ` ( 1o mPoly R ) ) X ) )
58 2 44 7 ply1vsca 
 |-  .xb = ( .s ` ( 1o mPoly S ) )
59 58 oveqi 
 |-  ( ( H ` C ) .xb ( H o. X ) ) = ( ( H ` C ) ( .s ` ( 1o mPoly S ) ) ( H o. X ) )
60 54 57 59 3eqtr4g 
 |-  ( ph -> ( H o. ( C .x. X ) ) = ( ( H ` C ) .xb ( H o. X ) ) )
61 coeq2 
 |-  ( p = ( C .x. X ) -> ( H o. p ) = ( H o. ( C .x. X ) ) )
62 1 3 4 6 24 9 10 ply1vscl 
 |-  ( ph -> ( C .x. X ) e. B )
63 8 62 coexd 
 |-  ( ph -> ( H o. ( C .x. X ) ) e. _V )
64 5 61 62 63 fvmptd3 
 |-  ( ph -> ( F ` ( C .x. X ) ) = ( H o. ( C .x. X ) ) )
65 coeq2 
 |-  ( p = X -> ( H o. p ) = ( H o. X ) )
66 8 10 coexd 
 |-  ( ph -> ( H o. X ) e. _V )
67 5 65 10 66 fvmptd3 
 |-  ( ph -> ( F ` X ) = ( H o. X ) )
68 67 oveq2d 
 |-  ( ph -> ( ( H ` C ) .xb ( F ` X ) ) = ( ( H ` C ) .xb ( H o. X ) ) )
69 60 64 68 3eqtr4d 
 |-  ( ph -> ( F ` ( C .x. X ) ) = ( ( H ` C ) .xb ( F ` X ) ) )