Metamath Proof Explorer


Theorem rhmpsr1

Description: Provide a ring homomorphism between two univariate power series algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 8-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 rhmpsr1.p P = PwSer 1 R
2 rhmpsr1.q Q = PwSer 1 S
3 rhmpsr1.b B = Base P
4 rhmpsr1.f F = p B H p
5 rhmpsr1.h φ H R RingHom S
6 eqid 1 𝑜 mPwSer R = 1 𝑜 mPwSer R
7 eqid 1 𝑜 mPwSer S = 1 𝑜 mPwSer S
8 1 3 6 psr1bas2 B = Base 1 𝑜 mPwSer R
9 1oex 1 𝑜 V
10 9 a1i φ 1 𝑜 V
11 6 7 8 4 10 5 rhmpsr φ F 1 𝑜 mPwSer R RingHom 1 𝑜 mPwSer S
12 eqid Base P = Base P
13 1 12 6 psr1bas2 Base P = Base 1 𝑜 mPwSer R
14 13 a1i φ Base P = Base 1 𝑜 mPwSer R
15 eqid Base Q = Base Q
16 2 15 7 psr1bas2 Base Q = Base 1 𝑜 mPwSer S
17 16 a1i φ Base Q = Base 1 𝑜 mPwSer S
18 eqidd φ Base P = Base P
19 eqidd φ Base Q = Base Q
20 eqid + P = + P
21 1 6 20 psr1plusg + P = + 1 𝑜 mPwSer R
22 21 eqcomi + 1 𝑜 mPwSer R = + P
23 22 a1i φ x Base P y Base P + 1 𝑜 mPwSer R = + P
24 23 oveqd φ x Base P y Base P x + 1 𝑜 mPwSer R y = x + P y
25 eqid + Q = + Q
26 2 7 25 psr1plusg + Q = + 1 𝑜 mPwSer S
27 26 eqcomi + 1 𝑜 mPwSer S = + Q
28 27 a1i φ x Base Q y Base Q + 1 𝑜 mPwSer S = + Q
29 28 oveqd φ x Base Q y Base Q x + 1 𝑜 mPwSer S y = x + Q y
30 eqid P = P
31 1 6 30 psr1mulr P = 1 𝑜 mPwSer R
32 31 eqcomi 1 𝑜 mPwSer R = P
33 32 a1i φ x Base P y Base P 1 𝑜 mPwSer R = P
34 33 oveqd φ x Base P y Base P x 1 𝑜 mPwSer R y = x P y
35 eqid Q = Q
36 2 7 35 psr1mulr Q = 1 𝑜 mPwSer S
37 36 eqcomi 1 𝑜 mPwSer S = Q
38 37 a1i φ x Base Q y Base Q 1 𝑜 mPwSer S = Q
39 38 oveqd φ x Base Q y Base Q x 1 𝑜 mPwSer S y = x Q y
40 14 17 18 19 24 29 34 39 rhmpropd φ 1 𝑜 mPwSer R RingHom 1 𝑜 mPwSer S = P RingHom Q
41 11 40 eleqtrd φ F P RingHom Q