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 𝑃 = ( PwSer1𝑅 )
rhmpsr1.q 𝑄 = ( PwSer1𝑆 )
rhmpsr1.b 𝐵 = ( Base ‘ 𝑃 )
rhmpsr1.f 𝐹 = ( 𝑝𝐵 ↦ ( 𝐻𝑝 ) )
rhmpsr1.h ( 𝜑𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion rhmpsr1 ( 𝜑𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )

Proof

Step Hyp Ref Expression
1 rhmpsr1.p 𝑃 = ( PwSer1𝑅 )
2 rhmpsr1.q 𝑄 = ( PwSer1𝑆 )
3 rhmpsr1.b 𝐵 = ( Base ‘ 𝑃 )
4 rhmpsr1.f 𝐹 = ( 𝑝𝐵 ↦ ( 𝐻𝑝 ) )
5 rhmpsr1.h ( 𝜑𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
6 eqid ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
7 eqid ( 1o mPwSer 𝑆 ) = ( 1o mPwSer 𝑆 )
8 1 3 6 psr1bas2 𝐵 = ( Base ‘ ( 1o mPwSer 𝑅 ) )
9 1oex 1o ∈ V
10 9 a1i ( 𝜑 → 1o ∈ V )
11 6 7 8 4 10 5 rhmpsr ( 𝜑𝐹 ∈ ( ( 1o mPwSer 𝑅 ) RingHom ( 1o mPwSer 𝑆 ) ) )
12 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
13 1 12 6 psr1bas2 ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPwSer 𝑅 ) )
14 13 a1i ( 𝜑 → ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
15 eqid ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
16 2 15 7 psr1bas2 ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPwSer 𝑆 ) )
17 16 a1i ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPwSer 𝑆 ) ) )
18 eqidd ( 𝜑 → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) )
19 eqidd ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 ) )
20 eqid ( +g𝑃 ) = ( +g𝑃 )
21 1 6 20 psr1plusg ( +g𝑃 ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
22 21 eqcomi ( +g ‘ ( 1o mPwSer 𝑅 ) ) = ( +g𝑃 )
23 22 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( +g ‘ ( 1o mPwSer 𝑅 ) ) = ( +g𝑃 ) )
24 23 oveqd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( +g ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( +g𝑃 ) 𝑦 ) )
25 eqid ( +g𝑄 ) = ( +g𝑄 )
26 2 7 25 psr1plusg ( +g𝑄 ) = ( +g ‘ ( 1o mPwSer 𝑆 ) )
27 26 eqcomi ( +g ‘ ( 1o mPwSer 𝑆 ) ) = ( +g𝑄 )
28 27 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( +g ‘ ( 1o mPwSer 𝑆 ) ) = ( +g𝑄 ) )
29 28 oveqd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝑥 ( +g ‘ ( 1o mPwSer 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g𝑄 ) 𝑦 ) )
30 eqid ( .r𝑃 ) = ( .r𝑃 )
31 1 6 30 psr1mulr ( .r𝑃 ) = ( .r ‘ ( 1o mPwSer 𝑅 ) )
32 31 eqcomi ( .r ‘ ( 1o mPwSer 𝑅 ) ) = ( .r𝑃 )
33 32 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( .r ‘ ( 1o mPwSer 𝑅 ) ) = ( .r𝑃 ) )
34 33 oveqd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( .r𝑃 ) 𝑦 ) )
35 eqid ( .r𝑄 ) = ( .r𝑄 )
36 2 7 35 psr1mulr ( .r𝑄 ) = ( .r ‘ ( 1o mPwSer 𝑆 ) )
37 36 eqcomi ( .r ‘ ( 1o mPwSer 𝑆 ) ) = ( .r𝑄 )
38 37 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( .r ‘ ( 1o mPwSer 𝑆 ) ) = ( .r𝑄 ) )
39 38 oveqd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝑥 ( .r ‘ ( 1o mPwSer 𝑆 ) ) 𝑦 ) = ( 𝑥 ( .r𝑄 ) 𝑦 ) )
40 14 17 18 19 24 29 34 39 rhmpropd ( 𝜑 → ( ( 1o mPwSer 𝑅 ) RingHom ( 1o mPwSer 𝑆 ) ) = ( 𝑃 RingHom 𝑄 ) )
41 11 40 eleqtrd ( 𝜑𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )