Metamath Proof Explorer


Theorem rhmply1

Description: Provide a ring homomorphism between two univariate polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 20-May-2025)

Ref Expression
Hypotheses rhmply1.p P = Poly 1 R
rhmply1.q Q = Poly 1 S
rhmply1.b B = Base P
rhmply1.f F = p B H p
rhmply1.h φ H R RingHom S
Assertion rhmply1 φ F P RingHom Q

Proof

Step Hyp Ref Expression
1 rhmply1.p P = Poly 1 R
2 rhmply1.q Q = Poly 1 S
3 rhmply1.b B = Base P
4 rhmply1.f F = p B H p
5 rhmply1.h φ H R RingHom S
6 eqid 1 𝑜 mPoly R = 1 𝑜 mPoly R
7 eqid 1 𝑜 mPoly S = 1 𝑜 mPoly S
8 1 3 ply1bas B = Base 1 𝑜 mPoly R
9 1oex 1 𝑜 V
10 9 a1i φ 1 𝑜 V
11 6 7 8 4 10 5 rhmmpl φ F 1 𝑜 mPoly R RingHom 1 𝑜 mPoly S
12 3 a1i φ B = Base P
13 eqid Base Q = Base Q
14 13 a1i φ Base Q = Base Q
15 8 a1i φ B = Base 1 𝑜 mPoly R
16 2 13 ply1bas Base Q = Base 1 𝑜 mPoly S
17 16 a1i φ Base Q = Base 1 𝑜 mPoly S
18 eqid + P = + P
19 1 6 18 ply1plusg + P = + 1 𝑜 mPoly R
20 19 oveqi x + P y = x + 1 𝑜 mPoly R y
21 20 a1i φ x B y B x + P y = x + 1 𝑜 mPoly R y
22 eqid + Q = + Q
23 2 7 22 ply1plusg + Q = + 1 𝑜 mPoly S
24 23 oveqi x + Q y = x + 1 𝑜 mPoly S y
25 24 a1i φ x Base Q y Base Q x + Q y = x + 1 𝑜 mPoly S y
26 eqid P = P
27 1 6 26 ply1mulr P = 1 𝑜 mPoly R
28 27 oveqi x P y = x 1 𝑜 mPoly R y
29 28 a1i φ x B y B x P y = x 1 𝑜 mPoly R y
30 eqid Q = Q
31 2 7 30 ply1mulr Q = 1 𝑜 mPoly S
32 31 oveqi x Q y = x 1 𝑜 mPoly S y
33 32 a1i φ x Base Q y Base Q x Q y = x 1 𝑜 mPoly S y
34 12 14 15 17 21 25 29 33 rhmpropd φ P RingHom Q = 1 𝑜 mPoly R RingHom 1 𝑜 mPoly S
35 11 34 eleqtrrd φ F P RingHom Q