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 = Poly 1 R
rhmply1vsca.q Q = Poly 1 S
rhmply1vsca.b B = Base P
rhmply1vsca.k K = Base R
rhmply1vsca.f F = p B H p
rhmply1vsca.t · ˙ = P
rhmply1vsca.u ˙ = Q
rhmply1vsca.h φ H R RingHom S
rhmply1vsca.c φ C K
rhmply1vsca.x φ X B
Assertion rhmply1vsca φ F C · ˙ X = H C ˙ F X

Proof

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