This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑄 ) )